Finitely supported permutations

This file records small bridges for Mathlib's finite-support predicate for permutations, (MulAction.fixedBy ι π)ᶜ.Finite, and packages the permutations satisfying it as the finitary symmetric group Equiv.Perm.finitary ι, a subgroup of Equiv.Perm ι.

The finitary symmetric group on a countable index type is itself countable; countability is what lets an action of it be handled one group element at a time under a filter closed under countable intersections (Mathlib's CountableInterFilter), such as the a.e. filter of a measure.

The file also supplies Equiv.Perm.exists_prodCongrRight_mem_finitary_apply_eq_on_finset: finitely many values of an arbitrary family of permutations can be matched by a family whose induced permutation of the product moves only finitely many indexed points altogether; the type synonym FinitaryPerm of the finitary symmetric group of ℕ, carrying the domain actions on path and array spaces that are installed beside those spaces; and the block swap Nat.blockSwap N, the finitely supported permutation of ℕ exchanging [0, N) with [N, 2N), which carries any finite index set inside [0, N) onto a disjoint copy.

theorem TauCeti.finite_compl_fixedBy_of_eventually_eq_self {π : Equiv.Perm ℕ} (hπ : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → π n = n) : (MulAction.fixedBy ℕ π)ᶜ.Finite

Constructor for Mathlib's finite-support predicate from an eventual fixedness bound.

theorem TauCeti.finite_compl_fixedBy_eventually_eq_self {π : Equiv.Perm ℕ} (hπ : (MulAction.fixedBy ℕ π)ᶜ.Finite) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → π n = n

A permutation of ℕ with finite Mathlib support fixes every sufficiently large index.

theorem TauCeti.finite_compl_fixedBy_iff_eventually_eq_self {π : Equiv.Perm ℕ} : (MulAction.fixedBy ℕ π)ᶜ.Finite ↔ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → π n = n

A permutation of ℕ is finitely supported iff it fixes all sufficiently large indices.

theorem TauCeti.finite_compl_fixedBy_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g h : G} (hh : (MulAction.fixedBy α h)ᶜ.Finite) : (MulAction.fixedBy α (g⁻¹ * h * g))ᶜ.Finite

Conjugating a group element preserves Mathlib's finite-support predicate (MulAction.fixedBy α ·)ᶜ.Finite; in particular this applies to conjugation of permutations.

The block swap

def Nat.blockSwap (N : ℕ) : Equiv.Perm ℕ

The finitely supported permutation of ℕ that swaps the block [0, N) with [N, 2N) pointwise and fixes everything from 2 * N on: Mathlib's half-swap finAddFlip on Fin (N + N), transported to ℕ along the value embedding.

Equations

• N.blockSwap = Equiv.Perm.viaFintypeEmbedding finAddFlip { toFun := Fin.val, inj' := ⋯ }

@[simp]

theorem Nat.blockSwap_apply_of_lt {N i : ℕ} (hi : i < N) : N.blockSwap i = N + i

On [0, N), N.blockSwap shifts by N.

@[simp]

theorem Nat.blockSwap_apply_add_of_lt {N i : ℕ} (hi : i < N) : N.blockSwap (N + i) = i

On [N, 2N), N.blockSwap shifts back by N.

@[simp]

theorem Nat.blockSwap_apply_of_le {N n : ℕ} (hn : N + N ≤ n) : N.blockSwap n = n

From 2 * N on, N.blockSwap is the identity.

theorem Nat.disjoint_map_blockSwap {N : ℕ} {F : Finset ℕ} (hF : F ⊆ Finset.range N) : Disjoint F (Finset.map (Equiv.toEmbedding N.blockSwap) F)

N.blockSwap carries any index set inside [0, N) off itself: the moved copy lands in [N, 2N).

theorem Nat.finite_compl_fixedBy_blockSwap (N : ℕ) : (MulAction.fixedBy ℕ N.blockSwap)ᶜ.Finite

N.blockSwap is finitely supported.

@[simp]

theorem Nat.blockSwap_blockSwap (N i : ℕ) : N.blockSwap (N.blockSwap i) = i

blockSwap N is an involution: two swaps restore every index.

@[simp]

theorem Nat.blockSwap_symm (N : ℕ) : Equiv.symm N.blockSwap = N.blockSwap

blockSwap N is its own inverse.

theorem TauCeti.countable_setOf_finite_ne_id {ι : Type u_1} [Countable ι] : {f : ι → ι | {x : ι | f x ≠ x}.Finite}.Countable

The self-maps of a countable type that move only finitely many points form a countable set: such a map is determined by the finite set it moves together with its values there.

def Equiv.Perm.finitary (ι : Type u_1) : Subgroup (Perm ι)

The finitary symmetric group on ι: the subgroup of Equiv.Perm ι consisting of the permutations that move only finitely many points, i.e. those satisfying Mathlib's finite-support predicate (MulAction.fixedBy ι π)ᶜ.Finite.

For finite ι this is all of Equiv.Perm ι; the definition is interesting for infinite index types, where it is the group generated by the transpositions.

Membership is mem_finitary; the structure body is not exposed, so that is the only interface.

Equations

• Equiv.Perm.finitary ι = { carrier := {π : Equiv.Perm ι | (MulAction.fixedBy ι π)ᶜ.Finite}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Equiv.Perm.mem_finitary {ι : Type u_1} {π : Perm ι} : π ∈ finitary ι ↔ (MulAction.fixedBy ι π)ᶜ.Finite

instance Equiv.Perm.instCountableSubtypeMemSubgroupFinitary {ι : Type u_1} [Countable ι] : Countable ↥(finitary ι)

The finitary symmetric group on a countable index type is countable: a finitely supported permutation moves only finitely many points, hence is determined by a finite amount of data.

theorem Equiv.Perm.exists_compl_fixedBy_subset_apply_eq {ι : Type u_1} {β : Type u_2} [Finite ι] (f g : ι ↪ β) : ∃ (σ : Perm β), (MulAction.fixedBy β σ)ᶜ ⊆ Set.range ⇑f ∪ Set.range ⇑g ∧ ∀ (i : ι), σ (f i) = g i

A pair of embeddings from a finite type is realised by a permutation supported on their ranges. For f g : ι ↪ β with ι finite there is a permutation of β carrying each f i to g i and fixing every point outside Set.range f ∪ Set.range g.

That union is finite, so Set.Finite.subset turns the containment into finite support in the sense of (MulAction.fixedBy β σ)ᶜ.Finite.

theorem Equiv.Perm.exists_finite_compl_fixedBy_apply_eq {ι : Type u_1} {β : Type u_2} [Finite ι] (f g : ι ↪ β) : ∃ (σ : Perm β), (MulAction.fixedBy β σ)ᶜ.Finite ∧ ∀ (i : ι), σ (f i) = g i

Finite-support form of Equiv.Perm.exists_compl_fixedBy_subset_apply_eq: for f g : ι ↪ β with ι finite there is a permutation of β carrying each f i to g i whose support is finite.

This is the shape consumers of finitely supported reindexing want, (MulAction.fixedBy β σ)ᶜ.Finite being Mathlib's finite-support predicate.

theorem Equiv.Perm.exists_finite_compl_fixedBy_apply_eq_on_finset {β : Type u_1} (π : Perm β) (s : Finset β) : ∃ (σ : Perm β), (MulAction.fixedBy β σ)ᶜ.Finite ∧ ∀ b ∈ s, σ b = π b

A permutation can be matched on a finite set by a finitely supported permutation.

@[simp]

theorem Equiv.Perm.compl_fixedBy_prodCongrRight {ι : Type u_1} {β : Type u_2} {τ : ι → Perm β} : (MulAction.fixedBy (ι × β) (prodCongrRight τ))ᶜ = {p : ι × β | (τ p.1) p.2 ≠ p.2}

The support of a row-wise family, read on the product, is the set of cells that the family moves in their own row.

theorem Equiv.Perm.mem_finitary_prodCongrRight_iff {ι : Type u_1} {β : Type u_2} {τ : ι → Perm β} : prodCongrRight τ ∈ finitary (ι × β) ↔ {a : ι | τ a ≠ 1}.Finite ∧ ∀ (a : ι), τ a ∈ finitary β

A row-wise family is finitely supported on the product exactly when it is finitely supported row by row. The permutation of ι × β induced by τ : ι → Equiv.Perm β moves only finitely many cells iff only finitely many rows of τ are nontrivial and every row moves only finitely many points.

theorem Equiv.Perm.exists_prodCongrRight_mem_finitary_apply_eq_on_finset {ι : Type u_1} {β : Type u_2} (π : ι → Perm β) (F : Finset (ι × β)) : ∃ (τ : ι → Perm β), prodCongrRight τ ∈ finitary (ι × β) ∧ ∀ p ∈ F, (τ p.1) p.2 = (π p.1) p.2

A family of permutations can be matched on finitely many indexed points by a family with finite total support. Given π : ι → Equiv.Perm β and finitely many pairs (i, b), there is a family τ agreeing with π at every listed pair and moving only finitely many pairs altogether.

theorem Equiv.Perm.exists_finite_compl_fixedBy_castAdd_natAdd (I J : Finset ℕ) (hIJ : Disjoint I J) {k l : ℕ} (hI : I.card = k) (hJ : J.card = l) : ∃ (σ : Perm ℕ), (MulAction.fixedBy ℕ σ)ᶜ.Finite ∧ (∀ (i : Fin k), σ ↑(Fin.castAdd l i) = (I.orderEmbOfFin hI) i) ∧ ∀ (j : Fin l), σ ↑(Fin.natAdd k j) = (J.orderEmbOfFin hJ) j

Two disjoint finite sets of cardinalities k and l are the images of the two windows of Fin (k + l) under a finitely supported permutation of ℕ.

theorem Equiv.Perm.map_Ico_eq_of_forall_apply_eq_orderEmbOfFin {σ : Perm ℕ} {J : Finset ℕ} {k l : ℕ} (hJ : J.card = l) (h : ∀ (j : Fin l), σ (k + ↑j) = (J.orderEmbOfFin hJ) j) : Finset.map (Equiv.toEmbedding σ) (Finset.Ico k (k + l)) = J

A permutation agreeing on the window [k, k + l) with the enumeration of J maps the window onto J.

The finitary symmetric group as a type synonym

def TauCeti.FinitaryPerm : Type

The finitary symmetric group of ℕ, the group of finitely supported permutations of ℕ, as a type synonym for ↥(Equiv.Perm.finitary ℕ) carrying the domain actions on path and array spaces: finitary reindexing of the time index of a path x : ℕ → α, and diagonal relabelling of both coordinates of an array x : ℕ × ℕ → α. Each action is installed beside the space it acts on. The synonym is deliberate: these are actions on the domain of a function, whereas Pi.instSMul would make a subgroup of Equiv.Perm ℕ act on the values whenever the state space α carries an action of it — which it does for α = ℕ. Wrapping the group keeps the domain actions from competing with that one.

The interface is equivFinitary, toPerm, ofPerm and FinitaryPerm.ext; no proof outside this section unfolds the synonym.

Equations

• TauCeti.FinitaryPerm = ↥(Equiv.Perm.finitary ℕ)

@[instance_reducible]

instance TauCeti.FinitaryPerm.instGroup : Group FinitaryPerm

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.FinitaryPerm.instCountable : Countable FinitaryPerm

def TauCeti.FinitaryPerm.equivFinitary : FinitaryPerm ≃ ↥(Equiv.Perm.finitary ℕ)

The identification of FinitaryPerm with the finitary symmetric group Equiv.Perm.finitary ℕ that it abbreviates.

Equations

• TauCeti.FinitaryPerm.equivFinitary = Equiv.refl TauCeti.FinitaryPerm

def TauCeti.FinitaryPerm.toPerm (g : FinitaryPerm) : Equiv.Perm ℕ

The finitely supported permutation of ℕ underlying an element of FinitaryPerm.

Equations

• g.toPerm = ↑(TauCeti.FinitaryPerm.equivFinitary g)

theorem TauCeti.FinitaryPerm.finite_compl_fixedBy_toPerm (g : FinitaryPerm) : (MulAction.fixedBy ℕ g.toPerm)ᶜ.Finite

The permutation underlying an element of FinitaryPerm is finitely supported.

theorem TauCeti.FinitaryPerm.toPerm_injective : Function.Injective toPerm

An element of FinitaryPerm is determined by the permutation underlying it.

theorem TauCeti.FinitaryPerm.ext {g h : FinitaryPerm} (hgh : g.toPerm = h.toPerm) : g = h

theorem TauCeti.FinitaryPerm.ext_iff {g h : FinitaryPerm} : g = h ↔ g.toPerm = h.toPerm

def TauCeti.FinitaryPerm.ofPerm (π : Equiv.Perm ℕ) (hπ : (MulAction.fixedBy ℕ π)ᶜ.Finite) : FinitaryPerm

Package a finitely supported permutation of ℕ as an element of FinitaryPerm.

Equations

• TauCeti.FinitaryPerm.ofPerm π hπ = TauCeti.FinitaryPerm.equivFinitary.symm ⟨π, ⋯⟩

@[simp]

theorem TauCeti.FinitaryPerm.toPerm_ofPerm (π : Equiv.Perm ℕ) (hπ : (MulAction.fixedBy ℕ π)ᶜ.Finite) : (ofPerm π hπ).toPerm = π

@[simp]

theorem TauCeti.FinitaryPerm.toPerm_one : toPerm 1 = 1

@[simp]

theorem TauCeti.FinitaryPerm.toPerm_mul (g h : FinitaryPerm) : (g * h).toPerm = g.toPerm * h.toPerm

@[simp]

theorem TauCeti.FinitaryPerm.toPerm_inv (g : FinitaryPerm) : g⁻¹.toPerm = g.toPerm⁻¹