Equipartitions: equidecompositions as finite partitions

Mathlib defines an equidecomposition f : Equidecomp X G as a partial bijection of X moving each point of its source by an element of a fixed finite subset of G. The more familiar definition partitions the source A into finitely many pieces Aᵢ and moves each piece by one group element gᵢ, so that the translates gᵢ • Aᵢ partition the target B. This file proves that the two definitions agree.

An equipartition E : Equidecomp.Equipartition X G is a finite set of pairs (Aᵢ, gᵢ) of a nonempty source piece and a group element, whose source pieces Aᵢ are pairwise disjoint and whose target pieces gᵢ • Aᵢ are pairwise disjoint. Its source and target are the unions of these pieces.

Main definitions

• Equidecomp.Equipartition X G: finitely many nonempty source pieces with group elements, with pairwise disjoint sources and pairwise disjoint targets.
• Equidecomp.Equipartition.toEquidecomp: the equidecomposition of an equipartition, moving each source piece Aᵢ by its element gᵢ.
• Equidecomp.toEquipartition: an equipartition of an equidecomposition, with the same source and target, whose pieces move points as the equidecomposition does; empty pieces are removed.
• Equidecomp.Equipartition.sourceFinpartition, Equidecomp.Equipartition.targetFinpartition: the finite partitions of the source and of the target into the pieces.
• Equidecomp.Equipartition.ofFinpartition: the equipartition moving each part s of a finite partition by a group element γ s, when the translates γ s • s are pairwise disjoint.

Main results

• Equidecomp.Equipartition.toEquidecomp_apply, Equidecomp.Equipartition.toEquidecomp_symm_apply: the equidecomposition of an equipartition moves the piece Aᵢ by gᵢ, and its inverse moves gᵢ • Aᵢ by gᵢ⁻¹.
• Equidecomp.toEquidecomp_toEquipartition: converting an equidecomposition to an equipartition and back recovers it on its source.
• Equidecomp.exists_iff_exists_equipartition: two sets are related by an equidecomposition exactly when they are the source and target of an equipartition.
• Equidecomp.exists_iff_exists_finpartition: A and B are related by an equidecomposition exactly when some finite partition of A, with one group element for each part, has pairwise disjoint translates with union B.

Implementation notes

The name of an equipartition, its description by pieces with independent disjointness conditions on sources and targets, and the two conversions to and from Equidecomp are those proposed in mathlib4 PR 30330; no code from that PR is used here. This notion is unrelated to Finpartition.IsEquipartition, a partition into parts of almost equal size.

Source pieces are required to be nonempty: an empty piece (∅, g) would satisfy both disjointness conditions for every g without contributing to the source, the target or the equidecomposition. Removing such pieces does not change the relation, and it makes the pieces of an equipartition determined by its source partition together with the group element of each part.

References

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

structure Equidecomp.Equipartition (X : Type u_1) (G : Type u_2) [SMul G X] : Type (max u_1 u_2)

An equipartition of X for an action of G: a finite set of pairs (Aᵢ, gᵢ) of a nonempty source piece Aᵢ : Set X and a group element gᵢ : G, such that the source pieces Aᵢ are pairwise disjoint and the target pieces gᵢ • Aᵢ are pairwise disjoint. When G is a group acting on X, moving each Aᵢ by gᵢ is then an equidecomposition of the union of the Aᵢ with the union of the gᵢ • Aᵢ (see Equidecomp.Equipartition.toEquidecomp).

• pieces : Finset (Set X × G)

  The pieces, each a source piece together with the group element moving it.

• nonempty_fst (p : Set X × G) : p ∈ self.pieces → p.1.Nonempty

  Every source piece is nonempty.

• pairwiseDisjoint_fst : (↑self.pieces).PairwiseDisjoint Prod.fst

  Distinct pieces have disjoint source pieces.

• pairwiseDisjoint_smul : (↑self.pieces).PairwiseDisjoint fun (p : Set X × G) => p.2 • p.1

  Distinct pieces have disjoint target pieces.

theorem Equidecomp.Equipartition.ext_iff {X : Type u_1} {G : Type u_2} {inst✝ : SMul G X} {x y : Equipartition X G} : x = y ↔ x.pieces = y.pieces

theorem Equidecomp.Equipartition.ext {X : Type u_1} {G : Type u_2} {inst✝ : SMul G X} {x y : Equipartition X G} (pieces : x.pieces = y.pieces) : x = y

def Equidecomp.Equipartition.source {X : Type u_1} {G : Type u_2} [SMul G X] (E : Equipartition X G) : Set X

The source of an equipartition: the union of its source pieces.

def Equidecomp.Equipartition.target {X : Type u_1} {G : Type u_2} [SMul G X] (E : Equipartition X G) : Set X

The target of an equipartition: the union of its target pieces gᵢ • Aᵢ.

@[simp]

theorem Equidecomp.Equipartition.mem_source {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {x : X} : x ∈ E.source ↔ ∃ p ∈ E.pieces, x ∈ p.1

@[simp]

theorem Equidecomp.Equipartition.mem_target {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {y : X} : y ∈ E.target ↔ ∃ p ∈ E.pieces, y ∈ p.2 • p.1

theorem Equidecomp.Equipartition.fst_subset_source {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {p : Set X × G} (hp : p ∈ E.pieces) : p.1 ⊆ E.source

theorem Equidecomp.Equipartition.smul_subset_target {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {p : Set X × G} (hp : p ∈ E.pieces) : p.2 • p.1 ⊆ E.target

theorem Equidecomp.Equipartition.eq_of_mem_fst {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {p q : Set X × G} {x : X} (hp : p ∈ E.pieces) (hq : q ∈ E.pieces) (hxp : x ∈ p.1) (hxq : x ∈ q.1) : p = q

A point of the source lies in only one source piece.

theorem Equidecomp.Equipartition.eq_of_mem_smul {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {p q : Set X × G} {y : X} (hp : p ∈ E.pieces) (hq : q ∈ E.pieces) (hyp : y ∈ p.2 • p.1) (hyq : y ∈ q.2 • q.1) : p = q

A point of the target lies in only one target piece.

noncomputable def Equidecomp.Equipartition.sourceFinpartition {X : Type u_1} {G : Type u_2} [SMul G X] (E : Equipartition X G) : Finpartition E.source

The finite partition of the source of an equipartition into its source pieces.

noncomputable def Equidecomp.Equipartition.targetFinpartition {X : Type u_1} {G : Type u_2} [SMul G X] (E : Equipartition X G) : Finpartition E.target

The finite partition of the target of an equipartition into its target pieces.

@[simp]

theorem Equidecomp.Equipartition.mem_sourceFinpartition_parts {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {s : Set X} : s ∈ E.sourceFinpartition.parts ↔ ∃ p ∈ E.pieces, p.1 = s

@[simp]

theorem Equidecomp.Equipartition.mem_targetFinpartition_parts {X : Type u_1} {G : Type u_2} [SMul G X] {E : Equipartition X G} {s : Set X} : s ∈ E.targetFinpartition.parts ↔ ∃ p ∈ E.pieces, p.2 • p.1 = s

theorem Equidecomp.Equipartition.exists_pairwiseDisjoint_smul_sourceFinpartition {X : Type u_1} {G : Type u_2} [SMul G X] [Nonempty G] (E : Equipartition X G) : ∃ (γ : Set X → G), ((↑E.sourceFinpartition.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) ∧ ⋃ s ∈ E.sourceFinpartition.parts, γ s • s = E.target

Each part of E.sourceFinpartition can be assigned the group element of its piece, so that the translated parts are pairwise disjoint with union the target of E.

noncomputable def Equidecomp.Equipartition.ofFinpartition {X : Type u_1} {G : Type u_2} [SMul G X] {A : Set X} (P : Finpartition A) (γ : Set X → G) (hγ : (↑P.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) : Equipartition X G

The equipartition whose source pieces are the parts s of a finite partition P, each moved by γ s, provided these translates are pairwise disjoint.

@[simp]

theorem Equidecomp.Equipartition.mem_ofFinpartition_pieces {X : Type u_1} {G : Type u_2} [SMul G X] {A : Set X} (P : Finpartition A) (γ : Set X → G) (hγ : (↑P.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) {p : Set X × G} : p ∈ (ofFinpartition P γ hγ).pieces ↔ p.1 ∈ P.parts ∧ γ p.1 = p.2

@[simp]

theorem Equidecomp.Equipartition.ofFinpartition_source {X : Type u_1} {G : Type u_2} [SMul G X] {A : Set X} (P : Finpartition A) (γ : Set X → G) (hγ : (↑P.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) : (ofFinpartition P γ hγ).source = A

@[simp]

theorem Equidecomp.Equipartition.ofFinpartition_target {X : Type u_1} {G : Type u_2} [SMul G X] {A : Set X} (P : Finpartition A) (γ : Set X → G) (hγ : (↑P.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) : (ofFinpartition P γ hγ).target = ⋃ s ∈ P.parts, γ s • s

noncomputable def Equidecomp.toEquipartition {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) : Equipartition X G

An equipartition of an equidecomposition f: for each element g of its witness set, the points of the source that f moves by the chosen element g form a piece moved by g, and the empty pieces are removed.

theorem Equidecomp.snd_mem_witness_of_mem_toEquipartition {X : Type u_1} {G : Type u_2} [SMul G X] {f : Equidecomp X G} {p : Set X × G} (hp : p ∈ f.toEquipartition.pieces) : p.2 ∈ f.witness

Each piece of f.toEquipartition is moved by an element of the witness set of f.

theorem Equidecomp.apply_eq_smul_of_mem_toEquipartition {X : Type u_1} {G : Type u_2} [SMul G X] {f : Equidecomp X G} {p : Set X × G} {x : X} (hp : p ∈ f.toEquipartition.pieces) (hx : x ∈ p.1) : ↑f.toPartialEquiv x = p.2 • x

On each piece of f.toEquipartition, the equidecomposition f acts by the piece's group element.

@[simp]

theorem Equidecomp.toEquipartition_source {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) : f.toEquipartition.source = f.source

@[simp]

theorem Equidecomp.toEquipartition_target {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) : f.toEquipartition.target = f.target

noncomputable def Equidecomp.Equipartition.toEquidecomp {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (E : Equipartition X G) : Equidecomp X G

The equidecomposition of an equipartition: each source piece Aᵢ is moved by its group element gᵢ, giving a bijection from the source onto the target. Points outside the source are fixed.

@[simp]

theorem Equidecomp.Equipartition.toEquidecomp_source {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (E : Equipartition X G) : E.toEquidecomp.source = E.source

@[simp]

theorem Equidecomp.Equipartition.toEquidecomp_target {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (E : Equipartition X G) : E.toEquidecomp.target = E.target

theorem Equidecomp.Equipartition.toEquidecomp_apply {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {E : Equipartition X G} {p : Set X × G} {x : X} (hp : p ∈ E.pieces) (hx : x ∈ p.1) : ↑E.toEquidecomp.toPartialEquiv x = p.2 • x

The equidecomposition of an equipartition moves each source piece by its group element.

theorem Equidecomp.Equipartition.toEquidecomp_symm_apply {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {E : Equipartition X G} {p : Set X × G} {y : X} (hp : p ∈ E.pieces) (hy : y ∈ p.2 • p.1) : ↑E.toEquidecomp.symm.toPartialEquiv y = p.2⁻¹ • y

The inverse of the equidecomposition of an equipartition moves each target piece gᵢ • Aᵢ by gᵢ⁻¹.

theorem Equidecomp.Equipartition.isDecompOn_toEquidecomp {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] [DecidableEq G] (E : Equipartition X G) : IsDecompOn (↑E.toEquidecomp.toPartialEquiv) E.source (Finset.image Prod.snd E.pieces)

The equidecomposition of an equipartition only uses the group elements of its pieces.

theorem Equidecomp.toEquidecomp_toEquipartition {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (f : Equidecomp X G) : f.toEquipartition.toEquidecomp.toPartialEquiv ≈ f.toPartialEquiv

Converting an equidecomposition to an equipartition and back recovers it on its source.

theorem Equidecomp.exists_iff_exists_equipartition {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {A B : Set X} : (∃ (f : Equidecomp X G), f.source = A ∧ f.target = B) ↔ ∃ (E : Equipartition X G), E.source = A ∧ E.target = B

Two sets are related by an equidecomposition exactly when they are the source and the target of an equipartition.

theorem Equidecomp.exists_iff_exists_finpartition {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {A B : Set X} : (∃ (f : Equidecomp X G), f.source = A ∧ f.target = B) ↔ ∃ (P : Finpartition A) (γ : Set X → G), ((↑P.parts).PairwiseDisjoint fun (s : Set X) => γ s • s) ∧ ⋃ s ∈ P.parts, γ s • s = B

Equidecompositions as partitions. Two sets A and B are related by an equidecomposition exactly when there are a finite partition of A and a group element γ s for each part s, such that the translates γ s • s are pairwise disjoint with union B.