Permutations preserving a square matrix

A permutation σ of the index set of a square matrix M preserves M when M.submatrix σ σ = M. This file records the three closure properties TauCeti.submatrix_perm_refl, TauCeti.submatrix_perm_trans and TauCeti.submatrix_perm_symm, and packages them as the subgroup TauCeti.matrixSymmetryGroup of Equiv.Perm.

For the Cartan matrix of a Dynkin diagram these permutations are the diagram symmetries.

Main definitions

• TauCeti.matrixSymmetryGroup: the group of permutations preserving a given square matrix.

theorem TauCeti.submatrix_perm_refl {B : Type u_1} {α : Type u_2} (M : Matrix B B α) : M.submatrix ⇑(Equiv.refl B) ⇑(Equiv.refl B) = M

The identity permutation preserves every square matrix.

This is Mathlib's Matrix.submatrix_id_id with the reindexing spelled as Equiv.refl rather than as id. The two are equal only by unfolding the coercion ⇑(Equiv.refl B) = id, which rw and simp do not do: a statement carrying Matrix.submatrix_id_id where a proof about ⇑(Equiv.refl B) is expected is not type-correct at their implicit transparency, so no such statement can be rewritten with.

theorem TauCeti.submatrix_perm_trans {B : Type u_1} {α : Type u_2} {M : Matrix B B α} {σ τ : Equiv.Perm B} (hσ : M.submatrix ⇑σ ⇑σ = M) (hτ : M.submatrix ⇑τ ⇑τ = M) : M.submatrix ⇑(Equiv.trans σ τ) ⇑(Equiv.trans σ τ) = M

If σ and τ preserve a square matrix then so does σ.trans τ.

theorem TauCeti.submatrix_perm_symm {B : Type u_1} {α : Type u_2} {M : Matrix B B α} {σ : Equiv.Perm B} (hσ : M.submatrix ⇑σ ⇑σ = M) : M.submatrix ⇑(Equiv.symm σ) ⇑(Equiv.symm σ) = M

If σ preserves a square matrix then so does σ.symm.

def TauCeti.matrixSymmetryGroup {B : Type u_1} {α : Type u_2} (M : Matrix B B α) : Subgroup (Equiv.Perm B)

The symmetry group of a square matrix: the permutations of its index type which leave it unchanged when both axes are reindexed along them.

Equations

• TauCeti.matrixSymmetryGroup M = { carrier := {σ : Equiv.Perm B | M.submatrix ⇑σ ⇑σ = M}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem TauCeti.mem_matrixSymmetryGroup_iff {B : Type u_1} {α : Type u_2} {M : Matrix B B α} {σ : Equiv.Perm B} : σ ∈ matrixSymmetryGroup M ↔ M.submatrix ⇑σ ⇑σ = M