Grace/Cumulus/Set/Ordinal/OrderType.g17

Open in Workbench Download source

Imports

Cardinal.Hartogs · WellOrder.Isomorphism

Declarations

Source

1-- Order types of well-orders: the collapse is an isomorphism onto the type,2-- equal types give isomorphic orders, and any two well-orders are comparable,3-- one being isomorphic to an initial segment of the other4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Set.Ordinal.OrderType10import Cardinal.Hartogs11import WellOrder.Isomorphism1213theorem wellOrderType.order_isomorphism (A r : Set)14  requires order : WellOrder(A, r)15  shows OrderIsomorphism(16    wellOrderCollapseGraph(A, r), A, r,17    wellOrderType(A, r), membershipOn(wellOrderType(A, r)))18proof19  have active := wellOrderCollapseGraph.order_isomorphism with order20  apply OrderIsomorphism.congr_left with active21  intros x hx y hy22  have rule := activeWellOrderRelation.relates at x, y, A, r23  constructor24  . intro h25    exact rule.backward with ⟨h, order⟩26  . intro h27    have parts := rule.forward with h28    exact parts.left2930theorem wellOrderType.isomorphic_of_equal (A r B s : Set)31  requires orderA : WellOrder(A, r)32  requires orderB : WellOrder(B, s)33  requires equal : wellOrderType(A, r) = wellOrderType(B, s)34  shows ∃ f, OrderIsomorphism(f, A, r, B, s)35proof36  have typeA := wellOrderType.order_isomorphism with orderA37  have typeB := wellOrderType.order_isomorphism with orderB38  have inverse := OrderIsomorphism.inverse with typeB39  rw ← equal at inverse40  witness compose(41    converse(wellOrderCollapseGraph(B, s), B, wellOrderType(A, r)),42    wellOrderCollapseGraph(A, r), A, wellOrderType(A, r), B)43  exact OrderIsomorphism.compose with typeA, inverse4445theorem wellOrderType.equal_of_isomorphic (A r B s f : Set)46  requires orderA : WellOrder(A, r)47  requires orderB : WellOrder(B, s)48  requires iso : OrderIsomorphism(f, A, r, B, s)49  shows wellOrderType(A, r) = wellOrderType(B, s)50proof51  have typeA := wellOrderType.order_isomorphism with orderA52  have typeB := wellOrderType.order_isomorphism with orderB53  have inverseA := OrderIsomorphism.inverse with typeA54  have step := OrderIsomorphism.compose with inverseA, iso55  have whole := OrderIsomorphism.compose with step, typeB56  have alphaOrdinal := wellOrderType.ordinal with orderA57  have betaOrdinal := wellOrderType.ordinal with orderB58  exact OrderIsomorphism.ordinal_equal with alphaOrdinal, betaOrdinal, whole5960-- The order type is a complete invariant of a well-order.61theorem wellOrderType.equal_iff_isomorphic (A r B s : Set)62  requires orderA : WellOrder(A, r)63  requires orderB : WellOrder(B, s)64  shows wellOrderType(A, r) = wellOrderType(B, s) ↔65    ∃ f, OrderIsomorphism(f, A, r, B, s)66proof67  constructor68  . intro equal69    exact wellOrderType.isomorphic_of_equal with orderA, orderB, equal70  . intro isomorphic71    obtain ⟨f, iso⟩ := isomorphic72    exact wellOrderType.equal_of_isomorphic with orderA, orderB, iso7374-- Membership on an ordinal is membership on any larger set, restricted.75theorem membershipOn.restrict_relates (α β x y : Set)76  requires hSub : α ⊆ β77  requires hx : x ∈ α78  requires hy : y ∈ α79  shows relates(membershipOn(α), x, y) ↔80    relates(restrictOrder(membershipOn(β), α), x, y)81proof82  have inner := membershipOn.relates with hx, hy83  have outer := membershipOn.relates with (hSub with x, hx), (hSub with y, hy)84  have restricted := restrictOrder.relates at membershipOn(β), α, x, y85  constructor86  . intro h87    apply restricted.backward88    exact ⟨(outer.backward with (inner.forward with h)), hx, hy⟩89  . intro h90    have parts := restricted.forward with h91    exact inner.backward with (outer.forward with parts.left)9293theorem Ordinal.subset_initial_segment (α β : Set)94  requires ordinal : α ∈ Ordinal95  requires hSub : α ⊆ β96  shows InitialSegment(β, membershipOn(β), α)97proof98  constructor99  . exact hSub100  . intros x hx y hy hyx101    have rule := membershipOn.relates with hy, (hSub with x, hx)102    have below := rule.forward with hyx103    have inside := Ordinal.member_subset with ordinal, hx104    exact inside with y, below105106-- When the type of (A, r) sits inside the type of (B, s), carrying the107-- smaller type back into B through the collapse of (B, s) cuts out an108-- initial segment of B, and composing the two collapses maps A onto it.109def typeSegment (A r B s : Set) : Set :=110  functionImage(111    converse(wellOrderCollapseGraph(B, s), B, wellOrderType(B, s)),112    wellOrderType(A, r), B)113114def typeEmbedding (A r B s : Set) : Set :=115  compose(116    restrict(117      converse(wellOrderCollapseGraph(B, s), B, wellOrderType(B, s)),118      wellOrderType(A, r)),119    wellOrderCollapseGraph(A, r), A, wellOrderType(A, r),120    typeSegment(A, r, B, s))121122theorem typeSegment.initial (A r B s : Set)123  requires orderA : WellOrder(A, r)124  requires orderB : WellOrder(B, s)125  requires hSub : wellOrderType(A, r) ⊆ wellOrderType(B, s)126  shows InitialSegment(B, s, typeSegment(A, r, B, s))127proof128  have alphaOrdinal := wellOrderType.ordinal with orderA129  have typeB := wellOrderType.order_isomorphism with orderB130  have inverse := OrderIsomorphism.inverse with typeB131  have initial := Ordinal.subset_initial_segment with alphaOrdinal, hSub132  unfold typeSegment133  exact OrderIsomorphism.image_initial with inverse, initial134135theorem typeEmbedding.order_isomorphism (A r B s : Set)136  requires orderA : WellOrder(A, r)137  requires orderB : WellOrder(B, s)138  requires hSub : wellOrderType(A, r) ⊆ wellOrderType(B, s)139  shows OrderIsomorphism(140    typeEmbedding(A, r, B, s), A, r,141    typeSegment(A, r, B, s), restrictOrder(s, typeSegment(A, r, B, s)))142proof143  have typeA := wellOrderType.order_isomorphism with orderA144  have typeB := wellOrderType.order_isomorphism with orderB145  have inverse := OrderIsomorphism.inverse with typeB146  have restricted := OrderIsomorphism.restrict with inverse, hSub147  have agree : ∀ x ∈ wellOrderType(A, r), ∀ y ∈ wellOrderType(A, r),148      relates(membershipOn(wellOrderType(A, r)), x, y) ↔149        relates(restrictOrder(membershipOn(wellOrderType(B, s)), wellOrderType(A, r)), x, y)150    intros x hx y hy151    exact membershipOn.restrict_relates with hSub, hx, hy152  have adjusted := OrderIsomorphism.congr_left with restricted, agree153  unfold typeEmbedding154  unfold typeSegment155  exact OrderIsomorphism.compose with typeA, adjusted156157-- Comparability: one of two well-orders is isomorphic to an initial158-- segment of the other.159theorem WellOrder.comparable (A r B s : Set)160  requires orderA : WellOrder(A, r)161  requires orderB : WellOrder(B, s)162  shows (∃ I, ∃ f, InitialSegment(B, s, I) ∧163      OrderIsomorphism(f, A, r, I, restrictOrder(s, I))) ∨164    (∃ I, ∃ f, InitialSegment(A, r, I) ∧165      OrderIsomorphism(f, B, s, I, restrictOrder(r, I)))166proof167  have alphaOrdinal := wellOrderType.ordinal with orderA168  have betaOrdinal := wellOrderType.ordinal with orderB169  have comparison := Ordinal.subset_or_member with alphaOrdinal, betaOrdinal170  cases comparison with below | above171  . left172    witness typeSegment(A, r, B, s)173    witness typeEmbedding(A, r, B, s)174    exact ⟨(typeSegment.initial with orderA, orderB, below), (typeEmbedding.order_isomorphism with orderA, orderB, below)⟩175  . right176    have reversed := Ordinal.member_subset with alphaOrdinal, above177    witness typeSegment(B, s, A, r)178    witness typeEmbedding(B, s, A, r)179    exact ⟨(typeSegment.initial with orderB, orderA, reversed), (typeEmbedding.order_isomorphism with orderB, orderA, reversed)⟩180