Signed permutations

Paper II, §2.2 (II:1008–1069): the signed permutations of a finite set Ω, as combinatorial data and as matrices.

• SignedPerm Ω: a permutation σ of Ω with a sign at each point, the permutation ±j ↦ ±(-1)^{s j} σ j of the signed set Ω_± = {±} × Ω, which commutes with the sign flip (II:1043). They form a group, Sym(Ω) ⋉ F₂^Ω (II:1057); the sign flip -Id is negOne, the ±1 diagonals are diag, and the action on a product of signed sets is prod (II:3062).
• SignedPerm.toMatrix: the matrix of the action on the anti-symmetric functions in the basis B^- (II:1049), the signed permutation matrix e_j ↦ (-1)^{s j} e_{σ j}. It is an injective monoid homomorphism (toMatrixHom, toMatrix_injective): an identity between products of signed permutation matrices is an identity in the group, which is decidable.
• IsSignedPerm: the matrices of this form. They are unitary, with real entries, so an involutive one is self-adjoint (IsSignedPerm.isHermitian); a diagonal one is a ±1 diagonal (IsSignedPerm.isDiag_iff); they are closed under products, -, adjoints, Kronecker products and reindexing.

(-1)^b

@[simp]

theorem MIPRE.Tailored.bitSign_false : bitSign false = 1

@[simp]

theorem MIPRE.Tailored.bitSign_true : bitSign true = -1

theorem MIPRE.Tailored.bitSign_mul_self (b : Bool) : bitSign b * bitSign b = 1

theorem MIPRE.Tailored.bitSign_xor (a b : Bool) : bitSign (a ^^ b) = bitSign a * bitSign b

theorem MIPRE.Tailored.bitSign_not (b : Bool) : (bitSign !b) = -bitSign b

@[simp]

theorem MIPRE.Tailored.star_bitSign (b : Bool) : star (bitSign b) = bitSign b

theorem MIPRE.Tailored.bitSign_ne_zero (b : Bool) : bitSign b ≠ 0

theorem MIPRE.Tailored.bitSign_injective : Function.Injective bitSign

Signed permutation matrices

theorem MIPRE.Tailored.signedPermMatrix_apply {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) (i j : Ω) : signedPermMatrix σ s i j = if σ j = i then bitSign (s j) else 0

theorem MIPRE.Tailored.signedPermMatrix_apply_self {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) (j : Ω) : signedPermMatrix σ s (σ j) j = bitSign (s j)

The entry of column j in row σ j, its only nonzero entry.

theorem MIPRE.Tailored.signedPermMatrix_one_one {Ω : Type u_1} [DecidableEq Ω] : (signedPermMatrix 1 fun (x : Ω) => false) = 1

theorem MIPRE.Tailored.signedPermMatrix_one {Ω : Type u_1} [DecidableEq Ω] (s : Ω → Bool) : signedPermMatrix 1 s = Matrix.diagonal fun (i : Ω) => bitSign (s i)

A signed permutation with trivial permutation is a ±1 diagonal.

theorem MIPRE.Tailored.neg_signedPermMatrix {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) : -signedPermMatrix σ s = signedPermMatrix σ fun (j : Ω) => !s j

theorem MIPRE.Tailored.signedPermMatrix_conjTranspose {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) : (signedPermMatrix σ s).conjTranspose = signedPermMatrix σ⁻¹ fun (i : Ω) => s (σ⁻¹ i)

theorem MIPRE.Tailored.signedPermMatrix_conjTranspose_eq_transpose {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) : (signedPermMatrix σ s).conjTranspose = (signedPermMatrix σ s).transpose

Signed permutation matrices have real entries, so their adjoint is their transpose.

theorem MIPRE.Tailored.signedPermMatrix_mul {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (σ τ : Equiv.Perm Ω) (s t : Ω → Bool) : signedPermMatrix σ s * signedPermMatrix τ t = signedPermMatrix (σ * τ) fun (j : Ω) => s (τ j) ^^ t j

theorem MIPRE.Tailored.signedPermMatrix_kronecker {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (σ : Equiv.Perm Ω) (s : Ω → Bool) (τ : Equiv.Perm Ω') (t : Ω' → Bool) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (signedPermMatrix σ s) (signedPermMatrix τ t) = signedPermMatrix (Equiv.prodCongr σ τ) fun (p : Ω × Ω') => s p.1 ^^ t p.2

theorem MIPRE.Tailored.signedPermMatrix_reindex {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (e : Ω ≃ Ω') (σ : Equiv.Perm Ω) (s : Ω → Bool) : (Matrix.reindex e e) (signedPermMatrix σ s) = signedPermMatrix (e.permCongr σ) (s ∘ ⇑e.symm)

theorem MIPRE.Tailored.isDiag_signedPermMatrix_iff {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) : (signedPermMatrix σ s).IsDiag ↔ σ = 1

The diagonal signed permutation matrices are those with trivial permutation.

Signed permutations as combinatorial data

structure MIPRE.Tailored.SignedPerm (Ω : Type u_1) : Type u_1

A signed permutation of Ω (II:1043): a permutation perm of Ω and a sign (-1)^{sign j} at each point, the permutation ±j ↦ ±(-1)^{sign j} perm j of Ω_± = {±} × Ω.

• perm : Equiv.Perm Ω

  The underlying permutation of Ω.

• sign : Ω → Bool

  The signs, true for -1.

theorem MIPRE.Tailored.SignedPerm.ext_iff {Ω : Type u_1} {x y : SignedPerm Ω} : x = y ↔ x.perm = y.perm ∧ x.sign = y.sign

theorem MIPRE.Tailored.SignedPerm.ext {Ω : Type u_1} {x y : SignedPerm Ω} (perm : x.perm = y.perm) (sign : x.sign = y.sign) : x = y

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instMul {Ω : Type u_1} : Mul (SignedPerm Ω)

Equations

• MIPRE.Tailored.SignedPerm.instMul = { mul := fun (g h : MIPRE.Tailored.SignedPerm Ω) => { perm := g.perm * h.perm, sign := fun (j : Ω) => g.sign (h.perm j) ^^ h.sign j } }

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instOne {Ω : Type u_1} : One (SignedPerm Ω)

Equations

• MIPRE.Tailored.SignedPerm.instOne = { one := { perm := 1, sign := fun (x : Ω) => false } }

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instInv {Ω : Type u_1} : Inv (SignedPerm Ω)

Equations

• MIPRE.Tailored.SignedPerm.instInv = { inv := fun (g : MIPRE.Tailored.SignedPerm Ω) => { perm := g.perm⁻¹, sign := fun (i : Ω) => g.sign (g.perm⁻¹ i) } }

@[simp]

theorem MIPRE.Tailored.SignedPerm.mul_perm {Ω : Type u_1} (g h : SignedPerm Ω) : (g * h).perm = g.perm * h.perm

@[simp]

theorem MIPRE.Tailored.SignedPerm.mul_sign {Ω : Type u_1} (g h : SignedPerm Ω) (j : Ω) : (g * h).sign j = (g.sign (h.perm j) ^^ h.sign j)

@[simp]

theorem MIPRE.Tailored.SignedPerm.one_perm {Ω : Type u_1} : perm 1 = 1

@[simp]

theorem MIPRE.Tailored.SignedPerm.one_sign {Ω : Type u_1} (j : Ω) : sign 1 j = false

@[simp]

theorem MIPRE.Tailored.SignedPerm.inv_perm {Ω : Type u_1} (g : SignedPerm Ω) : g⁻¹.perm = g.perm⁻¹

@[simp]

theorem MIPRE.Tailored.SignedPerm.inv_sign {Ω : Type u_1} (g : SignedPerm Ω) (i : Ω) : g⁻¹.sign i = g.sign (g.perm⁻¹ i)

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instGroup {Ω : Type u_1} : Group (SignedPerm Ω)

The signed permutations form a group, Sym(Ω) ⋉ F₂^Ω (II:1057).

Equations

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

def MIPRE.Tailored.SignedPerm.equivProd {Ω : Type u_1} : SignedPerm Ω ≃ Equiv.Perm Ω × (Ω → Bool)

The signed permutations of Ω as pairs.

Equations

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

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instFintypeOfDecidableEq {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] : Fintype (SignedPerm Ω)

Equations

• MIPRE.Tailored.SignedPerm.instFintypeOfDecidableEq = Fintype.ofEquiv (Equiv.Perm Ω × (Ω → Bool)) MIPRE.Tailored.SignedPerm.equivProd.symm

@[instance_reducible]

instance MIPRE.Tailored.SignedPerm.instDecidableEqOfFintype {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] : DecidableEq (SignedPerm Ω)

Equations

• MIPRE.Tailored.SignedPerm.instDecidableEqOfFintype = MIPRE.Tailored.SignedPerm.equivProd.decidableEq

def MIPRE.Tailored.SignedPerm.negOne {Ω : Type u_1} : SignedPerm Ω

The sign flip -Id (II:1029).

Equations

• MIPRE.Tailored.SignedPerm.negOne = { perm := 1, sign := fun (x : Ω) => true }

def MIPRE.Tailored.SignedPerm.diag {Ω : Type u_1} (s : Ω → Bool) : SignedPerm Ω

The ±1 diagonal with signs s.

Equations

• MIPRE.Tailored.SignedPerm.diag s = { perm := 1, sign := s }

def MIPRE.Tailored.SignedPerm.prod {Ω : Type u_1} {Ω' : Type u_2} (g : SignedPerm Ω) (h : SignedPerm Ω') : SignedPerm (Ω × Ω')

The action on a product of signed sets (II:3062–3069), whose matrix is the Kronecker product.

Equations

• g.prod h = { perm := Equiv.prodCongr g.perm h.perm, sign := fun (p : Ω × Ω') => g.sign p.1 ^^ h.sign p.2 }

def MIPRE.Tailored.SignedPerm.map {Ω : Type u_1} {Ω' : Type u_2} (e : Ω ≃ Ω') (g : SignedPerm Ω) : SignedPerm Ω'

Transport along a bijection of the underlying sets.

Equations

• MIPRE.Tailored.SignedPerm.map e g = { perm := e.permCongr g.perm, sign := g.sign ∘ ⇑e.symm }

theorem MIPRE.Tailored.SignedPerm.negOne_mul {Ω : Type u_1} (g : SignedPerm Ω) : negOne * g = { perm := g.perm, sign := fun (j : Ω) => !g.sign j }

theorem MIPRE.Tailored.SignedPerm.negOne_comm {Ω : Type u_1} (g : SignedPerm Ω) : negOne * g = g * negOne

The sign flip is central.

def MIPRE.Tailored.SignedPerm.toMatrix {Ω : Type u_1} [DecidableEq Ω] (g : SignedPerm Ω) : Matrix Ω Ω ℂ

The matrix of a signed permutation: of its action on the anti-symmetric functions, in the basis B^- (II:1049).

Equations

• g.toMatrix = MIPRE.Tailored.signedPermMatrix g.perm g.sign

theorem MIPRE.Tailored.SignedPerm.toMatrix_apply {Ω : Type u_1} [DecidableEq Ω] (g : SignedPerm Ω) (i j : Ω) : g.toMatrix i j = if g.perm j = i then bitSign (g.sign j) else 0

theorem MIPRE.Tailored.SignedPerm.toMatrix_one {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] : toMatrix 1 = 1

theorem MIPRE.Tailored.SignedPerm.toMatrix_mul {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (g h : SignedPerm Ω) : (g * h).toMatrix = g.toMatrix * h.toMatrix

def MIPRE.Tailored.SignedPerm.toMatrixHom {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] : SignedPerm Ω →* Matrix Ω Ω ℂ

The matrix interpretation, a monoid homomorphism (II:1043–1053).

Equations

• MIPRE.Tailored.SignedPerm.toMatrixHom = { toFun := MIPRE.Tailored.SignedPerm.toMatrix, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MIPRE.Tailored.SignedPerm.toMatrixHom_apply {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (g : SignedPerm Ω) : toMatrixHom g = g.toMatrix

theorem MIPRE.Tailored.SignedPerm.toMatrix_injective {Ω : Type u_1} [DecidableEq Ω] : Function.Injective toMatrix

A signed permutation is determined by its matrix.

theorem MIPRE.Tailored.SignedPerm.toMatrix_inj {Ω : Type u_1} [DecidableEq Ω] {g h : SignedPerm Ω} : g.toMatrix = h.toMatrix ↔ g = h

theorem MIPRE.Tailored.SignedPerm.toMatrix_inv {Ω : Type u_1} [DecidableEq Ω] (g : SignedPerm Ω) : g⁻¹.toMatrix = g.toMatrix.conjTranspose

theorem MIPRE.Tailored.SignedPerm.toMatrix_negOne {Ω : Type u_1} [DecidableEq Ω] : negOne.toMatrix = -1

theorem MIPRE.Tailored.SignedPerm.toMatrix_diag {Ω : Type u_1} [DecidableEq Ω] (s : Ω → Bool) : (diag s).toMatrix = Matrix.diagonal fun (i : Ω) => bitSign (s i)

theorem MIPRE.Tailored.SignedPerm.toMatrix_prod {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (g : SignedPerm Ω) (h : SignedPerm Ω') : (g.prod h).toMatrix = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) g.toMatrix h.toMatrix

theorem MIPRE.Tailored.SignedPerm.toMatrix_map {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (e : Ω ≃ Ω') (g : SignedPerm Ω) : (map e g).toMatrix = (Matrix.reindex e e) g.toMatrix

theorem MIPRE.Tailored.SignedPerm.toMatrix_mul_conjTranspose {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (g : SignedPerm Ω) : g.toMatrix * g.toMatrix.conjTranspose = 1

theorem MIPRE.Tailored.SignedPerm.toMatrix_conjTranspose_mul {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (g : SignedPerm Ω) : g.toMatrix.conjTranspose * g.toMatrix = 1

theorem MIPRE.Tailored.SignedPerm.toMatrix_mem_unitaryGroup {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (g : SignedPerm Ω) : g.toMatrix ∈ Matrix.unitaryGroup Ω ℂ

theorem MIPRE.Tailored.SignedPerm.isDiag_toMatrix_iff {Ω : Type u_1} [DecidableEq Ω] (g : SignedPerm Ω) : g.toMatrix.IsDiag ↔ g.perm = 1

Signed permutation matrices, as a property

theorem MIPRE.Tailored.isSignedPerm_iff {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} : IsSignedPerm M ↔ ∃ (g : SignedPerm Ω), g.toMatrix = M

theorem MIPRE.Tailored.SignedPerm.isSignedPerm_toMatrix {Ω : Type u_1} [DecidableEq Ω] (g : SignedPerm Ω) : IsSignedPerm g.toMatrix

theorem MIPRE.Tailored.IsSignedPerm.one {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] : IsSignedPerm 1

theorem MIPRE.Tailored.IsSignedPerm.mul {Ω : Type u_1} [DecidableEq Ω] {M N : Matrix Ω Ω ℂ} [Fintype Ω] (hM : IsSignedPerm M) (hN : IsSignedPerm N) : IsSignedPerm (M * N)

theorem MIPRE.Tailored.IsSignedPerm.neg {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : IsSignedPerm (-M)

theorem MIPRE.Tailored.IsSignedPerm.neg_one {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] : IsSignedPerm (-1)

theorem MIPRE.Tailored.IsSignedPerm.conjTranspose {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : IsSignedPerm M.conjTranspose

theorem MIPRE.Tailored.IsSignedPerm.conjTranspose_eq_transpose {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : M.conjTranspose = M.transpose

theorem MIPRE.Tailored.IsSignedPerm.transpose {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : IsSignedPerm M.transpose

theorem MIPRE.Tailored.IsSignedPerm.diagonal {Ω : Type u_1} [DecidableEq Ω] (s : Ω → Bool) : IsSignedPerm (Matrix.diagonal fun (i : Ω) => bitSign (s i))

theorem MIPRE.Tailored.IsSignedPerm.kronecker {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} {M' : Matrix Ω' Ω' ℂ} (hM : IsSignedPerm M) (hM' : IsSignedPerm M') : IsSignedPerm (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M M')

theorem MIPRE.Tailored.IsSignedPerm.reindex {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} (e : Ω ≃ Ω') (hM : IsSignedPerm M) : IsSignedPerm ((Matrix.reindex e e) M)

theorem MIPRE.Tailored.IsSignedPerm.conjTranspose_mul_self {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} [Fintype Ω] (hM : IsSignedPerm M) : M.conjTranspose * M = 1

theorem MIPRE.Tailored.IsSignedPerm.mul_conjTranspose_self {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} [Fintype Ω] (hM : IsSignedPerm M) : M * M.conjTranspose = 1

theorem MIPRE.Tailored.IsSignedPerm.mem_unitaryGroup {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} [Fintype Ω] (hM : IsSignedPerm M) : M ∈ Matrix.unitaryGroup Ω ℂ

theorem MIPRE.Tailored.IsSignedPerm.isHermitian {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} [Fintype Ω] (hM : IsSignedPerm M) (h : M * M = 1) : M.IsHermitian

An involutive signed permutation matrix is self-adjoint: it is unitary and its own inverse.

theorem MIPRE.Tailored.IsSignedPerm.isDiag_iff {Ω : Type u_1} [DecidableEq Ω] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : M.IsDiag ↔ ∃ (s : Ω → Bool), M = Matrix.diagonal fun (i : Ω) => bitSign (s i)

A diagonal signed permutation matrix is a ±1 diagonal.