Grace/Cumulus/Algebra/Group/Paradox/SchroederBernstein.g17

Open in Workbench Download source

Imports

Algebra.Group.Paradox.PieceMaps · Cardinal.Dominance

Declarations

Source

1-- The Banach–Schröder–Bernstein theorem for equidecomposability: a set2-- equidecomposable with a subset of a second set, which is in turn3-- equidecomposable with a subset of the first, is equidecomposable with4-- the second. Equidecomposability is realised by a piecewise-moved5-- bijection and conversely; the back-and-forth chain of the6-- Cantor–Schröder–Bernstein construction splits both sets into two7-- parts, each decomposed onto its image by restricting a piece map8-- Part of Cumulus, the Grace17 mathematics library.9-- Copyright (c) 2026 Grant Passmore.10-- Released under the Apache License 2.0. See LICENSE in the repository root.11-- Authors: Grant Passmore1213module Grace.Cumulus.Algebra.Group.Paradox.SchroederBernstein14import Algebra.Group.Paradox.PieceMaps15import Cardinal.Dominance1617-- A embeds in B when A is equidecomposable with a subset of B.18predicate Embeds (act G X A B : Set) :=19  ∃ C, C ⊆ B ∧ Equidecomposable(act, G, X, A, C)2021-- f moves A piecewise: finitely many disjoint pieces cover A, and on each22-- piece f agrees with one group element.23predicate PiecewiseMoved (act G X A f : Set) :=24  ∃ F, Finite(F) ∧ F ⊆ 𝒫(X) × Group.carrier(G) ∧ Pieces(A, F) ∧25    (∀ p ∈ F, ∀ x ∈ fst(p), f(x) = act(snd(p), x))2627-- The complement of the chain is the image under g of the complement of28-- the image of the chain under f.29theorem chain.complement (f g A B : Set)30  requires fFunction : f : A → B31  requires gInjective : InjectiveBetween(g, B, A)32  shows functionImage(g, B ∖ functionImage(f, chain(f, g, A, B), B), A) =33    A ∖ chain(f, g, A, B)34proof35  have gFunction := Injective.function with gInjective36  ext x37  constructor38  . intro hx39    obtain ⟨xIn, y, hy, xEq⟩ := functionImage.membership.forward with hx40    obtain ⟨yIn, outside⟩ := difference.membership.forward with hy41    apply difference.membership.backward42    refine ⟨xIn, ?_⟩43    intro inChain44    rw xEq at inChain45    obtain ⟨z, hz, zEq⟩ :=46      chain.preimage with fFunction, gInjective, yIn, inChain47    apply outside48    have zIn : z ∈ A := chain.subset at f, g, A, B with z, hz49    have inB := FunctionBetween.apply_closed with fFunction, zIn50    rw zEq at inB51    symm at zEq52    exact functionImage.membership.backward with ⟨inB, z, hz, zEq⟩53  . intro hx54    obtain ⟨xIn, outside⟩ := difference.membership.forward with hx55    have inImage := chain.off_in_image with xIn, outside56    obtain ⟨xIn2, y, hy, xEq⟩ := functionImage.membership.forward with inImage57    apply functionImage.membership.backward58    refine ⟨xIn, y, ?_, xEq⟩59    apply difference.membership.backward60    refine ⟨hy, ?_⟩61    intro inImageF62    obtain ⟨yIn, z, hz, yEq⟩ := functionImage.membership.forward with inImageF63    have closed := chain.closed with fFunction, gFunction, hz64    rw [← yEq, ← xEq] at closed65    exact outside with closed6667section SchroederBernstein68variable (act G X : Set)69hypothesis action : act : G ↷ X7071theorem Embeds.of_subset (A B : Set)72  requires bounded : A ⊆ X73  requires subset : A ⊆ B74  shows Embeds(act, G, X, A, B)75proof76  have same := Equidecomposable.reflexive with action, bounded77  witness A78  exact ⟨subset, same⟩7980theorem Embeds.of_equidecomposable (A B C : Set)81  requires subset : C ⊆ B82  requires equidecomposable : Equidecomposable(act, G, X, A, C)83  shows Embeds(act, G, X, A, B)84proof85  witness C86  exact ⟨subset, equidecomposable⟩8788-- Equidecomposability is realised by a piecewise-moved bijection.89theorem Equidecomposable.bijection (A B : Set)90  requires equidecomposable : Equidecomposable(act, G, X, A, B)91  shows ∃ f, BijectiveBetween(f, A, B) ∧ PiecewiseMoved(act, G, X, A, f)92proof93  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable94  have bijective := pieceMap.bijective with action, bounded, pieces, movedPieces95  witness pieceMap(act, X, F)96  constructor97  . exact bijective98  . witness F99    refine ⟨finite, bounded, pieces, ?_⟩100    intros p hp x hx101    exact pieceMap.apply with action, bounded, pieces, hp, hx102103-- Conversely, a piecewise-moved bijection onto B decomposes A onto B.104theorem Equidecomposable.of_bijection (A B f : Set)105  requires bijective : BijectiveBetween(f, A, B)106  requires piecewise : PiecewiseMoved(act, G, X, A, f)107  shows Equidecomposable(act, G, X, A, B)108proof109  obtain ⟨injective, surjective⟩ := bijective110  have function := Injective.function with injective111  obtain ⟨F, finite, bounded, pieces, values⟩ := piecewise112  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces113  have moves : ∀ p ∈ F, moved(act, X, p) = functionImage(f, fst(p), B)114    intros p hp115    obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)116    rw moved.unfold117    ext y118    constructor119    . intro hy120      obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with hy121      have value := values with p, hp, x, hx122      have xIn := piecesBounded with p, hp, x, hx123      have inB := FunctionBetween.apply_closed with function, xIn124      rw ← value at yEq125      rw yEq126      exact functionImage.membership.backward with ⟨inB, x, hx, rfl⟩127    . intro hy128      obtain ⟨inB, x, hx, yEq⟩ := functionImage.membership.forward with hy129      have value := values with p, hp, x, hx130      have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p)) :=131        translate.act_mem with action, subset, hx132      rw [yEq, value]133      exact member134  witness F135  refine ⟨finite, bounded, pieces, ?_⟩136  refine ⟨?_, ?_, ?_⟩137  . intros p hp138    have move := moves with p, hp139    rw move140    exact functionImage.subset at f, fst(p), B141  . intros y hy142    obtain ⟨x, hx, related⟩ := surjective.right with y, hy143    have value := FunctionBetween.apply_value with function, hx, related144    obtain ⟨p, hp, inP⟩ := piecesCover with x, hx145    have move := moves with p, hp146    symm at value147    have member : y ∈ functionImage(f, fst(p), B) :=148      functionImage.membership.backward with ⟨hy, x, inP, value⟩149    witness p150    rw move151    exact ⟨hp, member⟩152  . intros p hp q hq different153    have moveP := moves with p, hp154    have moveQ := moves with q, hq155    rw [moveP, moveQ]156    apply Disjoint.iff.backward157    intros y hyP hyQ158    obtain ⟨inB, x, hx, yEqX⟩ := functionImage.membership.forward with hyP159    obtain ⟨inB2, x2, hx2, yEqX2⟩ := functionImage.membership.forward with hyQ160    have xIn := piecesBounded with p, hp, x, hx161    have x2In := piecesBounded with q, hq, x2, hx2162    have same : f(x) = f(x2) by cc163    have equal := Injective.apply_cancel with injective, xIn, x2In, same164    rw ← equal at hx2165    have disjoint := piecesDisjoint with p, hp, q, hq, different166    have absent := Disjoint.iff.forward with disjoint167    exact absent with x, hx, hx2168169-- The Schröder–Bernstein engine: injections f : A → B and g : B → A that170-- decompose every subset onto its image decompose A onto B, by splitting171-- A at the chain and B at the image of the chain.172theorem Equidecomposable.of_injections (A B f g : Set)173  requires fFunction : f : A → B174  requires gInjective : InjectiveBetween(g, B, A)175  requires first : ∀ C, C ⊆ A →176    Equidecomposable(act, G, X, C, functionImage(f, C, B))177  requires second : ∀ D, D ⊆ B →178    Equidecomposable(act, G, X, D, functionImage(g, D, A))179  shows Equidecomposable(act, G, X, A, B)180proof181  have chainSubset := chain.subset at f, g, A, B182  have imageSubset := functionImage.subset at f, chain(f, g, A, B), B183  have restSubset :=184    difference.subset_left at B, functionImage(f, chain(f, g, A, B), B)185  have firstPart := first with chain(f, g, A, B), chainSubset186  have secondPart :=187    second with B ∖ functionImage(f, chain(f, g, A, B), B), restSubset188  have complement := chain.complement with fFunction, gInjective189  rw complement at secondPart190  have backPart := Equidecomposable.symmetric with action, secondPart191  have disjointSource := Disjoint.difference_right at A, chain(f, g, A, B)192  have disjointTarget :=193    Disjoint.difference_right at B, functionImage(f, chain(f, g, A, B), B)194  have union := Equidecomposable.disjoint_union with action, firstPart,195    backPart, disjointSource, disjointTarget196  have coverA := difference.union2_of_subset with chainSubset197  have coverB := difference.union2_of_subset with imageSubset198  rw [coverA, coverB] at union199  exact union200201-- The Banach–Schröder–Bernstein theorem.202theorem Equidecomposable.of_embeddings (A B : Set)203  requires boundedA : A ⊆ X204  requires boundedB : B ⊆ X205  requires forward : Embeds(act, G, X, A, B)206  requires backward : Embeds(act, G, X, B, A)207  shows Equidecomposable(act, G, X, A, B)208proof209  obtain ⟨B1, subsetB1, firstPieces⟩ := forward210  obtain ⟨A1, subsetA1, secondPieces⟩ := backward211  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := firstPieces212  obtain ⟨F2, finite2, bounded2, pieces2, movedPieces2⟩ := secondPieces213  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces214  obtain ⟨movedBounded2, movedCover2, movedDisjoint2⟩ := movedPieces2215  have movedB : ∀ p ∈ F, moved(act, X, p) ⊆ B216    intros p hp217    exact Subset.transitive with (movedBounded with p, hp), subsetB1218  have movedA : ∀ p ∈ F2, moved(act, X, p) ⊆ A219    intros p hp220    exact Subset.transitive with (movedBounded2 with p, hp), subsetA1221  have fInjective := pieceMap.injective with action, bounded, pieces, movedB,222    movedDisjoint223  have gInjective := pieceMap.injective with action, bounded2, pieces2, movedA,224    movedDisjoint2225  have fFunction := Injective.function with fInjective226  have first : ∀ C, C ⊆ A →227      Equidecomposable(act, G, X, C, functionImage(pieceMap(act, X, F), C, B))228    intros C hC229    exact Equidecomposable.restrict with action, finite, bounded, pieces,230      movedB, movedDisjoint, hC231  have second : ∀ D, D ⊆ B →232      Equidecomposable(act, G, X, D, functionImage(pieceMap(act, X, F2), D, A))233    intros D hD234    exact Equidecomposable.restrict with action, finite2, bounded2, pieces2,235      movedA, movedDisjoint2, hD236  exact Equidecomposable.of_injections with action, fFunction, gInjective,237    first, second238239end SchroederBernstein240