Grace/Cumulus/Cardinal/Square.g17

Open in Workbench Download source

Imports

Algebra · Set.MaximalPrinciple

Declarations

Source

1-- Infinite cardinal arithmetic: an infinite set is equipotent with its own2-- square, hence with its union or product with any set it dominates. Among3-- the bijections from the square of an infinite subset onto that subset, a4-- maximal one, which exists by the maximal principle since such bijections5-- are closed under nested unions, already covers the whole set.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Cardinal.Square12import Algebra13import Set.MaximalPrinciple1415-- Bijections from the square of an infinite subset of A onto that subset.16def squareBijections (A : Set) : Set :=17  { f ∈ 𝒫((A × A) × A) | ∃ X ∈ 𝒫(A), Infinite(X) ∧ BijectiveBetween(f, X × X, X) }1819theorem squareBijections.of_bijective (A f X : Set)20  requires subset : X ⊆ A21  requires infinite : Infinite(X)22  requires bijective : BijectiveBetween(f, X × X, X)23  shows f ∈ squareBijections(A)24proof25  apply squareBijections.membership.backward26  have relation := FunctionBetween.relation with (Injective.function with (Bijective.injective with bijective))27  have fSubset : f ⊆ (X × X) × X := relation28  have squareInside := product.monotone with subset, subset29  have bound := product.monotone with squareInside, subset30  constructor31  . exact powerset.membership_iff.backward with (Subset.transitive with fSubset, bound)32  . refine ⟨X, (powerset.membership_iff.backward with subset), infinite, bijective⟩3334-- The subset is the range of the bijection.35theorem squareBijections.range (f A : Set)36  requires hf : f ∈ squareBijections(A)37  shows Infinite(range(f)) ∧ BijectiveBetween(f, range(f) × range(f), range(f)) ∧ range(f) ⊆ A38proof39  obtain ⟨bound, X, hX, infiniteX, bijective⟩ := squareBijections.membership.forward with hf40  have function := Injective.function with (Bijective.injective with bijective)41  have surjective := Bijective.surjective with bijective42  have equal : range(f) = X43    apply Subset.antisymmetric44    . exact range.subset with (FunctionBetween.relation with function)45    . intros x hx46      obtain ⟨p, hp, related⟩ := surjective.right with x, hx47      have member : (p, x) ∈ f := related48      exact range.contains with member49  rw equal50  have inside : X ⊆ A := powerset.membership_iff.forward with hX51  exact ⟨infiniteX, bijective, inside⟩5253-- A countable infinite subset seeds the family.54theorem squareBijections.nonempty (A : Set)55  requires infinite : Infinite(A)56  shows ∃ f, f ∈ squareBijections(A)57proof58  obtain ⟨g, injective⟩ := Infinite.omega_dominated with infinite59  have equipotent := Equipotent.image with injective60  have squareEquipotent := Equipotent.product with equipotent, equipotent61  have chain := Equipotent.transitive with (Equipotent.symmetric with squareEquipotent), omega.square62  obtain ⟨f, bijective⟩ := Equipotent.transitive with chain, equipotent63  witness f64  have inside := functionImage.subset at g, ℕ, A65  have infiniteImage : Infinite(functionImage(g, ℕ, A))66    apply Infinite.iff_omega_dominated.backward67    exact Dominated.of_equipotent with equipotent68  exact squareBijections.of_bijective with inside, infiniteImage, bijective6970-- Nested unions stay in the family: the union is a bijection from the71-- square of the union of the ranges onto that union.72theorem squareBijections.union_closed (A S : Set)73  requires inhabited : Nonempty(S)74  requires inside : S ⊆ squareBijections(A)75  requires nested : ∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C76  shows ⋃(S) ∈ squareBijections(A)77proof78  have bases : ∀ f ∈ S, Infinite(range(f)) ∧ BijectiveBetween(f, range(f) × range(f), range(f)) ∧ range(f) ⊆ A79    intros f hf80    exact squareBijections.range with (inside with f, hf)81  have common : ∀ f ∈ S, ∀ g ∈ S, ∃ h ∈ S, f ⊆ h ∧ g ⊆ h82    intros f hf g hg83    have split := nested with f, hf, g, hg84    cases split with fg | gf85    . refine ⟨g, hg, fg, (Subset.reflexive at g)⟩86    . refine ⟨f, hf, (Subset.reflexive at f), gf⟩87  have rangeInside : ∀ f ∈ S, range(f) ⊆ range(⋃(S))88    intros f hf89    exact range.monotone with (union.subset_of_member with hf)90  have bounds : ∀ p ∈ ⋃(S), ∃ f ∈ S, p ∈ f91    intros p hp92    exact union.membership.forward with hp93  have unionRelation : ⋃(S) ⊆ (range(⋃(S)) × range(⋃(S))) × range(⋃(S))94    intros p hp95    obtain ⟨f, hf, pf⟩ := bounds with p, hp96    obtain ⟨infiniteF, bijectiveF, rangeF⟩ := bases with f, hf97    have relationF := FunctionBetween.relation with (Injective.function with (Bijective.injective with bijectiveF))98    have fSubset : f ⊆ (range(f) × range(f)) × range(f) := relationF99    have grow := rangeInside with f, hf100    have squareGrow := product.monotone with grow, grow101    have whole := product.monotone with squareGrow, grow102    exact whole with p, (fSubset with p, pf)103  have function : ⋃(S) : range(⋃(S)) × range(⋃(S)) → range(⋃(S))104    constructor105    . exact unionRelation106    . constructor107      . intros p y hpy z hpz108        have memberY : (p, y) ∈ ⋃(S) := hpy109        have memberZ : (p, z) ∈ ⋃(S) := hpz110        obtain ⟨f, hf, pf⟩ := bounds with (p, y), memberY111        obtain ⟨g, hg, pg⟩ := bounds with (p, z), memberZ112        obtain ⟨h, hh, fh, gh⟩ := common with f, hf, g, hg113        obtain ⟨infiniteH, bijectiveH, rangeH⟩ := bases with h, hh114        have functionalH := FunctionBetween.functional with (Injective.function with (Bijective.injective with bijectiveH))115        have relY : relates(h, p, y) := fh with (p, y), pf116        have relZ : relates(h, p, z) := gh with (p, z), pg117        exact functionalH with p, y, relY, z, relZ118      . intros p hp119        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp120        obtain ⟨qx, relatedX⟩ := range.membership_iff.forward with hx121        obtain ⟨qy, relatedY⟩ := range.membership_iff.forward with hy122        have memberX : (qx, x) ∈ ⋃(S) := relatedX123        have memberY : (qy, y) ∈ ⋃(S) := relatedY124        obtain ⟨f, hf, pf⟩ := bounds with (qx, x), memberX125        obtain ⟨g, hg, pg⟩ := bounds with (qy, y), memberY126        obtain ⟨h, hh, fh, gh⟩ := common with f, hf, g, hg127        obtain ⟨infiniteH, bijectiveH, rangeH⟩ := bases with h, hh128        have functionH := Injective.function with (Bijective.injective with bijectiveH)129        have xInH := range.contains with (fh with (qx, x), pf)130        have yInH := range.contains with (gh with (qy, y), pg)131        have pairIn : (x, y) ∈ range(h) × range(h) := product.pair with xInH, yInH132        obtain ⟨z, hz, related⟩ := FunctionBetween.exists_value with functionH, pairIn133        refine ⟨z, (rangeInside with h, hh, z, hz), ?_⟩134        rw shape135        have memberZ : ((x, y), z) ∈ h := related136        exact union.contains with hh, memberZ137  apply squareBijections.of_bijective at A, ⋃(S), range(⋃(S))138  . intros x hx139    obtain ⟨q, related⟩ := range.membership_iff.forward with hx140    have member : (q, x) ∈ ⋃(S) := related141    obtain ⟨f, hf, pf⟩ := bounds with (q, x), member142    obtain ⟨infiniteF, bijectiveF, rangeF⟩ := bases with f, hf143    have inRange := range.contains with pf144    exact rangeF with x, inRange145  . obtain ⟨f, hf⟩ := inhabited146    obtain ⟨infiniteF, bijectiveF, rangeF⟩ := bases with f, hf147    exact Infinite.of_subset with infiniteF, (rangeInside with f, hf)148  . constructor149    . constructor150      . exact function151      . intros p hp q hq z hz hpz hqz152        have memberP : (p, z) ∈ ⋃(S) := hpz153        have memberQ : (q, z) ∈ ⋃(S) := hqz154        obtain ⟨f, hf, pf⟩ := bounds with (p, z), memberP155        obtain ⟨g, hg, pg⟩ := bounds with (q, z), memberQ156        obtain ⟨h, hh, fh, gh⟩ := common with f, hf, g, hg157        obtain ⟨infiniteH, bijectiveH, rangeH⟩ := bases with h, hh158        have injectiveH := Bijective.injective with bijectiveH159        have functionH := Injective.function with injectiveH160        have relP : relates(h, p, z) := fh with (p, z), pf161        have relQ : relates(h, q, z) := gh with (q, z), pg162        have boundsP := FunctionBetween.bounds with functionH, relP163        have boundsQ := FunctionBetween.bounds with functionH, relQ164        exact Injective.cancel with injectiveH, boundsP.left, boundsQ.left, boundsP.right, relP, relQ165    . constructor166      . exact function167      . intros z hz168        obtain ⟨p, related⟩ := range.membership_iff.forward with hz169        have member : (p, z) ∈ ⋃(S) := related170        have pIn := unionRelation with (p, z), member171        have coordinates := product.pair_membership.forward with pIn172        refine ⟨p, coordinates.left, related⟩173174-- The square of a union splits into the square of the first set and the175-- three mixed products.176theorem product.union2_square (X Y : Set)177  shows (X ∪ Y) × (X ∪ Y) = (X × X) ∪ ((X × Y) ∪ ((Y × X) ∪ (Y × Y)))178proof179  rw [product.union2_left, product.union2_right, product.union2_right, union2.associative]180  rfl181182-- With X infinite, X × X ≃ X, and Y a disjoint copy of X, the three mixed183-- products together are a copy of Y.184theorem squareBijections.rest_equipotent (X Y : Set)185  requires infinite : Infinite(X)186  requires square : (X × X) ≃ X187  requires equipotent : X ≃ Y188  requires disjoint : Disjoint(X, Y)189  shows ((X × Y) ∪ ((Y × X) ∪ (Y × Y))) ≃ Y190proof191  obtain ⟨a, ha, b, hb, distinct⟩ := Infinite.two_points with infinite192  have yDisjoint := Disjoint.symmetric with disjoint193  have squareDominated := Dominated.of_equipotent with square194  have yToX := Dominated.of_equipotent with (Equipotent.symmetric with equipotent)195  have xToY := Dominated.of_equipotent with equipotent196  have xSelf := Dominated.reflexive at X197  have xy := Dominated.transitive with (Dominated.product with xSelf, yToX), squareDominated198  have yx := Dominated.transitive with (Dominated.product with yToX, xSelf), squareDominated199  have yy := Dominated.transitive with (Dominated.product with yToX, yToX), squareDominated200  have innerDisjoint : Disjoint(Y × X, Y × Y) := product.disjoint_of_right with disjoint201  have inner := Dominated.union_of_two_points with yx, yy, ha, hb, distinct, innerDisjoint202  have innerX := Dominated.transitive with inner, squareDominated203  have outerDisjoint : Disjoint(X × Y, (Y × X) ∪ (Y × Y))204    apply Disjoint.symmetric205    apply Disjoint.union2_iff.backward206    constructor207    . exact product.disjoint_of_left with yDisjoint208    . exact product.disjoint_of_left with yDisjoint209  have rest := Dominated.union_of_two_points with xy, innerX, ha, hb, distinct, outerDisjoint210  have restY := Dominated.transitive with (Dominated.transitive with rest, squareDominated), xToY211  obtain ⟨g, gBijective⟩ := equipotent212  have gFunction := Injective.function with (Bijective.injective with gBijective)213  have point := FunctionBetween.apply_closed with gFunction, ha214  have inhabited : Nonempty(Y) := ⟨g(a), point⟩215  have up := Dominated.left_factor at Y, Y with inhabited216  have step1 := union2.subset_right at (Y × X), (Y × Y)217  have step2 := union2.subset_right at (X × Y), ((Y × X) ∪ (Y × Y))218  have inside := Subset.transitive with step1, step2219  have yRest := Dominated.transitive with up, (Dominated.of_subset with inside)220  exact Dominated.antisymmetric with restY, yRest221222-- A disjoint copy of the range extends a member of the family properly.223theorem squareBijections.extend (A M Y : Set)224  requires hM : M ∈ squareBijections(A)225  requires hY : Y ⊆ A226  requires disjoint : Disjoint(range(M), Y)227  requires equipotent : range(M) ≃ Y228  shows ∃ J ∈ squareBijections(A), M ⊆ J ∧ J ≠ M229proof230  obtain ⟨infiniteX, bijective, rangeInside⟩ := squareBijections.range with hM231  have squareEquipotent : (range(M) × range(M)) ≃ range(M) := ⟨M, bijective⟩232  obtain ⟨k, kBijective⟩ := squareBijections.rest_equipotent with infiniteX, squareEquipotent, equipotent, disjoint233  have yDisjoint := Disjoint.symmetric with disjoint234  have domainsDisjoint : Disjoint(range(M) × range(M), (range(M) × Y) ∪ ((Y × range(M)) ∪ (Y × Y)))235    apply Disjoint.symmetric236    apply Disjoint.union2_iff.backward237    constructor238    . exact product.disjoint_of_right with yDisjoint239    . apply Disjoint.union2_iff.backward240      constructor241      . exact product.disjoint_of_left with yDisjoint242      . exact product.disjoint_of_left with yDisjoint243  have jBijective := Bijective.union_disjoint with bijective, kBijective, domainsDisjoint, disjoint244  have square := product.union2_square at range(M), Y245  rw ← square at jBijective246  have unionInside := union2.subset with rangeInside, hY247  have infiniteUnion := Infinite.of_subset with infiniteX, (union2.subset_left at range(M), Y)248  have hJ := squareBijections.of_bijective with unionInside, infiniteUnion, jBijective249  refine ⟨M ∪ k, hJ, (union2.subset_left at M, k), ?_⟩250  intro equal251  obtain ⟨a, ha, b, hb, distinct⟩ := Infinite.two_points with infiniteX252  obtain ⟨g, gBijective⟩ := equipotent253  have gFunction := Injective.function with (Bijective.injective with gBijective)254  have point := FunctionBetween.apply_closed with gFunction, ha255  have kSurjective := Bijective.surjective with kBijective256  obtain ⟨p, hp, related⟩ := kSurjective.right with g(a), point257  have inK : (p, g(a)) ∈ k := related258  have inJ := union2.right at (p, g(a)), M, k with inK259  rw equal at inJ260  have relationM := FunctionBetween.relation with (Injective.function with (Bijective.injective with bijective))261  have mSubset : M ⊆ (range(M) × range(M)) × range(M) := relationM262  have inProduct := mSubset with (p, g(a)), inJ263  have coordinates := product.pair_membership.forward with inProduct264  have separated := Disjoint.iff.forward with disjoint265  exact separated with g(a), coordinates.right, point266267-- A maximal member of the family covers A: either the complement of the268-- range is dominated by the range, and then A is a copy of the range, or269-- the range injects into its complement, which yields a proper extension.270theorem squareBijections.maximal_full (A M : Set)271  requires hM : M ∈ squareBijections(A)272  requires maximal : ∀ J ∈ squareBijections(A), M ⊆ J → J = M273  shows A ≃ range(M)274proof275  obtain ⟨infiniteX, bijective, rangeInside⟩ := squareBijections.range with hM276  have squareEquipotent : (range(M) × range(M)) ≃ range(M) := ⟨M, bijective⟩277  have comparison := Dominated.total at A ∖ range(M), range(M)278  cases comparison with small | large279  . obtain ⟨a, ha, b, hb, distinct⟩ := Infinite.two_points with infiniteX280    have cover := difference.union2_of_subset with rangeInside281    have disjoint := Disjoint.symmetric with (difference.disjoint at A, range(M))282    have unionDominated := Dominated.union_of_two_points with (Dominated.reflexive at range(M)), small, ha, hb, distinct, disjoint283    rw cover at unionDominated284    have down := Dominated.transitive with unionDominated, (Dominated.of_equipotent with squareEquipotent)285    exact Dominated.antisymmetric with down, (Dominated.of_subset with rangeInside)286  . exfalso287    obtain ⟨h, hInjective⟩ := large288    have yInside := functionImage.subset at h, range(M), A ∖ range(M)289    have yInA := Subset.transitive with yInside, (difference.subset_left at A, range(M))290    have disjoint := Disjoint.symmetric with (Disjoint.of_subset_left with (difference.disjoint at A, range(M)), yInside)291    have equipotent := Equipotent.image with hInjective292    obtain ⟨J, hJ, extends, different⟩ := squareBijections.extend with hM, yInA, disjoint, equipotent293    exact different with (maximal with J, hJ, extends)294295theorem Infinite.square (A : Set)296  requires infinite : Infinite(A)297  shows (A × A) ≃ A298proof299  obtain ⟨f, seed⟩ := squareBijections.nonempty with infinite300  have closed : ∀ S, Nonempty(S) → S ⊆ squareBijections(A) →301      (∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C) → ⋃(S) ∈ squareBijections(A)302    intros S inhabited inside nested303    exact squareBijections.union_closed with inhabited, inside, nested304  obtain ⟨M, hM, extends, maximal⟩ := maximal_extension with seed, closed305  have full := squareBijections.maximal_full with hM, maximal306  obtain ⟨infiniteX, bijective, rangeInside⟩ := squareBijections.range with hM307  have squareEquipotent : (range(M) × range(M)) ≃ range(M) := ⟨M, bijective⟩308  have squares := Equipotent.product with full, full309  have step := Equipotent.transitive with squares, squareEquipotent310  exact Equipotent.transitive with step, (Equipotent.symmetric with full)311312-- Consequences: an infinite set absorbs any set it dominates, by union or313-- by product.314theorem Infinite.union (A B : Set)315  requires infinite : Infinite(A)316  requires dominated : B ≼ A317  shows (A ∪ B) ≃ A318proof319  obtain ⟨a, ha, b, hb, distinct⟩ := Infinite.two_points with infinite320  have restDominated := Dominated.transitive with (Dominated.of_subset with (difference.subset_left at B, A)), dominated321  have disjoint := Disjoint.symmetric with (difference.disjoint at B, A)322  have unionDominated := Dominated.union_of_two_points with (Dominated.reflexive at A), restDominated, ha, hb, distinct, disjoint323  have cover := difference.union2_self at A, B324  rw cover at unionDominated325  have down := Dominated.transitive with unionDominated, (Dominated.of_equipotent with (Infinite.square with infinite))326  exact Dominated.antisymmetric with down, (Dominated.of_subset with (union2.subset_left at A, B))327328theorem Infinite.product (A B : Set)329  requires infinite : Infinite(A)330  requires dominated : B ≼ A331  requires inhabited : Nonempty(B)332  shows (A × B) ≃ A333proof334  have down := Dominated.transitive with (Dominated.product with (Dominated.reflexive at A), dominated), (Dominated.of_equipotent with (Infinite.square with infinite))335  have up := Dominated.left_factor at A, B with inhabited336  exact Dominated.antisymmetric with down, up337