Grace/Cumulus/Cardinal/Infinite.g17

Open in Workbench Download source

Imports

Set.WellOrdering · Dominance · ListSupport

Declarations

Source

1-- Infinite sets: a set is infinite exactly when the naturals inject into it,2-- and exactly when it is Dedekind-infinite, carrying an injective self-map3-- that is not onto. The forward direction well-orders the set and compares4-- its order type with ω; the backward direction follows the orbit of a5-- point outside the image.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.Infinite12import Set.WellOrdering13import Dominance14import ListSupport1516-- An infinite set admits an injection from the naturals: well-order it and17-- compare the order type with ω.18theorem Infinite.omega_dominated (A : Set)19  requires infinite : Infinite(A)20  shows ℕ ≼ A21proof22  obtain ⟨r, order⟩ := WellOrder.exists at A23  have typeOrdinal := wellOrderType.ordinal with order24  have omegaOrdinal := Ordinal.omega25  have collapse := wellOrderCollapseGraph.bijective with order26  have equipotent : A ≃ wellOrderType(A, r) := ⟨wellOrderCollapseGraph(A, r), collapse⟩27  have comparison := Ordinal.subset_or_member with omegaOrdinal, typeOrdinal28  cases comparison with below | small29  . have typeDominated := Dominated.of_equipotent with (Equipotent.symmetric with equipotent)30    have omegaDominated := Dominated.of_subset with below31    exact Dominated.transitive with omegaDominated, typeDominated32  . exfalso33    unfold Infinite at infinite34    apply infinite35    have natural := nat.omega.backward with small36    witness wellOrderType(A, r)37    exact ⟨natural, equipotent⟩3839-- The shift along an injective sequence g : ℕ → A sends g(n) to g(n + 1)40-- and fixes every point outside the range of g.41def shiftMap (g A : Set) : Set :=42  { p ∈ A × A | ∃ x ∈ A, ∃ y ∈ A,43      ((¬x ∈ functionImage(g, ℕ, A) ∧ y = x) ∨44        (∃ n ∈ ℕ, x = g(n) ∧ y = g(succ(n)))) ∧ p = (x, y) }4546theorem shiftMap.relates (g A x y : Set)47  shows relates(shiftMap(g, A), x, y) ↔ x ∈ A ∧ y ∈ A ∧48    ((¬x ∈ functionImage(g, ℕ, A) ∧ y = x) ∨49      (∃ n ∈ ℕ, x = g(n) ∧ y = g(succ(n))))50proof51  constructor52  . intro h53    unfold relates at h54    simp [shiftMap] at h55    obtain ⟨hproduct, u, hu, v, hv, rule, hpair⟩ := h56    obtain ⟨hxu, hyv⟩ := orderedPair.injective with hpair57    rw under hxu58    rw under hyv59    exact ⟨hu, hv, rule⟩60  . intro h61    obtain ⟨hx, hy, rule⟩ := h62    unfold relates63    exact shiftMap.backward with ⟨(product.pair with hx, hy), x, hx, y, hy, rule, rfl⟩6465theorem shiftMap.in_image (g A n : Set)66  requires function : g : ℕ → A67  requires hn : n ∈ ℕ68  shows g(n) ∈ functionImage(g, ℕ, A)69proof70  have value := FunctionBetween.apply_closed with function, hn71  simp [functionImage.membership]7273theorem shiftMap.function (g A : Set)74  requires injective : InjectiveBetween(g, ℕ, A)75  shows shiftMap(g, A) : A → A76proof77  have function := Injective.function with injective78  constructor79  . intros p hp80    simp [shiftMap] at hp81    exact hp.left82  . constructor83    . intros x y hxy z hxz84      obtain ⟨hx, hy, caseY⟩ := shiftMap.relates.forward with hxy85      obtain ⟨hx2, hz, caseZ⟩ := shiftMap.relates.forward with hxz86      cases caseY with fixedY | movedY87      . cases caseZ with fixedZ | movedZ88        . rw [fixedY.right, fixedZ.right]89          rfl90        . exfalso91          obtain ⟨n, hn, shapeX, shapeZ⟩ := movedZ92          apply fixedY.left93          rw shapeX94          exact shiftMap.in_image with function, hn95      . cases caseZ with fixedZ | movedZ96        . exfalso97          obtain ⟨n, hn, shapeX, shapeY⟩ := movedY98          apply fixedZ.left99          rw shapeX100          exact shiftMap.in_image with function, hn101        . obtain ⟨n, hn, xn, yn⟩ := movedY102          obtain ⟨m, hm, xm, zm⟩ := movedZ103          have same : g(n) = g(m) by cc104          have equal := Injective.apply_cancel with injective, hn, hm, same105          rw [yn, zm, equal]106          rfl107    . intros x hx108      have split : x ∈ functionImage(g, ℕ, A) ∨ ¬x ∈ functionImage(g, ℕ, A) by tauto109      cases split with inside | outside110      . simp [functionImage.membership] at inside111        obtain ⟨hxA, n, hn, shape⟩ := inside112        have hsucc := omega.successor with hn113        have value := FunctionBetween.apply_closed with function, hsucc114        witness g(succ(n))115        constructor116        . exact value117        . apply shiftMap.relates.backward118          refine ⟨hx, value, ?_⟩119          right120          refine ⟨n, hn, shape, rfl⟩121      . witness x122        constructor123        . exact hx124        . apply shiftMap.relates.backward125          refine ⟨hx, hx, ?_⟩126          left127          exact ⟨outside, rfl⟩128129theorem shiftMap.injective (g A : Set)130  requires injective : InjectiveBetween(g, ℕ, A)131  shows InjectiveBetween(shiftMap(g, A), A, A)132proof133  have function := Injective.function with injective134  constructor135  . exact shiftMap.function with injective136  . intros x hx y hy z hz hxz hyz137    obtain ⟨hx2, hz2, caseX⟩ := shiftMap.relates.forward with hxz138    obtain ⟨hy2, hz3, caseY⟩ := shiftMap.relates.forward with hyz139    cases caseX with fixedX | movedX140    . cases caseY with fixedY | movedY141      . rw [← fixedX.right, ← fixedY.right]142        rfl143      . exfalso144        obtain ⟨m, hm, ym, zm⟩ := movedY145        apply fixedX.left146        rw [← fixedX.right, zm]147        have hsucc := omega.successor with hm148        exact shiftMap.in_image with function, hsucc149    . cases caseY with fixedY | movedY150      . exfalso151        obtain ⟨n, hn, xn, zn⟩ := movedX152        apply fixedY.left153        rw [← fixedY.right, zn]154        have hsucc := omega.successor with hn155        exact shiftMap.in_image with function, hsucc156      . obtain ⟨n, hn, xn, zn⟩ := movedX157        obtain ⟨m, hm, ym, zm⟩ := movedY158        have hsuccN := omega.successor with hn159        have hsuccM := omega.successor with hm160        have same : g(succ(n)) = g(succ(m)) by cc161        have equalSucc := Injective.apply_cancel with injective, hsuccN, hsuccM, same162        have equal := Naturals.injective.succ with equalSucc163        rw [xn, ym, equal]164        rfl165166theorem shiftMap.not_surjective (g A : Set)167  requires injective : InjectiveBetween(g, ℕ, A)168  shows ¬SurjectiveBetween(shiftMap(g, A), A, A)169proof170  have function := Injective.function with injective171  have zeroNat : Nat(0) by typecheck172  have hzero : 0 ∈ ℕ := nat.omega.forward with zeroNat173  have start := FunctionBetween.apply_closed with function, hzero174  intro surjective175  obtain ⟨x, hx, hit⟩ := surjective.right with g(0), start176  obtain ⟨hx2, hstart, rule⟩ := shiftMap.relates.forward with hit177  cases rule with fixed | moved178  . apply fixed.left179    rw ← fixed.right180    exact shiftMap.in_image with function, hzero181  . obtain ⟨n, hn, xn, shape⟩ := moved182    have hsucc := omega.successor with hn183    have equal := Injective.apply_cancel with injective, hzero, hsucc, shape184    exact Naturals.disjoint.zero.succ at n with equal185186theorem DedekindInfinite.of_omega_dominated (A : Set)187  requires dominated : ℕ ≼ A188  shows DedekindInfinite(A)189proof190  obtain ⟨g, injective⟩ := dominated191  refine ⟨shiftMap(g, A), shiftMap.injective with injective, shiftMap.not_surjective with injective⟩192193-- The orbit of a point under a self-map.194def orbit (f a : Set, n : Nat) → Set195  | f, a, zero => a196  | f, a, succ(k) => f(orbit(f, a, k))197198theorem orbit.zero (f a : Set)199  shows orbit(f, a, 0) = a200proof201  simp [orbit]202203theorem orbit.succ (f a : Set, k : Nat)204  shows orbit(f, a, succ(k)) = f(orbit(f, a, k))205proof206  simp [orbit]207208theorem orbit.closed (f A a : Set, n : Nat)209  requires function : f : A → A210  requires ha : a ∈ A211  shows orbit(f, a, n) ∈ A212proof213  induction n214  | zero =>215    rw orbit.zero216    exact ha217  | succ(k) using ih =>218    rw orbit.succ219    exact FunctionBetween.apply_closed with function, ih220221-- Starting outside the image of an injection, the orbit never repeats.222theorem orbit.distinct (f A a : Set, m : Nat)223  requires injective : InjectiveBetween(f, A, A)224  requires ha : a ∈ A225  requires outside : ¬a ∈ functionImage(f, A, A)226  shows ∀ n, Nat(n) → m < n → orbit(f, a, m) ≠ orbit(f, a, n)227proof228  induction m229  | zero =>230    have function := Injective.function with injective231    intros n hn below equal232    have shape := natural.zero_or_successor with hn233    cases shape with isZero | isSucc234    . rw isZero at below235      exact Less.irreflexive at 0 with below236    . obtain ⟨k, hk, nk⟩ := isSucc237      rw [nk, orbit.zero, orbit.succ] at equal238      apply outside239      rw equal240      have closed := orbit.closed at f, A, a, k with function, ha241      have value := FunctionBetween.apply_closed with function, closed242      simp [functionImage.membership]243  | succ(j) using ih =>244    have function := Injective.function with injective245    intros n hn below equal246    have shape := natural.zero_or_successor with hn247    cases shape with isZero | isSucc248    . rw isZero at below249      arith250    . obtain ⟨k, hk, nk⟩ := isSucc251      rw [nk, orbit.succ, orbit.succ] at equal252      rw nk at below253      have upper := Less.successor_upper with below254      have self := bootstrap.succ.self at j255      have selfLess := Less.of_membership at j, succ(j) with self256      have jk := Less.transitive_LessEqual with selfLess, upper257      have closedJ := orbit.closed at f, A, a, j with function, ha258      have closedK := orbit.closed at f, A, a, k with function, ha259      have same := Injective.apply_cancel with injective, closedJ, closedK, equal260      exact ih with k, hk, jk, same261262defgraph orbitMap (f A a : Set) (n ∈ ℕ) : A := orbit(f, a, n)263requires function : f : A → A264requires ha : a ∈ A265proof266  exact orbit.closed with function, ha267268theorem orbitMap.injective (f A a : Set)269  requires injective : InjectiveBetween(f, A, A)270  requires ha : a ∈ A271  requires outside : ¬a ∈ functionImage(f, A, A)272  shows InjectiveBetween(orbitMap(f, A, a), ℕ, A)273proof274  have function := Injective.function with injective275  have graph := orbitMap.function at f, A, a with *276  constructor277  . exact graph278  . intros m hm n hn z hz mappedM mappedN279    have valueM := FunctionBetween.apply_value with graph, hm, mappedM280    have valueN := FunctionBetween.apply_value with graph, hn, mappedN281    have stepM := orbitMap.value at f, A, a, m with *282    have stepN := orbitMap.value at f, A, a, n with *283    have equal : orbit(f, a, m) = orbit(f, a, n) by cc284    have mNat := nat.omega.backward with hm285    have nNat := nat.omega.backward with hn286    have alternatives := Less.trichotomy with mNat, nNat287    cases alternatives with mn | rest288    . exfalso289      have distinct := orbit.distinct at f, A, a, m with injective, ha, outside290      exact distinct with n, nNat, mn, equal291    . cases rest with same | nm292      . exact same293      . exfalso294        have distinct := orbit.distinct at f, A, a, n with injective, ha, outside295        apply distinct with m, mNat, nm296        symm297        exact equal298299theorem DedekindInfinite.omega_dominated (A : Set)300  requires dedekind : DedekindInfinite(A)301  shows ℕ ≼ A302proof303  obtain ⟨f, injective, notOnto⟩ := dedekind304  have function := Injective.function with injective305  have missed : ∃ a ∈ A, ¬a ∈ functionImage(f, A, A)306    by_contra none307    apply notOnto308    constructor309    . exact function310    . intros y hy311      have covered : y ∈ functionImage(f, A, A)312        by_contra absent313        apply none314        refine ⟨y, hy, absent⟩315      simp [functionImage.membership] at covered316      obtain ⟨hyA, x, hx, shape⟩ := covered317      refine ⟨x, hx, ?_⟩318      rw shape319      exact FunctionBetween.relates_apply with function, hx320  obtain ⟨a, ha, outside⟩ := missed321  witness orbitMap(f, A, a)322  exact orbitMap.injective with injective, ha, outside323324-- The three faces of infinity coincide.325theorem Infinite.iff_omega_dominated (A : Set)326  shows Infinite(A) ↔ ℕ ≼ A327proof328  constructor329  . intro infinite330    exact Infinite.omega_dominated with infinite331  . intro dominated332    unfold Infinite333    intro finite334    have omegaFinite := Finite.of_dominated with finite, dominated335    exact omega.infinite with omegaFinite336337theorem Infinite.iff_dedekind (A : Set)338  shows Infinite(A) ↔ DedekindInfinite(A)339proof340  constructor341  . intro infinite342    exact DedekindInfinite.of_omega_dominated with (Infinite.omega_dominated with infinite)343  . intro dedekind344    have dominated := DedekindInfinite.omega_dominated with dedekind345    exact Infinite.iff_omega_dominated.backward with dominated346