Equidecomposability of sets

Let G act on X. Two sets A B : Set X are equidecomposable, TauCeti.Equidecomposable G A B, when some Equidecomp X G (a partial bijection that moves each point of its source by one of finitely many elements of G) has source A and target B. Equivalently, A can be cut into finitely many pieces which, each moved by a single element of G, reassemble into B. The set A is equidecomposable with a subset of B, TauCeti.EquidecomposableLE G A B, when it is equidecomposable with some B' ⊆ B.

This file shows that equidecomposability is an equivalence relation stable under restriction to subsets, finite disjoint unions, single translations, equivariant bijections and changes of the acting group that do not change the action, and that EquidecomposableLE G is a preorder. The main result is the Schröder–Bernstein theorem for equidecompositions (EquidecomposableLE.antisymm): if each of A and B is equidecomposable with a subset of the other, then A and B are equidecomposable. It follows from Mathlib's Schröder–Bernstein theorem for injections preserving a relation (Function.Embedding.schroeder_bernstein_of_rel), so the resulting equidecomposition uses only the finitely many group elements of the first given equidecomposition together with the inverses of those of the second. These are the basic tools for paradoxical decompositions, for instance in Tarski's characterization of amenable groups.

Main definitions

• Equidecomp.disjointUnion: the union of two equidecompositions with disjoint sources and disjoint targets.
• TauCeti.Equidecomposable G A B: A and B are equidecomposable using G.
• TauCeti.EquidecomposableLE G A B: A is equidecomposable with a subset of B.

Main results

• TauCeti.Equidecomposable.equivalence: equidecomposability is an equivalence relation.
• Equidecomp.IsDecompOn.equidecomposable_image: a map injective on A that moves each point of A by one of finitely many group elements makes A equidecomposable with its image.
• TauCeti.Equidecomposable.biUnion_finset: finite disjoint unions of equidecomposable families are equidecomposable.
• TauCeti.Equidecomposable.exists_subset_and_sdiff: restricting an equidecomposition to a subset A' ⊆ A splits both A' ∼ B' and A \ A' ∼ B \ B' off it.
• TauCeti.EquidecomposableLE.antisymm: the Schröder–Bernstein theorem for equidecompositions.
• TauCeti.equidecomposable_iff_equidecomposableLE: equidecomposability is the equivalence relation induced by the preorder EquidecomposableLE G.

References

• G. Tomkowicz, S. Wagon, The Banach–Tarski Paradox, 2nd ed., Chapter 3, for the Banach–Schröder–Bernstein theorem and its proof.
• A. Garrido, An introduction to amenable groups, §1.

def Equidecomp.disjointUnion {X : Type u_1} {G : Type u_3} [SMul G X] (f f' : Equidecomp X G) (hs : Disjoint f.source f'.source) (ht : Disjoint f.target f'.target) [(x : X) → Decidable (x ∈ f.source)] [(y : X) → Decidable (y ∈ f.target)] : Equidecomp X G

The union of two equidecompositions with disjoint sources and disjoint targets: it acts as f on f.source and as f' on f'.source.

@[simp]

theorem Equidecomp.disjointUnion_toPartialEquiv {X : Type u_1} {G : Type u_3} [SMul G X] (f f' : Equidecomp X G) (hs : Disjoint f.source f'.source) (ht : Disjoint f.target f'.target) [(x : X) → Decidable (x ∈ f.source)] [(y : X) → Decidable (y ∈ f.target)] : (f.disjointUnion f' hs ht).toPartialEquiv = f.disjointUnion f'.toPartialEquiv hs ht

theorem Equidecomp.coe_disjointUnion {X : Type u_1} {G : Type u_3} [SMul G X] (f f' : Equidecomp X G) (hs : Disjoint f.source f'.source) (ht : Disjoint f.target f'.target) [(x : X) → Decidable (x ∈ f.source)] [(y : X) → Decidable (y ∈ f.target)] : ↑(f.disjointUnion f' hs ht).toPartialEquiv = f.source.piecewise ↑f.toPartialEquiv ↑f'.toPartialEquiv

The union of two equidecompositions acts as the first on its source and as the second elsewhere.

theorem Equidecomp.target_restr {X : Type u_1} {G : Type u_3} [SMul G X] (f : Equidecomp X G) {A : Set X} (hA : A ⊆ f.source) : (f.restr A).target = ↑f.toPartialEquiv '' A

The target of the restriction of an equidecomposition to a subset of its source is the image of that subset.

def TauCeti.Equidecomposable {X : Type u_1} (G : Type u_3) [SMul G X] (A B : Set X) : Prop

Two sets A B : Set X are equidecomposable using G when some equidecomposition has source A and target B: A can be cut into finitely many pieces which, each moved by a single element of G, reassemble into B.

def TauCeti.EquidecomposableLE {X : Type u_1} (G : Type u_3) [SMul G X] (A B : Set X) : Prop

A set A is equidecomposable with a subset of B using G. For a monoid action this is a preorder, and for a group action its induced equivalence relation is Equidecomposable G (equidecomposable_iff_equidecomposableLE).

theorem TauCeti.equidecomposable_iff {X : Type u_1} {G : Type u_3} [SMul G X] {A B : Set X} : Equidecomposable G A B ↔ ∃ (f : Equidecomp X G), f.source = A ∧ f.target = B

Unfolds Equidecomposable: some equidecomposition has source A and target B.

theorem TauCeti.equidecomposableLE_iff {X : Type u_1} {G : Type u_3} [SMul G X] {A B : Set X} : EquidecomposableLE G A B ↔ ∃ B' ⊆ B, Equidecomposable G A B'

Unfolds EquidecomposableLE: A is equidecomposable with some subset of B.

theorem Equidecomp.equidecomposable {X : Type u_1} {G : Type u_3} [SMul G X] (f : Equidecomp X G) : TauCeti.Equidecomposable G f.source f.target

The source and target of an equidecomposition are equidecomposable.

theorem Equidecomp.equidecomposable_image {X : Type u_1} {G : Type u_3} [SMul G X] {A : Set X} (f : Equidecomp X G) (hA : A ⊆ f.source) : TauCeti.Equidecomposable G A (↑f.toPartialEquiv '' A)

A subset of the source of an equidecomposition is equidecomposable with its image.

@[simp]

theorem TauCeti.equidecomposable_empty {X : Type u_1} {G : Type u_3} [SMul G X] : Equidecomposable G ∅ ∅

The empty set is equidecomposable with itself.

theorem Equidecomp.IsDecompOn.equidecomposable_image {X : Type u_1} {G : Type u_3} [SMul G X] {A : Set X} {f : X → X} {S : Finset G} (hfS : IsDecompOn f A S) (hf : Set.InjOn f A) : TauCeti.Equidecomposable G A (f '' A)

A map that is injective on A and moves each point of A by one of finitely many elements of G makes A equidecomposable with its image.

theorem TauCeti.Equidecomposable.nonempty_iff {X : Type u_1} {G : Type u_3} [SMul G X] {A B : Set X} (h : Equidecomposable G A B) : A.Nonempty ↔ B.Nonempty

Equidecomposable sets are simultaneously empty or nonempty.

theorem TauCeti.Equidecomposable.exists_subset_and_sdiff {X : Type u_1} {G : Type u_3} [SMul G X] {A A' B : Set X} (h : Equidecomposable G A B) (hA' : A' ⊆ A) : ∃ B' ⊆ B, Equidecomposable G A' B' ∧ Equidecomposable G (A \ A') (B \ B')

Restricting an equidecomposition of A with B to A' ⊆ A makes A' equidecomposable with some B' ⊆ B, and the remaining pieces A \ A' and B \ B' equidecomposable too.

theorem TauCeti.Equidecomposable.equidecomposableLE_of_subset {X : Type u_1} {G : Type u_3} [SMul G X] {A A' B : Set X} (h : Equidecomposable G A B) (hA' : A' ⊆ A) : EquidecomposableLE G A' B

A subset of a set equidecomposable with B is equidecomposable with a subset of B.

theorem TauCeti.Equidecomposable.equidecomposableLE {X : Type u_1} {G : Type u_3} [SMul G X] {A B : Set X} (h : Equidecomposable G A B) : EquidecomposableLE G A B

If A is equidecomposable with B, then A is equidecomposable with a subset of B.

theorem TauCeti.Equidecomposable.union {X : Type u_1} {G : Type u_3} [SMul G X] {A₁ A₂ B₁ B₂ : Set X} (h₁ : Equidecomposable G A₁ B₁) (h₂ : Equidecomposable G A₂ B₂) (hA : Disjoint A₁ A₂) (hB : Disjoint B₁ B₂) : Equidecomposable G (A₁ ∪ A₂) (B₁ ∪ B₂)

Unions of equidecomposable pairs with disjoint sources and disjoint targets are equidecomposable.

theorem TauCeti.Equidecomposable.biUnion_finset {X : Type u_1} {G : Type u_3} [SMul G X] {ι : Type u_5} {s : Finset ι} {A B : ι → Set X} (h : ∀ i ∈ s, Equidecomposable G (A i) (B i)) (hA : (↑s).PairwiseDisjoint A) (hB : (↑s).PairwiseDisjoint B) : Equidecomposable G (⋃ i ∈ s, A i) (⋃ i ∈ s, B i)

Finite unions of pairwise disjoint families, termwise equidecomposable, are equidecomposable.

theorem TauCeti.Equidecomposable.of_smul_eq {X : Type u_1} {G : Type u_3} {H : Type u_4} [SMul G X] {A B : Set X} [SMul H X] (φ : G → H) (hφ : ∀ (g : G) (x : X), φ g • x = g • x) (h : Equidecomposable G A B) : Equidecomposable H A B

An equidecomposition using G is one using H when each element of G acts as some element of H does.

theorem TauCeti.equidecomposable_iff_of_surjective {X : Type u_1} {G : Type u_3} {H : Type u_4} [SMul G X] {A B : Set X} [SMul H X] {φ : G → H} (hφs : Function.Surjective φ) (hφ : ∀ (g : G) (x : X), φ g • x = g • x) : Equidecomposable G A B ↔ Equidecomposable H A B

Equidecomposability does not depend on the acting group, only on the transformations through which it acts: a surjection φ : G → H with φ g • x = g • x identifies equidecomposability using G and using H. This applies in particular to a group isomorphism.

theorem TauCeti.Equidecomposable.image_equiv {X : Type u_1} {Y : Type u_2} {G : Type u_3} [SMul G X] {A B : Set X} [SMul G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) (h : Equidecomposable G A B) : Equidecomposable G (⇑e '' A) (⇑e '' B)

An equivariant bijection e : X ≃ Y carries equidecomposable sets to equidecomposable sets.

theorem TauCeti.equidecomposable_image_equiv_iff {X : Type u_1} {Y : Type u_2} {G : Type u_3} [SMul G X] {A B : Set X} [SMul G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) : Equidecomposable G (⇑e '' A) (⇑e '' B) ↔ Equidecomposable G A B

Equidecomposability is invariant under equivariant bijections.

@[simp]

theorem TauCeti.Equidecomposable.refl {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] (A : Set X) : Equidecomposable G A A

Every set is equidecomposable with itself.

theorem TauCeti.Equidecomposable.trans {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] {A B C : Set X} (h₁ : Equidecomposable G A B) (h₂ : Equidecomposable G B C) : Equidecomposable G A C

Equidecomposability is transitive.

theorem TauCeti.equidecomposableLE_of_subset {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] {A B : Set X} (h : A ⊆ B) : EquidecomposableLE G A B

A subset of B is equidecomposable with a subset of B.

@[simp]

theorem TauCeti.EquidecomposableLE.refl {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] (A : Set X) : EquidecomposableLE G A A

Every set is equidecomposable with a subset of itself.

theorem TauCeti.EquidecomposableLE.trans {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] {A B C : Set X} (h₁ : EquidecomposableLE G A B) (h₂ : EquidecomposableLE G B C) : EquidecomposableLE G A C

Being equidecomposable with a subset is transitive.

instance TauCeti.instIsPreorderSetEquidecomposableLE {X : Type u_1} {G : Type u_3} [Monoid G] [MulAction G X] : IsPreorder (Set X) (EquidecomposableLE G)

theorem TauCeti.Equidecomposable.symm {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {A B : Set X} (h : Equidecomposable G A B) : Equidecomposable G B A

Equidecomposability is symmetric.

theorem TauCeti.equidecomposable_comm {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {A B : Set X} : Equidecomposable G A B ↔ Equidecomposable G B A

Equidecomposability is a symmetric relation.

theorem TauCeti.Equidecomposable.equivalence (X : Type u_1) (G : Type u_3) [Group G] [MulAction G X] : Equivalence (Equidecomposable G)

Equidecomposability is an equivalence relation on Set X.

theorem TauCeti.equidecomposable_smul_set {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] (g : G) (A : Set X) : Equidecomposable G A (g • A)

A set is equidecomposable with each of its translates.

theorem TauCeti.EquidecomposableLE.antisymm {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {A B : Set X} (hAB : EquidecomposableLE G A B) (hBA : EquidecomposableLE G B A) : Equidecomposable G A B

Schröder–Bernstein theorem for equidecompositions. If each of A and B is equidecomposable with a subset of the other, then A and B are equidecomposable.

theorem TauCeti.equidecomposable_iff_equidecomposableLE {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {A B : Set X} : Equidecomposable G A B ↔ EquidecomposableLE G A B ∧ EquidecomposableLE G B A

Equidecomposability is the equivalence relation induced by the preorder EquidecomposableLE G.