Paradoxical sets

Let G act on X. A set S : Set X is paradoxical, TauCeti.Paradoxical G S, when it is nonempty and splits into two disjoint sets A ∪ B = S each of which is equidecomposable with S using G. Informally, S can be cut into finitely many pieces which, moved by elements of G, reassemble into two copies of S. The empty set satisfies the splitting condition trivially and is excluded by the nonemptiness requirement.

The main result, TauCeti.paradoxical_iff_exists_subset, says that it is enough to find two disjoint subsets of S, not necessarily covering S, each equidecomposable with S. This is how paradoxical decompositions are usually exhibited, for instance for the free group of rank two. The proof enlarges one of the two subsets to the complement of the other using the Schröder–Bernstein theorem for equidecompositions, TauCeti.EquidecomposableLE.antisymm.

Paradoxicality is invariant under equidecomposition, under equivariant bijections, and under changes of the acting group that do not change the action.

Main definitions

• TauCeti.Paradoxical G S: S is nonempty and is the union of two disjoint sets, each equidecomposable with S using G.

Main results

• TauCeti.paradoxical_iff_exists_subset: S is paradoxical exactly when it is nonempty and has two disjoint subsets each equidecomposable with S.
• TauCeti.Paradoxical.of_equidecomposable, TauCeti.Equidecomposable.paradoxical_iff: paradoxicality passes to equidecomposable sets.
• TauCeti.paradoxical_image_equiv_iff: paradoxicality is invariant under equivariant bijections.
• TauCeti.paradoxical_iff_of_surjective: paradoxicality depends only on the transformations through which the group acts.

References

• A. Garrido, An introduction to amenable groups, §1.
• G. Tomkowicz, S. Wagon, The Banach–Tarski Paradox, 2nd ed., Definition 1.1 and Chapter 3.

def TauCeti.Paradoxical {X : Type u_1} (G : Type u_3) [SMul G X] (S : Set X) : Prop

A set S : Set X is paradoxical for the action of G when it is nonempty and is the union of two disjoint sets A and B, each equidecomposable with S using G.

theorem TauCeti.paradoxical_iff {X : Type u_1} {G : Type u_3} [SMul G X] {S : Set X} : Paradoxical G S ↔ S.Nonempty ∧ ∃ (A : Set X) (B : Set X), Disjoint A B ∧ A ∪ B = S ∧ Equidecomposable G A S ∧ Equidecomposable G B S

Unfolds Paradoxical.

theorem TauCeti.Paradoxical.nonempty {X : Type u_1} {G : Type u_3} [SMul G X] {S : Set X} (h : Paradoxical G S) : S.Nonempty

A paradoxical set is nonempty.

@[simp]

theorem TauCeti.not_paradoxical_empty {X : Type u_1} {G : Type u_3} [SMul G X] : ¬Paradoxical G ∅

The empty set is not paradoxical.

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

Paradoxicality is preserved by an equivariant bijection e : X ≃ Y.

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

Paradoxicality is invariant under equivariant bijections.

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

A set paradoxical using G is paradoxical using H when each element of G acts as some element of H does.

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

Paradoxicality depends only on the transformations through which the group acts: a surjection φ : G → H with φ g • x = g • x identifies paradoxicality using G and using H.

theorem TauCeti.paradoxical_iff_exists_subset {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {S : Set X} : Paradoxical G S ↔ S.Nonempty ∧ ∃ A ⊆ S, ∃ B ⊆ S, Disjoint A B ∧ Equidecomposable G A S ∧ Equidecomposable G B S

Paradoxical decompositions from disjoint subcopies. A set S is paradoxical exactly when it is nonempty and has two disjoint subsets A, B ⊆ S, not necessarily covering S, each equidecomposable with S.

theorem TauCeti.Paradoxical.of_equidecomposable {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {S T : Set X} (hS : Paradoxical G S) (hST : Equidecomposable G S T) : Paradoxical G T

Paradoxicality passes from a set to every set equidecomposable with it.

theorem TauCeti.Equidecomposable.paradoxical_iff {X : Type u_1} {G : Type u_3} [Group G] [MulAction G X] {S T : Set X} (hST : Equidecomposable G S T) : Paradoxical G S ↔ Paradoxical G T

Equidecomposable sets are simultaneously paradoxical or not.