Grace/Cumulus/Cardinal/Algebra.g17

Open in Workbench Download source

Imports

Set.Ordinal.OrderType · Infinite · CountableClosure

Declarations

Source

1-- The algebra of dominance and equipotence: products and disjoint sums2-- respect dominance, a factor embeds in a product, any two sets are3-- comparable under dominance, and the naturals square to themselves4-- 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.Cardinal.Algebra10import Set.Ordinal.OrderType11import Infinite12import CountableClosure1314theorem Dominated.product (A B C D : Set)15  requires hAC : A ≼ C16  requires hBD : B ≼ D17  shows (A × B) ≼ (C × D)18proof19  obtain ⟨f, hf⟩ := hAC20  obtain ⟨g, hg⟩ := hBD21  witness productMap(f, g, A, B, C, D)22  exact productMap.injective with hf, hg2324theorem Dominated.disjointSum (A B C D : Set)25  requires hAC : A ≼ C26  requires hBD : B ≼ D27  shows (A ⊎ B) ≼ (C ⊎ D)28proof29  obtain ⟨f, hf⟩ := hAC30  obtain ⟨g, hg⟩ := hBD31  witness sumMap(f, g, A, B, C, D)32  exact sumMap.injective with hf, hg3334theorem Equipotent.product_commutative (A B : Set)35  shows (A × B) ≃ (B × A)36proof37  witness productSwap(A, B)38  exact productSwap.bijective3940-- A factor embeds in the product once the other factor has a point.41defgraph pairWith (A B b : Set) (x ∈ A) : A × B := (x, b)42requires hb : b ∈ B43proof44  exact product.pair with hb4546theorem pairWith.injective (A B b : Set)47  requires hb : b ∈ B48  shows InjectiveBetween(pairWith(A, B, b), A, A × B)49proof50  have function := pairWith.function at A, B, b with *51  constructor52  . exact function53  . intros x hx y hy z hz hxz hyz54    have valueX := FunctionBetween.apply_value with function, hx, hxz55    have valueY := FunctionBetween.apply_value with function, hy, hyz56    have stepX := pairWith.value at A, B, b, x with *57    have stepY := pairWith.value at A, B, b, y with *58    have same : (x, b) = (y, b) by cc59    have parts := orderedPair.injective with same60    exact parts.left6162theorem Dominated.left_factor (A B : Set)63  requires inhabited : Nonempty(B)64  shows A ≼ A × B65proof66  obtain ⟨b, hb⟩ := inhabited67  witness pairWith(A, B, b)68  exact pairWith.injective with hb6970theorem Dominated.right_factor (A B : Set)71  requires inhabited : Nonempty(B)72  shows A ≼ B × A73proof74  have left := Dominated.left_factor at A, B with inhabited75  have swap := Dominated.of_equipotent with (Equipotent.product_commutative at A, B)76  exact Dominated.transitive with left, swap7778-- Any two sets are comparable: well-order both and compare the orders.79theorem Dominated.total (A B : Set)80  shows A ≼ B ∨ B ≼ A81proof82  obtain ⟨r, orderA⟩ := WellOrder.exists at A83  obtain ⟨s, orderB⟩ := WellOrder.exists at B84  have comparison := WellOrder.comparable with orderA, orderB85  cases comparison with intoB | intoA86  . obtain ⟨I, f, initial, iso⟩ := intoB87    left88    have hI := InitialSegment.subset with initial89    have injective := Bijective.injective with iso.left90    have toSegment := Dominated.of_injective with injective91    exact Dominated.transitive with toSegment, (Dominated.of_subset with hI)92  . obtain ⟨I, f, initial, iso⟩ := intoA93    right94    have hI := InitialSegment.subset with initial95    have injective := Bijective.injective with iso.left96    have toSegment := Dominated.of_injective with injective97    exact Dominated.transitive with toSegment, (Dominated.of_subset with hI)9899theorem omega.square100  shows (ℕ × ℕ) ≃ ℕ101proof102  obtain ⟨f, hf⟩ := Countable.product with naturals.countable, naturals.countable103  have down := Dominated.of_injective with hf104  have zeroNat : Nat(0) by typecheck105  have hzero : 0 ∈ ℕ := nat.omega.forward with zeroNat106  have inhabited : Nonempty(ℕ) := ⟨0, hzero⟩107  have up := Dominated.left_factor at ℕ, ℕ with inhabited108  exact Dominated.antisymmetric with down, up109110-- Infinite sets: closed upward, and holding two distinct points.111theorem Infinite.of_subset (A B : Set)112  requires infinite : Infinite(A)113  requires hAB : A ⊆ B114  shows Infinite(B)115proof116  unfold Infinite117  intro finite118  unfold Infinite at infinite119  apply infinite120  exact Finite.subset with finite, hAB121122theorem Infinite.two_points (A : Set)123  requires infinite : Infinite(A)124  shows ∃ a ∈ A, ∃ b ∈ A, a ≠ b125proof126  obtain ⟨g, injective⟩ := Infinite.omega_dominated with infinite127  have function := Injective.function with injective128  have zeroNat : Nat(0) by typecheck129  have oneNat : Nat(1) by typecheck130  have hzero : 0 ∈ ℕ := nat.omega.forward with zeroNat131  have hone : 1 ∈ ℕ := nat.omega.forward with oneNat132  have closedZero := FunctionBetween.apply_closed with function, hzero133  have closedOne := FunctionBetween.apply_closed with function, hone134  refine ⟨g(0), closedZero, g(1), closedOne, ?_⟩135  intro equal136  have same := Injective.apply_cancel with injective, equal137  exact zero.ne_one with same138139-- Two sets dominated by X, kept apart by two points of X, together sit140-- inside X × X: send one through (·, a) and the other through (·, b).141theorem Dominated.union_of_two_points (A B X a b : Set)142  requires hA : A ≼ X143  requires hB : B ≼ X144  requires ha : a ∈ X145  requires hb : b ∈ X146  requires distinct : a ≠ b147  requires disjoint : Disjoint(A, B)148  shows (A ∪ B) ≼ (X × X)149proof150  obtain ⟨f, hf⟩ := hA151  obtain ⟨g, hg⟩ := hB152  have fFunction := Injective.function with hf153  have gFunction := Injective.function with hg154  have pairA := pairWith.injective at X, X, a with ha155  have pairB := pairWith.injective at X, X, b with hb156  have pairAFunction := pairWith.function at X, X, a with ha157  have pairBFunction := pairWith.function at X, X, b with hb158  have leftInjective := compose.injective with hf, pairA159  have rightInjective := compose.injective with hg, pairB160  have leftCorestrict := Injective.corestrict with leftInjective161  have rightCorestrict := Injective.corestrict with rightInjective162  have imagesDisjoint : Disjoint(163      functionImage(compose(pairWith(X, X, a), f, A, X, X × X), A, X × X),164      functionImage(compose(pairWith(X, X, b), g, B, X, X × X), B, X × X))165    apply Disjoint.iff.backward166    intros p hp hp2167    simp [functionImage.membership] at hp168    simp [functionImage.membership] at hp2169    obtain ⟨pIn, x, hx, shapeX⟩ := hp170    obtain ⟨pIn2, y, hy, shapeY⟩ := hp2171    have stepX := compose.apply with fFunction, pairAFunction, hx172    have stepY := compose.apply with gFunction, pairBFunction, hy173    have closedX := FunctionBetween.apply_closed with fFunction, hx174    have closedY := FunctionBetween.apply_closed with gFunction, hy175    have valueX := pairWith.value with ha, closedX176    have valueY := pairWith.value with hb, closedY177    have same : (f(x), a) = (g(y), b) by cc178    have parts := orderedPair.injective with same179    exact distinct with parts.right180  have unionInjective := Injective.union_disjoint with leftCorestrict, rightCorestrict, disjoint, imagesDisjoint181  have dominated := Dominated.of_injective with unionInjective182  have leftInside := functionImage.subset at compose(pairWith(X, X, a), f, A, X, X × X), A, X × X183  have rightInside := functionImage.subset at compose(pairWith(X, X, b), g, B, X, X × X), B, X × X184  have inside := union2.subset with leftInside, rightInside185  exact Dominated.transitive with dominated, (Dominated.of_subset with inside)186