Equidecompositions

This file develops the basic theory of equidecompositions.

Main Definitions

Let G be a group acting on a space X, and A B : Set X.

An equidecomposition of A and B is typically defined as a finite partition of A together with a finite list of elements of G of the same size such that applying each element to the matching piece of the partition yields a partition of B.

This yields a bijection f : A ≃ B where, given a : A, f a = γ • a for γ : G the group element for a's piece of the partition. Reversing this is easy, and so we get an equivalent (up to the choice of group elements) definition: an Equidecomposition of A and B is a bijection f : A ≃ B such that for some S : Finset G, f a ∈ S • a for all a.

We take this as our definition as it is easier to work with. It is implemented as an element PartialEquiv X X with source A and target B.

Implementation Notes

• Equidecompositions are implemented as elements of PartialEquiv X X together with a Finset of elements of the acting group and a proof that every point in the source is moved by an element in the finset.

• The requirement that G be a group is relaxed where possible.

• We introduce a non-standard predicate, IsDecompOn, to state that a function satisfies the main combinatorial property of equidecompositions, even if it is not injective or surjective.

TODO

• Prove that if two sets equidecompose into subsets of eachother, they are equidecomposable (Schroeder-Bernstein type theorem)
• Define equidecomposability into subsets as a preorder on sets and prove that its induced equivalence relation is equidecomposability.
• Prove the definition of equidecomposition used here is equivalent to the more familiar one using partitions.

def Equidecomp.IsDecompOn {X : Type u_1} {G : Type u_2} [SMul G X] (f : X → X) (A : Set X) (S : Finset G) : Prop

Let G act on a space X and A : Set X. We say f : X → X is a decomposition on A as witnessed by some S : Finset G if for all a ∈ A, the value f a can be obtained by applying some element of S to a instead.

More familiarly, the restriction of f to A is the result of partitioning A into finitely many pieces, then applying a single element of G to each piece.

Equations

• Equidecomp.IsDecompOn f A S = ∀ a ∈ A, ∃ g ∈ S, f a = g • a

structure Equidecomp (X : Type u_1) (G : Type u_2) [SMul G X] extends PartialEquiv X X : Type u_1

Let G act on a space X. An Equidecomposition with respect to X and G is a partial bijection f : PartialEquiv X X with the property that for some set elements : Finset G, (which we record), for each a ∈ f.source, f a can be obtained by applying some g ∈ elements instead. We call f an equidecomposition of f.source with f.target.

More familiarly, f is the result of partitioning f.source into finitely many pieces, then applying a single element of G to each to get a partition of f.target.

• toFun : X → X
• invFun : X → X
• source : Set X
• target : Set X
• map_source' ⦃x : X⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : X⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : X⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : X⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• isDecompOn' : ∃ (S : Finset G), IsDecompOn (↑self.toPartialEquiv) self.source S

instance Equidecomp.instCoeFunForall {X : Type u_1} {G : Type u_2} [SMul G X] : CoeFun (Equidecomp X G) fun (x : Equidecomp X G) => X → X

Note that Equidecomp X G is not FunLike.

Equations

• Equidecomp.instCoeFunForall = { coe := fun (f : Equidecomp X G) => ↑f.toPartialEquiv }

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

A finite set of group elements witnessing that f is an equidecomposition.

Equations

• f.witness = ⋯.choose

theorem Equidecomp.isDecompOn {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) : IsDecompOn (↑f.toPartialEquiv) f.source f.witness

@[simp]

theorem Equidecomp.apply_mem_target {X : Type u_1} {G : Type u_2} [SMul G X] {f : Equidecomp X G} {x : X} (h : x ∈ f.source) : ↑f.toPartialEquiv x ∈ f.target

theorem Equidecomp.toPartialEquiv_injective {X : Type u_1} {G : Type u_2} [SMul G X] : Function.Injective toPartialEquiv

theorem Equidecomp.IsDecompOn.mono {X : Type u_1} {G : Type u_2} [SMul G X] {f f' : X → X} {A A' : Set X} {S : Finset G} (h : IsDecompOn f A S) (hA' : A' ⊆ A) (hf' : Set.EqOn f f' A') : IsDecompOn f' A' S

def Equidecomp.restr {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) : Equidecomp X G

The restriction of an equidecomposition as an equidecomposition.

Equations

• f.restr A = { toPartialEquiv := f.restr A, isDecompOn' := ⋯ }

@[simp]

theorem Equidecomp.restr_toFun {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) (a✝ : X) : ↑(f.restr A).toPartialEquiv a✝ = ↑f.toPartialEquiv a✝

@[simp]

theorem Equidecomp.restr_target {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) : (f.restr A).target = f.target ∩ ↑f.symm ⁻¹' A

@[simp]

theorem Equidecomp.restr_source {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) : (f.restr A).source = f.source ∩ A

@[simp]

theorem Equidecomp.restr_invFun {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) (a✝ : X) : (f.restr A).invFun a✝ = ↑f.symm a✝

@[simp]

theorem Equidecomp.toPartialEquiv_restr {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) (A : Set X) : (f.restr A).toPartialEquiv = f.restr A

theorem Equidecomp.source_restr {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) {A : Set X} (hA : A ⊆ f.source) : (f.restr A).source = A

theorem Equidecomp.restr_of_source_subset {X : Type u_1} {G : Type u_2} [SMul G X] {f : Equidecomp X G} {A : Set X} (hA : f.source ⊆ A) : f.restr A = f

@[simp]

theorem Equidecomp.restr_univ {X : Type u_1} {G : Type u_2} [SMul G X] (f : Equidecomp X G) : f.restr Set.univ = f

def Equidecomp.refl (X : Type u_1) (G : Type u_2) [Monoid G] [MulAction G X] : Equidecomp X G

The identity function is an equidecomposition of the space with itself.

Equations

• Equidecomp.refl X G = { toPartialEquiv := PartialEquiv.refl X, isDecompOn' := ⋯ }

@[simp]

theorem Equidecomp.refl_toPartialEquiv (X : Type u_1) (G : Type u_2) [Monoid G] [MulAction G X] : (refl X G).toPartialEquiv = PartialEquiv.refl X

theorem Equidecomp.IsDecompOn.comp' {X : Type u_1} {G : Type u_2} [Monoid G] [MulAction G X] {g f : X → X} {B A : Set X} {T S : Finset G} (hg : IsDecompOn g B T) (hf : IsDecompOn f A S) : IsDecompOn (g ∘ f) (A ∩ f ⁻¹' B) (T * S)

theorem Equidecomp.IsDecompOn.comp {X : Type u_1} {G : Type u_2} [Monoid G] [MulAction G X] {g f : X → X} {B A : Set X} {T S : Finset G} (hg : IsDecompOn g B T) (hf : IsDecompOn f A S) (h : Set.MapsTo f A B) : IsDecompOn (g ∘ f) A (T * S)

noncomputable def Equidecomp.trans {X : Type u_1} {G : Type u_2} [Monoid G] [MulAction G X] (f g : Equidecomp X G) : Equidecomp X G

The composition of two equidecompositions as an equidecomposition.

Equations

• f.trans g = { toPartialEquiv := f.trans g.toPartialEquiv, isDecompOn' := ⋯ }

@[simp]

theorem Equidecomp.trans_toPartialEquiv {X : Type u_1} {G : Type u_2} [Monoid G] [MulAction G X] (f g : Equidecomp X G) : (f.trans g).toPartialEquiv = f.trans g.toPartialEquiv

theorem Equidecomp.IsDecompOn.of_leftInvOn {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {f g : X → X} {A : Set X} {S : Finset G} (hf : IsDecompOn f A S) (h : Set.LeftInvOn g f A) : IsDecompOn g (f '' A) S⁻¹

noncomputable def Equidecomp.symm {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (f : Equidecomp X G) : Equidecomp X G

The inverse function of an equidecomposition as an equidecomposition.

Equations

• f.symm = { toPartialEquiv := f.symm, isDecompOn' := ⋯ }

@[simp]

theorem Equidecomp.symm_toPartialEquiv {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (f : Equidecomp X G) : f.symm.toPartialEquiv = f.symm

theorem Equidecomp.map_target {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {f : Equidecomp X G} {x : X} (h : x ∈ f.target) : ↑f.symm.toPartialEquiv x ∈ f.source

@[simp]

theorem Equidecomp.left_inv {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {f : Equidecomp X G} {x : X} (h : x ∈ f.source) : ↑f.symm (↑f.toPartialEquiv x) = x

@[simp]

theorem Equidecomp.right_inv {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {f : Equidecomp X G} {x : X} (h : x ∈ f.target) : ↑f.toPartialEquiv (↑f.symm x) = x

@[simp]

theorem Equidecomp.symm_symm {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (f : Equidecomp X G) : f.symm.symm = f

theorem Equidecomp.symm_involutive {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] : Function.Involutive symm

theorem Equidecomp.symm_bijective {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] : Function.Bijective symm

@[simp]

theorem Equidecomp.refl_symm {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] : (refl X G).symm = refl X G

@[simp]

theorem Equidecomp.restr_refl_symm {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (A : Set X) : ((refl X G).restr A).symm = (refl X G).restr A