Grace/Cumulus/Set/OrderTransport.g17

Open in Workbench Download source

Imports

Order

Declarations

Source

1-- Transport of well-orders along injections, without Choice.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module Grace.Cumulus.Set.OrderTransport9import Order1011def transportedOrder (f A B r : Set) : Set :=12  {p ∈ B × B | ∃ x ∈ A, ∃ y ∈ A, relates(r, x, y) ∧ p = (f[x], f[y])}1314theorem transportedOrder.decode (f A B r u v : Set)15  requires related : relates(transportedOrder(f, A, B, r), u, v)16  shows ∃ x ∈ A, ∃ y ∈ A, relates(r, x, y) ∧ u = f[x] ∧ v = f[y]17proof18  unfold relates at related19  obtain ⟨bounded, x, hx, y, hy, edge, shape⟩ := transportedOrder.membership.forward with related20  obtain ⟨left, right⟩ := orderedPair.injective with shape21  refine ⟨x, hx, y, hy, edge, left, right⟩2223theorem transportedOrder.edge (f A B r x y : Set)24  requires function : f : A → B25  requires hx : x ∈ A26  requires hy : y ∈ A27  requires related : relates(r, x, y)28  shows relates(transportedOrder(f, A, B, r), f[x], f[y])29proof30  have left := FunctionBetween.apply_closed at f, A, B, x with *31  have right := FunctionBetween.apply_closed at f, A, B, y with *32  have pair := product.pair with left, right33  unfold relates34  exact transportedOrder.membership.backward with ⟨pair, x, hx, y, hy, related, rfl⟩3536theorem transportedOrder.reflect (f A B r x y : Set)37  requires injective : InjectiveBetween(f, A, B)38  requires hx : x ∈ A39  requires hy : y ∈ A40  requires related : relates(transportedOrder(f, A, B, r), f[x], f[y])41  shows relates(r, x, y)42proof43  obtain ⟨a, ha, b, hb, edge, left, right⟩ := transportedOrder.decode with related44  have sameA := Injective.apply_cancel with injective, hx, ha, left45  have sameB := Injective.apply_cancel with injective, hy, hb, right46  rw sameA47  rwa sameB4849theorem transportedOrder.relation (f A B r : Set)50  requires function : f : A → B51  shows RelationBetween(transportedOrder(f, A, B, r), functionImage(f, A, B), functionImage(f, A, B))52proof53  intros p member54  obtain ⟨bounded, x, hx, y, hy, edge, shape⟩ := transportedOrder.membership.forward with member55  have left := functionImage.value with hx56  have right := functionImage.value with hy57  rw shape58  exact product.pair with left, right5960theorem transportedOrder.strict_linear (f A B r : Set)61  requires injective : InjectiveBetween(f, A, B)62  requires order : StrictLinearOrder(A, r)63  shows StrictLinearOrder(functionImage(f, A, B), transportedOrder(f, A, B, r))64proof65  have function := Injective.function with injective66  have irreflexive := StrictLinearOrder.irreflexive with order67  have transitive := StrictLinearOrder.transitive with order68  have connected := StrictLinearOrder.connected with order69  constructor70    constructor71    . exact transportedOrder.relation at f, A, B, r with function72    . constructor73        intros u hu self74        obtain ⟨bound, x, hx, value⟩ := functionImage.membership.forward with hu75        rw value at self76        have original := transportedOrder.reflect at f, A, B, r, x, x with *77        exact irreflexive with x, hx, original78        intros u hu v hv w hw uv vw79        obtain ⟨bu, a, ha, uValue⟩ := functionImage.membership.forward with hu80        obtain ⟨bv, b, hb, vValue⟩ := functionImage.membership.forward with hv81        obtain ⟨bw, c, hc, wValue⟩ := functionImage.membership.forward with hw82        rw [uValue, vValue] at uv83        rw [vValue, wValue] at vw84        have ab := transportedOrder.reflect at f, A, B, r, a, b with *85        have bc := transportedOrder.reflect at f, A, B, r, b, c with *86        have ac := transitive with a, ha, b, hb, c, hc, ab, bc87        rw [uValue, wValue]88        exact transportedOrder.edge at f, A, B, r, a, c with *89    intros u hu v hv distinct90    obtain ⟨bu2, a2, ha2, uValue2⟩ := functionImage.membership.forward with hu91    obtain ⟨bv2, b2, hb2, vValue2⟩ := functionImage.membership.forward with hv92    have different : a2 ≠ b2 by simp93    have alternatives := connected with a2, ha2, b2, hb2, different94    rw [uValue2, vValue2]95    cases alternatives with ab2 | ba296    . left97      exact transportedOrder.edge at f, A, B, r, a2, b2 with *98    . right99      exact transportedOrder.edge at f, A, B, r, b2, a2 with *100101theorem transportedOrder.well_founded (f A B r : Set)102  requires injective : InjectiveBetween(f, A, B)103  requires founded : wellFoundedOn(r, A)104  shows wellFoundedOn(transportedOrder(f, A, B, r), functionImage(f, A, B))105proof106  intros S conditions107  rcases conditions with ⟨subsetS, nonemptyS⟩108  obtain ⟨u, hu⟩ := Nonempty.of_ne_empty with nonemptyS109  have inImage := subsetS with u, hu110  obtain ⟨bounded, x, hx, value⟩ := functionImage.membership.forward with inImage111  rw value at hu112  have preimageNonempty : Nonempty(functionPreimage(f, A, S)) := ⟨x, (functionPreimage.membership.backward with ⟨hx, hu⟩)⟩113  have preimageNe := Nonempty.ne_empty with preimageNonempty114  have preimageSubset : subset(functionPreimage(f, A, S), A) by simp [functionPreimage, subset]115  obtain ⟨m, hm, minimal⟩ := founded with functionPreimage(f, A, S), ⟨preimageSubset, preimageNe⟩116  obtain ⟨mInA, imageInS⟩ := functionPreimage.membership.forward with hm117  refine ⟨f[m], imageInS, ?_⟩118  intros v hv edge119  have vInImage := subsetS with v, hv120  obtain ⟨vBound, y, hy, vValue⟩ := functionImage.membership.forward with vInImage121  rw vValue at hv122  rw vValue at edge123  have yPreimage : y ∈ functionPreimage(f, A, S) := functionPreimage.membership.backward with ⟨hy, hv⟩124  have original := transportedOrder.reflect with *125  exact minimal with y, yPreimage, original126127theorem transportedOrder.well_order (f A B r : Set)128  requires injective : InjectiveBetween(f, A, B)129  requires order : WellOrder(A, r)130  shows WellOrder(functionImage(f, A, B), transportedOrder(f, A, B, r))131proof132  have strict := WellOrder.strict_linear with order133  have founded := WellOrder.well_founded with order134  constructor135  . exact transportedOrder.strict_linear with *136  . exact transportedOrder.well_founded with *137