Sign of a permutation

The main definition of this file is Equiv.Perm.sign, associating a ℤˣ sign with a permutation.

This file also contains miscellaneous lemmas about Equiv.Perm and Equiv.swap, building on top of those in Data/Equiv/Basic and other files in GroupTheory/Perm/*.

def Equiv.Perm.modSwap {α : Type u} [DecidableEq α] (i : α) (j : α) : Setoid (Equiv.Perm α)

modSwap i j contains permutations up to swapping i and j.

We use this to partition permutations in Matrix.det_zero_of_row_eq, such that each partition sums up to 0.

noncomputable instance Equiv.Perm.instDecidableRelPermRModSwap {α : Type u_1} [Fintype α] [DecidableEq α] (i : α) (j : α) : DecidableRel Setoid.r

theorem Equiv.Perm.perm_inv_on_of_perm_on_finset {α : Type u} {s : Finset α} {f : Equiv.Perm α} (h : ∀ (x : α), x ∈ s → ↑f x ∈ s) {y : α} (hy : y ∈ s) : ↑f⁻¹ y ∈ s

theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo {α : Type u} (f : Equiv.Perm α) {s : Set α} [Finite ↑s] (h : Set.MapsTo (↑f) s s) : Set.MapsTo (↑f⁻¹) s s

@[simp]

theorem Equiv.Perm.perm_inv_mapsTo_iff_mapsTo {α : Type u} {f : Equiv.Perm α} {s : Set α} [Finite ↑s] : Set.MapsTo (↑f⁻¹) s s ↔ Set.MapsTo (↑f) s s

theorem Equiv.Perm.perm_inv_on_of_perm_on_finite {α : Type u} {f : Equiv.Perm α} {p : α → Prop} [Finite { x // p x }] (h : (x : α) → p x → p (↑f x)) {x : α} (hx : p x) : p (↑f⁻¹ x)

@[inline, reducible]

abbrev Equiv.Perm.subtypePermOfFintype {α : Type u} (f : Equiv.Perm α) {p : α → Prop} [Fintype { x // p x }] (h : (x : α) → p x → p (↑f x)) : Equiv.Perm { x // p x }

If the permutation f maps {x // p x} into itself, then this returns the permutation on {x // p x} induced by f. Note that the h hypothesis is weaker than for Equiv.Perm.subtypePerm.

@[simp]

theorem Equiv.Perm.subtypePermOfFintype_apply {α : Type u} (f : Equiv.Perm α) {p : α → Prop} [Fintype { x // p x }] (h : (x : α) → p x → p (↑f x)) (x : { x // p x }) : ↑(Equiv.Perm.subtypePermOfFintype f h) x = { val := ↑f ↑x, property := h (↑x) x.property }

theorem Equiv.Perm.subtypePermOfFintype_one {α : Type u} (p : α → Prop) [Fintype { x // p x }] (h : (x : α) → p x → p (↑1 x)) : Equiv.Perm.subtypePermOfFintype 1 h = 1

theorem Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] (σ : Equiv.Perm (m ⊕ n)) : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)

theorem Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] {σ : Equiv.Perm (m ⊕ n)} (h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)) : σ ∈ MonoidHom.range (Equiv.Perm.sumCongrHom m n)

theorem Equiv.Perm.Disjoint.orderOf {α : Type u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) : orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ)

theorem Equiv.Perm.Disjoint.extendDomain {β : Type v} {α : Type u_1} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : Equiv.Perm.Disjoint σ τ) : Equiv.Perm.Disjoint (Equiv.Perm.extendDomain σ f) (Equiv.Perm.extendDomain τ f)

theorem Equiv.Perm.support_pow_coprime {α : Type u} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) : Equiv.Perm.support (σ ^ n) = Equiv.Perm.support σ

def Equiv.Perm.swapFactorsAux {α : Type u} [DecidableEq α] (l : List α) (f : Equiv.Perm α) : (∀ {x : α}, ↑f x ≠ x → x ∈ l) → { l // List.prod l = f ∧ ∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsSwap g }

Given a list l : List α and a permutation f : Perm α such that the nonfixed points of f are in l, recursively factors f as a product of transpositions.

Equations

• One or more equations did not get rendered due to their size.
• Equiv.Perm.swapFactorsAux [] = fun f h => { val := [], property := (_ : List.prod [] = f ∧ ∀ (g : Equiv.Perm α), g ∈ [] → Equiv.Perm.IsSwap g) }

def Equiv.Perm.swapFactors {α : Type u} [DecidableEq α] [Fintype α] [LinearOrder α] (f : Equiv.Perm α) : { l // List.prod l = f ∧ ∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsSwap g }

swapFactors represents a permutation as a product of a list of transpositions. The representation is non unique and depends on the linear order structure. For types without linear order truncSwapFactors can be used.

def Equiv.Perm.truncSwapFactors {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Trunc { l // List.prod l = f ∧ ∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsSwap g }

This computably represents the fact that any permutation can be represented as the product of a list of transpositions.

theorem Equiv.Perm.swap_induction_on {α : Type u} [DecidableEq α] [Finite α] {P : Equiv.Perm α → Prop} (f : Equiv.Perm α) : P 1 → ((f : Equiv.Perm α) → (x y : α) → x ≠ y → P f → P (Equiv.swap x y * f)) → P f

An induction principle for permutations. If P holds for the identity permutation, and is preserved under composition with a non-trivial swap, then P holds for all permutations.

theorem Equiv.Perm.closure_isSwap {α : Type u} [DecidableEq α] [Finite α] : Subgroup.closure {σ | Equiv.Perm.IsSwap σ} = ⊤

theorem Equiv.Perm.swap_induction_on' {α : Type u} [DecidableEq α] [Finite α] {P : Equiv.Perm α → Prop} (f : Equiv.Perm α) : P 1 → ((f : Equiv.Perm α) → (x y : α) → x ≠ y → P f → P (f * Equiv.swap x y)) → P f

Like swap_induction_on, but with the composition on the right of f.

An induction principle for permutations. If P holds for the identity permutation, and is preserved under composition with a non-trivial swap, then P holds for all permutations.

theorem Equiv.Perm.isConj_swap {α : Type u} [DecidableEq α] {w : α} {x : α} {y : α} {z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (Equiv.swap w x) (Equiv.swap y z)

def Equiv.Perm.finPairsLT (n : ℕ) : Finset ((_ : Fin n) × Fin n)

set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a

theorem Equiv.Perm.mem_finPairsLT {n : ℕ} {a : (_ : Fin n) × Fin n} : a ∈ Equiv.Perm.finPairsLT n ↔ a.snd < a.fst

def Equiv.Perm.signAux {n : ℕ} (a : Equiv.Perm (Fin n)) : ℤˣ

signAux σ is the sign of a permutation on Fin n, defined as the parity of the number of pairs (x₁, x₂) such that x₂ < x₁ but σ x₁ ≤ σ x₂

@[simp]

theorem Equiv.Perm.signAux_one (n : ℕ) : Equiv.Perm.signAux 1 = 1

def Equiv.Perm.signBijAux {n : ℕ} (f : Equiv.Perm (Fin n)) (a : (_ : Fin n) × Fin n) : (_ : Fin n) × Fin n

signBijAux f ⟨a, b⟩ returns the pair consisting of f a and f b in decreasing order.

theorem Equiv.Perm.signBijAux_inj {n : ℕ} {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) (b : (_ : Fin n) × Fin n) : a ∈ Equiv.Perm.finPairsLT n → b ∈ Equiv.Perm.finPairsLT n → Equiv.Perm.signBijAux f a = Equiv.Perm.signBijAux f b → a = b

theorem Equiv.Perm.signBijAux_surj {n : ℕ} {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) : a ∈ Equiv.Perm.finPairsLT n → ∃ b _H, a = Equiv.Perm.signBijAux f b

theorem Equiv.Perm.signBijAux_mem {n : ℕ} {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) : a ∈ Equiv.Perm.finPairsLT n → Equiv.Perm.signBijAux f a ∈ Equiv.Perm.finPairsLT n

@[simp]

theorem Equiv.Perm.signAux_inv {n : ℕ} (f : Equiv.Perm (Fin n)) : Equiv.Perm.signAux f⁻¹ = Equiv.Perm.signAux f

theorem Equiv.Perm.signAux_mul {n : ℕ} (f : Equiv.Perm (Fin n)) (g : Equiv.Perm (Fin n)) : Equiv.Perm.signAux (f * g) = Equiv.Perm.signAux f * Equiv.Perm.signAux g

theorem Equiv.Perm.signAux_swap {n : ℕ} {x : Fin n} {y : Fin n} (_hxy : x ≠ y) : Equiv.Perm.signAux (Equiv.swap x y) = -1

def Equiv.Perm.signAux2 {α : Type u} [DecidableEq α] : List α → Equiv.Perm α → ℤˣ

When the list l : List α contains all nonfixed points of the permutation f : Perm α, signAux2 l f recursively calculates the sign of f.

Equations

• Equiv.Perm.signAux2 [] x = 1
• Equiv.Perm.signAux2 (x_2 :: l) x = if x_2 = ↑x x_2 then Equiv.Perm.signAux2 l x else -Equiv.Perm.signAux2 l (Equiv.swap x_2 (↑x x_2) * x)

theorem Equiv.Perm.signAux_eq_signAux2 {α : Type u} [DecidableEq α] {n : ℕ} (l : List α) (f : Equiv.Perm α) (e : α ≃ Fin n) (_h : ∀ (x : α), ↑f x ≠ x → x ∈ l) : Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f

def Equiv.Perm.signAux3 {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) {s : Multiset α} : (∀ (x : α), x ∈ s) → ℤˣ

When the multiset s : Multiset α contains all nonfixed points of the permutation f : Perm α, signAux2 f _ recursively calculates the sign of f.

theorem Equiv.Perm.signAux3_mul_and_swap {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) (s : Multiset α) (hs : ∀ (x : α), x ∈ s) : Equiv.Perm.signAux3 (f * g) hs = Equiv.Perm.signAux3 f hs * Equiv.Perm.signAux3 g hs ∧ ∀ (x y : α), x ≠ y → Equiv.Perm.signAux3 (Equiv.swap x y) hs = -1

def Equiv.Perm.sign {α : Type u} [DecidableEq α] [Fintype α] : Equiv.Perm α →* ℤˣ

SignType.sign of a permutation returns the signature or parity of a permutation, 1 for even permutations, -1 for odd permutations. It is the unique surjective group homomorphism from Perm α to the group with two elements.

theorem Equiv.Perm.sign_mul {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) : ↑Equiv.Perm.sign (f * g) = ↑Equiv.Perm.sign f * ↑Equiv.Perm.sign g

@[simp]

theorem Equiv.Perm.sign_trans {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) : ↑Equiv.Perm.sign (f.trans g) = ↑Equiv.Perm.sign g * ↑Equiv.Perm.sign f

theorem Equiv.Perm.sign_one {α : Type u} [DecidableEq α] [Fintype α] : ↑Equiv.Perm.sign 1 = 1

@[simp]

theorem Equiv.Perm.sign_refl {α : Type u} [DecidableEq α] [Fintype α] : ↑Equiv.Perm.sign (Equiv.refl α) = 1

theorem Equiv.Perm.sign_inv {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : ↑Equiv.Perm.sign f⁻¹ = ↑Equiv.Perm.sign f

@[simp]

theorem Equiv.Perm.sign_symm {α : Type u} [DecidableEq α] [Fintype α] (e : Equiv.Perm α) : ↑Equiv.Perm.sign e.symm = ↑Equiv.Perm.sign e

theorem Equiv.Perm.sign_swap {α : Type u} [DecidableEq α] [Fintype α] {x : α} {y : α} (h : x ≠ y) : ↑Equiv.Perm.sign (Equiv.swap x y) = -1

@[simp]

theorem Equiv.Perm.sign_swap' {α : Type u} [DecidableEq α] [Fintype α] {x : α} {y : α} : ↑Equiv.Perm.sign (Equiv.swap x y) = if x = y then 1 else -1

theorem Equiv.Perm.IsSwap.sign_eq {α : Type u} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (h : Equiv.Perm.IsSwap f) : ↑Equiv.Perm.sign f = -1

theorem Equiv.Perm.signAux3_symm_trans_trans {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (e : α ≃ β) {s : Multiset α} {t : Multiset β} (hs : ∀ (x : α), x ∈ s) (ht : ∀ (x : β), x ∈ t) : Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = Equiv.Perm.signAux3 f hs

@[simp]

theorem Equiv.Perm.sign_symm_trans_trans {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (e : α ≃ β) : ↑Equiv.Perm.sign ((e.symm.trans f).trans e) = ↑Equiv.Perm.sign f

@[simp]

theorem Equiv.Perm.sign_trans_trans_symm {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm β) (e : α ≃ β) : ↑Equiv.Perm.sign ((e.trans f).trans e.symm) = ↑Equiv.Perm.sign f

theorem Equiv.Perm.sign_prod_list_swap {α : Type u} [DecidableEq α] [Fintype α] {l : List (Equiv.Perm α)} (hl : ∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsSwap g) : ↑Equiv.Perm.sign (List.prod l) = (-1) ^ List.length l

theorem Equiv.Perm.sign_surjective (α : Type u) [DecidableEq α] [Fintype α] [Nontrivial α] : Function.Surjective ↑Equiv.Perm.sign

theorem Equiv.Perm.eq_sign_of_surjective_hom {α : Type u} [DecidableEq α] [Fintype α] {s : Equiv.Perm α →* ℤˣ} (hs : Function.Surjective ↑s) : s = Equiv.Perm.sign

theorem Equiv.Perm.sign_subtypePerm {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) {p : α → Prop} [DecidablePred p] (h₁ : ∀ (x : α), p x ↔ p (↑f x)) (h₂ : (x : α) → ↑f x ≠ x → p x) : ↑Equiv.Perm.sign (Equiv.Perm.subtypePerm f h₁) = ↑Equiv.Perm.sign f

theorem Equiv.Perm.sign_eq_sign_of_equiv {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (g : Equiv.Perm β) (e : α ≃ β) (h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)) : ↑Equiv.Perm.sign f = ↑Equiv.Perm.sign g

theorem Equiv.Perm.sign_bij {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] {f : Equiv.Perm α} {g : Equiv.Perm β} (i : (x : α) → ↑f x ≠ x → β) (h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)) (hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) (hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y) : ↑Equiv.Perm.sign f = ↑Equiv.Perm.sign g

theorem Equiv.Perm.prod_prodExtendRight {β : Type v} {α : Type u_1} [DecidableEq α] (σ : α → Equiv.Perm β) {l : List α} (hl : List.Nodup l) (mem_l : ∀ (a : α), a ∈ l) : List.prod (List.map (fun a => Equiv.Perm.prodExtendRight a (σ a)) l) = Equiv.prodCongrRight σ

If we apply prod_extendRight a (σ a) for all a : α in turn, we get prod_congrRight σ.

@[simp]

theorem Equiv.Perm.sign_prodExtendRight {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : α) (σ : Equiv.Perm β) : ↑Equiv.Perm.sign (Equiv.Perm.prodExtendRight a σ) = ↑Equiv.Perm.sign σ

theorem Equiv.Perm.sign_prodCongrRight {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σ : α → Equiv.Perm β) : ↑Equiv.Perm.sign (Equiv.prodCongrRight σ) = Finset.prod Finset.univ fun k => ↑Equiv.Perm.sign (σ k)

theorem Equiv.Perm.sign_prodCongrLeft {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σ : α → Equiv.Perm β) : ↑Equiv.Perm.sign (Equiv.prodCongrLeft σ) = Finset.prod Finset.univ fun k => ↑Equiv.Perm.sign (σ k)

@[simp]

theorem Equiv.Perm.sign_permCongr {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (e : α ≃ β) (p : Equiv.Perm α) : ↑Equiv.Perm.sign (↑(Equiv.permCongr e) p) = ↑Equiv.Perm.sign p

@[simp]

theorem Equiv.Perm.sign_sumCongr {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σa : Equiv.Perm α) (σb : Equiv.Perm β) : ↑Equiv.Perm.sign (Equiv.Perm.sumCongr σa σb) = ↑Equiv.Perm.sign σa * ↑Equiv.Perm.sign σb

@[simp]

theorem Equiv.Perm.sign_subtypeCongr {α : Type u} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) : ↑Equiv.Perm.sign (Equiv.Perm.subtypeCongr ep en) = ↑Equiv.Perm.sign ep * ↑Equiv.Perm.sign en

@[simp]

theorem Equiv.Perm.sign_extendDomain {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (e : Equiv.Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : ↑Equiv.Perm.sign (Equiv.Perm.extendDomain e f) = ↑Equiv.Perm.sign e

@[simp]

theorem Equiv.Perm.sign_ofSubtype {α : Type u} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) : ↑Equiv.Perm.sign (↑Equiv.Perm.ofSubtype f) = ↑Equiv.Perm.sign f