Grace/Cumulus/Cardinal/Dominance.g17

Open in Workbench Download source

Imports

Finite · ListSupport · Set

Declarations

Source

1-- Dominance between sets by injections, and the Cantor–Schröder–Bernstein2-- theorem: mutual injections yield a bijection3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Cardinal.Dominance9import Finite10import ListSupport11import Set1213-- A set is infinite when it is not finite, and Dedekind-infinite when it14-- injects into itself without covering itself.15predicate Infinite (A : Set) := ¬Finite(A)16predicate DedekindInfinite (A : Set) :=17  ∃ f, InjectiveBetween(f, A, A) ∧ ¬SurjectiveBetween(f, A, A)1819-- An injection is a bijection onto its image.20theorem Equipotent.image (f A B : Set)21  requires injective : InjectiveBetween(f, A, B)22  shows A ≃ functionImage(f, A, B)23proof24  witness f25  constructor26  . exact Injective.corestrict with injective27  . exact functionImage.surjective with (Injective.function with injective)2829predicate Dominated (A B : Set) := ∃ f, InjectiveBetween(f, A, B)30notation infix 50 "≼" => Dominated3132-- A set dominated by a finite set is finite.33theorem Finite.of_dominated (A B : Set)34  requires finite : Finite(B)35  requires dominated : A ≼ B36  shows Finite(A)37proof38  obtain ⟨f, injective⟩ := dominated39  have imageFinite := Finite.subset with finite, (functionImage.subset at f, A, B)40  have equipotent := Equipotent.image with injective41  exact Finite.of_equipotent with imageFinite, (Equipotent.symmetric with equipotent)4243theorem Dominated.of_injective (f A B : Set)44  requires h : InjectiveBetween(f, A, B)45  shows A ≼ B46proof47  witness f48  exact h4950theorem Dominated.reflexive (A : Set)51  shows A ≼ A52proof53  witness identity(A)54  exact identity.injective5556theorem Dominated.of_equipotent (A B : Set)57  requires h : A ≃ B58  shows A ≼ B59proof60  obtain ⟨f, hf⟩ := h61  witness f62  exact hf.left6364theorem Dominated.transitive (A B C : Set)65  requires hAB : A ≼ B66  requires hBC : B ≼ C67  shows A ≼ C68proof69  obtain ⟨f, hf⟩ := hAB70  obtain ⟨g, hg⟩ := hBC71  witness compose(g, f, A, B, C)72  exact compose.injective with hf, hg7374theorem Dominated.of_subset (A B : Set)75  requires h : A ⊆ B76  shows A ≼ B77proof78  witness identity(A)79  have function := identity.function at A80  have widened : identity(A) : A → B81    apply FunctionBetween.codomain_of_values with function82    intros x hx83    have fixed := identity.apply with hx84    rw fixed85    exact h with x, hx86  constructor87  . exact widened88  . intros x hx y hy z hz hxz hyz89    have valueX := FunctionBetween.apply_value with function, hx, hxz90    have valueY := FunctionBetween.apply_value with function, hy, hyz91    have fixedX := identity.apply with hx92    have fixedY := identity.apply with hy93    rw fixedX at valueX94    rw fixedY at valueY95    rw [valueX, valueY]96    rfl9798-- The back-and-forth chain. Stage zero holds the points of A outside the99-- image of g; each later stage is the image under g ∘ f of the one before.100101def chainStage (f g A B : Set, n : Nat) → Set102  | f, g, A, B, zero => A ∖ functionImage(g, B, A)103  | f, g, A, B, succ(k) => functionImage(g, functionImage(f, chainStage(f, g, A, B, k), B), A)104105def chainStages (f g A B : Set) : Set := { chainStage(f, g, A, B, n) | n ∈ ℕ }106107def chain (f g A B : Set) : Set := ⋃(chainStages(f, g, A, B))108109-- The bijection: f on the chain, the inverse of g off it.110def bernsteinMap (f g A B : Set) : Set :=111  restrict(f, chain(f, g, A, B)) ∪ restrict(converse(g, B, A), A ∖ chain(f, g, A, B))112113theorem chainStage.zero (f g A B : Set)114  shows chainStage(f, g, A, B, 0) = A ∖ functionImage(g, B, A)115proof116  simp [chainStage]117118theorem chainStage.succ (f g A B : Set, k : Nat)119  shows chainStage(f, g, A, B, succ(k)) = functionImage(g, functionImage(f, chainStage(f, g, A, B, k), B), A)120proof121  simp [chainStage]122123theorem chainStage.subset (f g A B : Set, n : Nat)124  shows chainStage(f, g, A, B, n) ⊆ A125proof126  induction n127  | zero =>128    rw chainStage.zero129    exact difference.subset_left at A, functionImage(g, B, A)130  | succ(k) using ih =>131    rw chainStage.succ132    exact functionImage.subset at g, functionImage(f, chainStage(f, g, A, B, k), B), A133134theorem chain.membership (f g A B x : Set)135  shows x ∈ chain(f, g, A, B) ↔ ∃ n ∈ ℕ, x ∈ chainStage(f, g, A, B, n)136proof137  constructor138  . intro h139    simp [chain, set.union] at h140    obtain ⟨S, hS, hx⟩ := h141    simp [chainStages] at hS142    obtain ⟨n, hn, shape⟩ := hS143    witness n144    constructor145    . exact hn146    . rw ← shape at hx147      exact hx148  . intro h149    obtain ⟨n, hn, hx⟩ := h150    have stageIn : chainStage(f, g, A, B, n) ∈ chainStages(f, g, A, B) by simp [chainStages]151    simp [chain]152    exact union.contains with stageIn, hx153154theorem chain.subset (f g A B : Set)155  shows chain(f, g, A, B) ⊆ A156proof157  intros x hx158  obtain ⟨n, hn, inStage⟩ := chain.membership.forward with hx159  exact chainStage.subset at f, g, A, B, n with x, inStage160161theorem chain.stage_zero (f g A B x : Set)162  requires hx : x ∈ A163  requires outside : ¬(x ∈ functionImage(g, B, A))164  shows x ∈ chain(f, g, A, B)165proof166  apply chain.membership.backward167  witness 0168  constructor169  . exact Naturals.constructor.zero170  . rw chainStage.zero171    simp [difference.membership]172173theorem chain.closed (f g A B x : Set)174  requires fFunction : f : A → B175  requires gFunction : g : B → A176  requires hx : x ∈ chain(f, g, A, B)177  shows g(f(x)) ∈ chain(f, g, A, B)178proof179  obtain ⟨n, hn, inStage⟩ := chain.membership.forward with hx180  apply chain.membership.backward181  witness succ(n)182  constructor183  . exact Naturals.constructor.succ at n with hn184  . rw chainStage.succ185    have hxA : x ∈ A := chainStage.subset at f, g, A, B, n with x, inStage186    have valueB := FunctionBetween.apply_closed with fFunction, hxA187    have inImage : f(x) ∈ functionImage(f, chainStage(f, g, A, B, n), B) by simp [functionImage.membership]188    have valueA := FunctionBetween.apply_closed with gFunction, valueB189    simp [functionImage.membership]190    exact ⟨valueA, f(x), inImage, rfl⟩191192theorem chain.off_in_image (f g A B x : Set)193  requires hx : x ∈ A194  requires outside : ¬(x ∈ chain(f, g, A, B))195  shows x ∈ functionImage(g, B, A)196proof197  by_contra absent198  exact outside with (chain.stage_zero with hx, absent)199200-- A point of the chain that g reaches is reached from a point of the chain201-- through f.202theorem chain.preimage (f g A B y : Set)203  requires fFunction : f : A → B204  requires gInjective : InjectiveBetween(g, B, A)205  requires hy : y ∈ B206  requires inChain : g(y) ∈ chain(f, g, A, B)207  shows ∃ x ∈ chain(f, g, A, B), f(x) = y208proof209  have gFunction := gInjective.left210  obtain ⟨n, hn, inStage⟩ := chain.membership.forward with inChain211  have valueA := FunctionBetween.apply_closed with gFunction, hy212  have inImage : g(y) ∈ functionImage(g, B, A) by simp [functionImage.membership]213  have cases := natural.zero_or_successor at n214  cases cases with zero | successor215  . exfalso216    rw [zero, chainStage.zero] at inStage217    simp [difference.membership] at inStage218  . obtain ⟨k, hk, shape⟩ := successor219    rw [shape, chainStage.succ] at inStage220    simp [functionImage.membership] at inStage221    obtain ⟨inA, z, hz, equation⟩ := inStage222    simp [functionImage.membership] at hz223    obtain ⟨inB, x, hx, shapeZ⟩ := hz224    have hxA : x ∈ A := chainStage.subset at f, g, A, B, k with x, hx225    have same : y = z := Injective.apply_cancel with gInjective, hy, inB, equation226    witness x227    constructor228    . exact chain.membership.backward with ⟨k, hk, hx⟩229    . rw [same, shapeZ]230      rfl231232-- The map relates x to y exactly when either x lies on the chain and f233-- carries x to y, or x lies off the chain and g carries y to x.234theorem bernsteinMap.relates (f g A B x y : Set)235  shows relates(bernsteinMap(f, g, A, B), x, y) ↔236    (x ∈ chain(f, g, A, B) ∧ relates(f, x, y)) ∨237    (x ∈ A ∧ ¬(x ∈ chain(f, g, A, B)) ∧ y ∈ B ∧ relates(g, y, x))238proof239  constructor240  . intro h241    have member : (x, y) ∈ bernsteinMap(f, g, A, B) := h242    simp [bernsteinMap, union2.membership] at member243    cases member with onChain | offChain244    . left245      exact restrict.relates.forward at f, chain(f, g, A, B), x, y with onChain246    . right247      obtain ⟨inDifference, flipped⟩ := restrict.relates.forward at converse(g, B, A), A ∖ chain(f, g, A, B), x, y with offChain248      simp [difference.membership] at inDifference249      obtain ⟨hxA, outside⟩ := inDifference250      have flippedMember : (x, y) ∈ converse(g, B, A) := flipped251      simp [converse.membership] at flippedMember252      obtain ⟨bound, b, hb, a, ha, equation, back⟩ := flippedMember253      have coordinates := orderedPair.injective with equation254      rw [coordinates.left, coordinates.right]255      rw coordinates.left at outside256      exact ⟨ha, outside, hb, back⟩257  . intro h258    cases h with onChain | offChain259    . have related := restrict.relates.backward with onChain260      have member : (x, y) ∈ restrict(f, chain(f, g, A, B)) := related261      have inUnion : (x, y) ∈ bernsteinMap(f, g, A, B) by simp [bernsteinMap, union2.membership, member]262      exact inUnion263    . obtain ⟨hxA, outside, hyB, back⟩ := offChain264      have flipped := converse.relates with hyB, hxA, back265      have inDifference : x ∈ A ∖ chain(f, g, A, B) by simp [difference.membership, hxA, outside]266      have related := restrict.relates.backward at converse(g, B, A), A ∖ chain(f, g, A, B), x, y with ⟨inDifference, flipped⟩267      have member : (x, y) ∈ restrict(converse(g, B, A), A ∖ chain(f, g, A, B)) := related268      have inUnion : (x, y) ∈ bernsteinMap(f, g, A, B) by simp [bernsteinMap, union2.membership, member]269      exact inUnion270271theorem bernsteinMap.function (f g A B : Set)272  requires fFunction : f : A → B273  requires gInjective : InjectiveBetween(g, B, A)274  shows bernsteinMap(f, g, A, B) : A → B275proof276  have gFunction := gInjective.left277  constructor278  . intros p hp279    simp [bernsteinMap, union2.membership] at hp280    cases hp with onChain | offChain281    . have inF := restrict.subset at f, chain(f, g, A, B) with p, onChain282      have included : f ⊆ A × B := fFunction.left283      exact included with p, inF284    . have inConverse := restrict.subset at converse(g, B, A), A ∖ chain(f, g, A, B) with p, offChain285      have included : converse(g, B, A) ⊆ A × B := converse.relation at g, B, A286      exact included with p, inConverse287  . constructor288    . intros x y hxy z hxz289      have first := bernsteinMap.relates.forward with hxy290      have second := bernsteinMap.relates.forward with hxz291      cases first with onChain | offChain292      . cases second with onChain2 | offChain2293        . exact Functional.unique with fFunction.right.left, onChain.right, onChain2.right294        . exfalso295          exact offChain2.right.left with onChain.left296      . cases second with onChain2 | offChain2297        . exfalso298          exact offChain.right.left with onChain2.left299        . have valueY := FunctionBetween.apply_value with gFunction, offChain.right.right.left, offChain.right.right.right300          have valueZ := FunctionBetween.apply_value with gFunction, offChain2.right.right.left, offChain2.right.right.right301          apply Injective.apply_cancel with gInjective, offChain.right.right.left, offChain2.right.right.left302          rw [valueY, valueZ]303          rfl304    . intros x hx305      have split : x ∈ chain(f, g, A, B) ∨ ¬(x ∈ chain(f, g, A, B)) by tauto306      cases split with onChain | offChain307      . witness f(x)308        constructor309        . exact FunctionBetween.apply_closed with fFunction, hx310        . apply bernsteinMap.relates.backward311          left312          constructor313          . exact onChain314          . exact FunctionBetween.relates_apply with fFunction, hx315      . have inImage := chain.off_in_image with hx, offChain316        simp [functionImage.membership] at inImage317        obtain ⟨inA, y, hy, shape⟩ := inImage318        witness y319        constructor320        . exact hy321        . apply bernsteinMap.relates.backward322          right323          have back := FunctionBetween.relates_apply with gFunction, hy324          rw ← shape at back325          exact ⟨hx, offChain, hy, back⟩326327theorem bernsteinMap.injective (f g A B : Set)328  requires fInjective : InjectiveBetween(f, A, B)329  requires gInjective : InjectiveBetween(g, B, A)330  shows InjectiveBetween(bernsteinMap(f, g, A, B), A, B)331proof332  have fFunction := fInjective.left333  have gFunction := gInjective.left334  constructor335  . exact bernsteinMap.function with fFunction, gInjective336  . intros x hx y hy z hz hxz hyz337    have first := bernsteinMap.relates.forward with hxz338    have second := bernsteinMap.relates.forward with hyz339    cases first with onChain | offChain340    . cases second with onChain2 | offChain2341      . exact Injective.cancel with fInjective, hx, hy, hz, onChain.right, onChain2.right342      . exfalso343        have valueZ := FunctionBetween.apply_value with fFunction, hx, onChain.right344        have valueY := FunctionBetween.apply_value with gFunction, hz, offChain2.right.right.right345        have closed := chain.closed with fFunction, gFunction, onChain.left346        rw [valueZ, valueY] at closed347        exact offChain2.right.left with closed348    . cases second with onChain2 | offChain2349      . exfalso350        have valueZ := FunctionBetween.apply_value with fFunction, hy, onChain2.right351        have valueX := FunctionBetween.apply_value with gFunction, hz, offChain.right.right.right352        have closed := chain.closed with fFunction, gFunction, onChain2.left353        rw [valueZ, valueX] at closed354        exact offChain.right.left with closed355      . exact Functional.unique with gFunction.right.left, offChain.right.right.right, offChain2.right.right.right356357theorem bernsteinMap.surjective (f g A B : Set)358  requires fInjective : InjectiveBetween(f, A, B)359  requires gInjective : InjectiveBetween(g, B, A)360  shows SurjectiveBetween(bernsteinMap(f, g, A, B), A, B)361proof362  have fFunction := fInjective.left363  have gFunction := gInjective.left364  constructor365  . exact bernsteinMap.function with fFunction, gInjective366  . intros y hy367    have valueA := FunctionBetween.apply_closed with gFunction, hy368    have split : g(y) ∈ chain(f, g, A, B) ∨ ¬(g(y) ∈ chain(f, g, A, B)) by tauto369    cases split with onChain | offChain370    . obtain ⟨x, hx, shape⟩ := chain.preimage with fFunction, gInjective, hy, onChain371      have hxA : x ∈ A := chain.subset at f, g, A, B with x, hx372      witness x373      constructor374      . exact hxA375      . apply bernsteinMap.relates.backward376        left377        constructor378        . exact hx379        . have related := FunctionBetween.relates_apply with fFunction, hxA380          rwa shape at related381    . witness g(y)382      constructor383      . exact valueA384      . apply bernsteinMap.relates.backward385        right386        exact ⟨valueA, offChain, hy, (FunctionBetween.relates_apply with gFunction, hy)⟩387388-- Cantor–Schröder–Bernstein: mutual injections give a bijection.389theorem Equipotent.of_mutual_dominance (A B : Set)390  requires hAB : A ≼ B391  requires hBA : B ≼ A392  shows A ≃ B393proof394  obtain ⟨f, hf⟩ := hAB395  obtain ⟨g, hg⟩ := hBA396  witness bernsteinMap(f, g, A, B)397  constructor398  . exact bernsteinMap.injective with hf, hg399  . exact bernsteinMap.surjective with hf, hg400401theorem Dominated.antisymmetric (A B : Set)402  requires hAB : A ≼ B403  requires hBA : B ≼ A404  shows A ≃ B405proof406  exact Equipotent.of_mutual_dominance with hAB, hBA407408-- Cantor: the power set strictly dominates.409410defgraph singletonMap (A : Set) (x ∈ A) : 𝒫(A) := {x}411proof412  apply powerset.membership_iff.backward413  exact singleton.subset_iff.backward with member414415theorem singletonMap.injective (A : Set)416  shows InjectiveBetween(singletonMap(A), A, 𝒫(A))417proof418  have function := singletonMap.function at A419  constructor420  . exact function421  . intros x hx y hy z hz hxz hyz422    have valueX := FunctionBetween.apply_value with function, hx, hxz423    have valueY := FunctionBetween.apply_value with function, hy, hyz424    have shownX := singletonMap.value with hx425    have shownY := singletonMap.value with hy426    rw shownX at valueX427    rw shownY at valueY428    apply singleton.injective429    rw [valueX, valueY]430    rfl431432theorem Dominated.powerset (A : Set)433  shows A ≼ 𝒫(A)434proof435  witness singletonMap(A)436  exact singletonMap.injective437438-- The points of A that g sends outside their own preimage set.439def cantorDiagonalOf (g A : Set) : Set := { x ∈ A | ∃ X ∈ 𝒫(A), g(X) = x ∧ ¬(x ∈ X) }440441theorem Cantor.powerset_not_dominated (A : Set)442  shows ¬(𝒫(A) ≼ A)443proof444  intro h445  obtain ⟨g, injective⟩ := h446  have function := injective.left447  have diagonalIn : cantorDiagonalOf(g, A) ∈ 𝒫(A)448    apply powerset.membership_iff.backward449    intros x hx450    simp [cantorDiagonalOf.membership] at hx451    exact hx.left452  have valueA := FunctionBetween.apply_closed with function, diagonalIn453  have split : g(cantorDiagonalOf(g, A)) ∈ cantorDiagonalOf(g, A) ∨ ¬(g(cantorDiagonalOf(g, A)) ∈ cantorDiagonalOf(g, A)) by tauto454  cases split with inside | outside455  . have member := cantorDiagonalOf.membership.forward with inside456    obtain ⟨inA, X, hX, equation, absent⟩ := member457    have same : X = cantorDiagonalOf(g, A) := Injective.apply_cancel with injective, hX, diagonalIn, equation458    rw same at absent459    exact absent with inside460  . apply outside461    apply cantorDiagonalOf.membership.backward462    constructor463    . exact valueA464    . witness cantorDiagonalOf(g, A)465      constructor466      . exact diagonalIn467      . constructor468        . rfl469        . exact outside470