Grace/Cumulus/Set/WellOrder/Isomorphism.g17

Open in Workbench Download source

Imports

WellOrder

Declarations

Source

1-- Order isomorphisms: the pointwise characterisation, identity, inverse,2-- composition, restriction, images of initial segments, and the rigidity3-- of ordinals: an isomorphism between ordinals under membership is the4-- identity5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Set.WellOrder.Isomorphism11import WellOrder1213-- An order isomorphism, read through function application: for x and y14-- in A, x is below y exactly when f(x) is below f(y).15theorem OrderIsomorphism.apply_iff (f A r B s x y : Set)16  requires iso : OrderIsomorphism(f, A, r, B, s)17  requires hx : x ∈ A18  requires hy : y ∈ A19  shows relates(r, x, y) ↔ relates(s, f(x), f(y))20proof21  have function := Bijective.injective with iso.left22  have fFunction := Injective.function with function23  have valueX := FunctionBetween.apply_closed with fFunction, hx24  have valueY := FunctionBetween.apply_closed with fFunction, hy25  have relatedX := FunctionBetween.relates_apply with fFunction, hx26  have relatedY := FunctionBetween.relates_apply with fFunction, hy27  exact iso.right with x, hx, y, hy, f(x), valueX, f(y), valueY, relatedX, relatedY2829theorem OrderIsomorphism.of_apply (f A r B s : Set)30  requires bijective : BijectiveBetween(f, A, B)31  requires preserves : ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) ↔ relates(s, f(x), f(y))32  shows OrderIsomorphism(f, A, r, B, s)33proof34  have fFunction := Injective.function with (Bijective.injective with bijective)35  constructor36  . exact bijective37  . intros x hx y hy u hu v hv hxu hyv38    have valueU := FunctionBetween.apply_value with fFunction, hx, hxu39    have valueV := FunctionBetween.apply_value with fFunction, hy, hyv40    rw [← valueU, ← valueV]41    exact preserves with x, hx, y, hy4243theorem OrderIsomorphism.identity (A r : Set)44  shows OrderIsomorphism(identity(A), A, r, A, r)45proof46  apply OrderIsomorphism.of_apply with (identity.bijective at A)47  intros x hx y hy48  have fixedX := identity.apply with hx49  have fixedY := identity.apply with hy50  rw [fixedX, fixedY]51  constructor52  . intro h53    exact h54  . intro h55    exact h5657theorem OrderIsomorphism.inverse (f A r B s : Set)58  requires iso : OrderIsomorphism(f, A, r, B, s)59  shows OrderIsomorphism(converse(f, A, B), B, s, A, r)60proof61  have bijective := iso.left62  have inverse := converse.bijective with bijective63  have fFunction := Injective.function with (Bijective.injective with bijective)64  have gFunction := Injective.function with (Bijective.injective with inverse)65  apply OrderIsomorphism.of_apply with inverse66  intros u hu v hv67  have preimageU := FunctionBetween.apply_closed with gFunction, hu68  have preimageV := FunctionBetween.apply_closed with gFunction, hv69  have backU := Bijective.apply_inverse with bijective, hu70  have backV := Bijective.apply_inverse with bijective, hv71  have characterization := OrderIsomorphism.apply_iff with iso, preimageU, preimageV72  rw [backU, backV] at characterization73  constructor74  . intro h75    exact characterization.backward with h76  . intro h77    exact characterization.forward with h7879theorem OrderIsomorphism.compose (g f A r B s C t : Set)80  requires first : OrderIsomorphism(f, A, r, B, s)81  requires second : OrderIsomorphism(g, B, s, C, t)82  shows OrderIsomorphism(compose(g, f, A, B, C), A, r, C, t)83proof84  have fFunction := Injective.function with (Bijective.injective with first.left)85  have gFunction := Injective.function with (Bijective.injective with second.left)86  have bijective := compose.bijective with first.left, second.left87  apply OrderIsomorphism.of_apply with bijective88  intros x hx y hy89  have valueX := FunctionBetween.apply_closed with fFunction, hx90  have valueY := FunctionBetween.apply_closed with fFunction, hy91  have stepX := compose.apply with fFunction, gFunction, hx92  have stepY := compose.apply with fFunction, gFunction, hy93  rw [stepX, stepY]94  have innerCharacterization := OrderIsomorphism.apply_iff with first, hx, hy95  have outerCharacterization := OrderIsomorphism.apply_iff with second, valueX, valueY96  constructor97  . intro h98    exact outerCharacterization.forward with (innerCharacterization.forward with h)99  . intro h100    exact innerCharacterization.backward with (outerCharacterization.backward with h)101102-- Replacing the order on the domain by one that agrees on it.103theorem OrderIsomorphism.congr_left (f A r t B s : Set)104  requires iso : OrderIsomorphism(f, A, r, B, s)105  requires agree : ∀ x ∈ A, ∀ y ∈ A, relates(t, x, y) ↔ relates(r, x, y)106  shows OrderIsomorphism(f, A, t, B, s)107proof108  apply OrderIsomorphism.of_apply with iso.left109  intros x hx y hy110  have inner := agree with x, hx, y, hy111  have characterization := OrderIsomorphism.apply_iff with iso, hx, hy112  constructor113  . intro h114    exact characterization.forward with (inner.forward with h)115  . intro h116    exact inner.backward with (characterization.backward with h)117118-- The image of an initial segment under an isomorphism is an initial segment.119theorem OrderIsomorphism.image_initial (f A r B s I : Set)120  requires iso : OrderIsomorphism(f, A, r, B, s)121  requires initial : InitialSegment(A, r, I)122  shows InitialSegment(B, s, functionImage(f, I, B))123proof124  have hI := InitialSegment.subset with initial125  have bijective := iso.left126  have inverse := converse.bijective with bijective127  have gFunction := Injective.function with (Bijective.injective with inverse)128  constructor129  . intros y hy130    simp [functionImage.membership] at hy131    exact hy.left132  . intros y hy z hz hzy133    simp [functionImage.membership] at hy134    obtain ⟨inB, x, hx, shape⟩ := hy135    have hxA := hI with x, hx136    have hw := FunctionBetween.apply_closed with gFunction, hz137    have back := Bijective.apply_inverse with bijective, hz138    rw [shape, ← back] at hzy139    have characterization := OrderIsomorphism.apply_iff with iso, hw, hxA140    have below := characterization.backward with hzy141    have inI := initial.right with x, hx, converse(f, A, B)(z), hw, below142    rw ← back at hz143    rw ← back144    simp [functionImage.membership]145    constructor146    . exact hz147    . witness converse(f, A, B)(z)148      constructor149      . exact inI150      . rfl151152-- The order carried to the image of an injection is the transported order153-- of Set/OrderTransport; the restriction of an isomorphism to a subset of154-- its domain is an isomorphism onto the image under the restricted orders.155theorem OrderIsomorphism.restrict (f A r B s S : Set)156  requires iso : OrderIsomorphism(f, A, r, B, s)157  requires hS : S ⊆ A158  shows OrderIsomorphism(restrict(f, S), S, restrictOrder(r, S), functionImage(f, S, B), restrictOrder(s, functionImage(f, S, B)))159proof160  have fFunction := Injective.function with (Bijective.injective with iso.left)161  have closed : ∀ x ∈ S, f(x) ∈ functionImage(f, S, B)162    intros x hx163    have value := FunctionBetween.apply_closed with fFunction, (hS with x, hx)164    simp [functionImage.membership]165  have restricted := restrict.function with fFunction, hS, closed166  have injective : InjectiveBetween(restrict(f, S), S, functionImage(f, S, B))167    constructor168    . exact restricted169    . intros x hx y hy z hz hxz hyz170      have valueX := FunctionBetween.apply_value with restricted, hx, hxz171      have valueY := FunctionBetween.apply_value with restricted, hy, hyz172      have stepX := restrict.apply with fFunction, hS, closed, hx173      have stepY := restrict.apply with fFunction, hS, closed, hy174      rw stepX at valueX175      rw stepY at valueY176      have agree : f(x) = f(y)177        rw [valueX, valueY]178        rfl179      exact Injective.apply_cancel with (Bijective.injective with iso.left), (hS with x, hx), (hS with y, hy), agree180  have surjective : SurjectiveBetween(restrict(f, S), S, functionImage(f, S, B))181    constructor182    . exact restricted183    . intros y hy184      simp [functionImage.membership] at hy185      obtain ⟨inB, x, hx, shape⟩ := hy186      witness x187      constructor188      . exact hx189      . have related := FunctionBetween.relates_apply with restricted, hx190        have step := restrict.apply with fFunction, hS, closed, hx191        rwa [step, ← shape] at related192  apply OrderIsomorphism.of_apply with ⟨injective, surjective⟩193  intros x hx y hy194  have stepX := restrict.apply with fFunction, hS, closed, hx195  have stepY := restrict.apply with fFunction, hS, closed, hy196  rw [stepX, stepY]197  have characterization := OrderIsomorphism.apply_iff with iso, (hS with x, hx), (hS with y, hy)198  have imageX := closed with x, hx199  have imageY := closed with y, hy200  constructor201  . intro h202    have inner := restrictOrder.relates.forward with h203    apply restrictOrder.relates.backward204    exact ⟨(characterization.forward with inner.left), imageX, imageY⟩205  . intro h206    have inner := restrictOrder.relates.forward with h207    apply restrictOrder.relates.backward208    exact ⟨(characterization.backward with inner.left), hx, hy⟩209210-- Ordinals are rigid: an order isomorphism between two ordinals, each211-- under membership, fixes every point, so isomorphic ordinals are equal.212theorem OrderIsomorphism.ordinal_fixed (f α β γ : Set)213  requires hAlpha : α ∈ Ordinal214  requires hBeta : β ∈ Ordinal215  requires iso : OrderIsomorphism(f, α, membershipOn(α), β, membershipOn(β))216  requires hγ : γ ∈ α217  shows f(γ) = γ218proof219  revert hγ220  induction γ using membership221  intros current ih hCurrent222  have bijective := iso.left223  have fFunction := Injective.function with (Bijective.injective with bijective)224  have inverse := converse.bijective with bijective225  have gFunction := Injective.function with (Bijective.injective with inverse)226  have value := FunctionBetween.apply_closed with fFunction, hCurrent227  ext z228  constructor229  . intro hz230    have below := Ordinal.member_subset with hBeta, value231    have hzB := below with z, hz232    have hw := FunctionBetween.apply_closed with gFunction, hzB233    have back := Bijective.apply_inverse with bijective, hzB234    have fw := FunctionBetween.apply_closed with fFunction, hw235    have outerRule := membershipOn.relates with fw, value236    have innerRule := membershipOn.relates with hw, hCurrent237    have characterization := OrderIsomorphism.apply_iff with iso, hw, hCurrent238    rw ← back at hz239    have outer := outerRule.backward with hz240    have inner := characterization.backward with outer241    have member := innerRule.forward with inner242    have fixed := ih with converse(f, α, β)(z), member, hw243    rwa [← back, fixed]244  . intro hz245    have below := Ordinal.member_subset with hAlpha, hCurrent246    have hzA := below with z, hz247    have innerRule := membershipOn.relates with hzA, hCurrent248    have inner := innerRule.backward with hz249    have characterization := OrderIsomorphism.apply_iff with iso, hzA, hCurrent250    have outer := characterization.forward with inner251    have fz := FunctionBetween.apply_closed with fFunction, hzA252    have outerRule := membershipOn.relates with fz, value253    have member := outerRule.forward with outer254    have fixed := ih with z, hz, hzA255    rwa fixed at member256257theorem OrderIsomorphism.ordinal_equal (f α β : Set)258  requires hAlpha : α ∈ Ordinal259  requires hBeta : β ∈ Ordinal260  requires iso : OrderIsomorphism(f, α, membershipOn(α), β, membershipOn(β))261  shows α = β262proof263  have bijective := iso.left264  have fFunction := Injective.function with (Bijective.injective with bijective)265  have inverse := OrderIsomorphism.inverse with iso266  have gFunction := Injective.function with (Bijective.injective with inverse.left)267  apply Subset.antisymmetric268  . intros γ hγ269    have fixed := OrderIsomorphism.ordinal_fixed with hAlpha, hBeta, iso, hγ270    have value := FunctionBetween.apply_closed with fFunction, hγ271    rwa fixed at value272  . intros γ hγ273    have fixed := OrderIsomorphism.ordinal_fixed with hBeta, hAlpha, inverse, hγ274    have value := FunctionBetween.apply_closed with gFunction, hγ275    rwa fixed at value276