Signs of Permutations #
This file formalizes the notion of the sign (signature) of a permutation and its properties.
The sign of a permutation σ ∈ Sₙ is defined as (-1)^ℓ(σ) where ℓ(σ) is the length (number of inversions) of σ. This is a fundamental concept in combinatorics and algebra, playing a crucial role in the definition of determinants and exterior powers.
Main definitions #
Most definitions are already in Mathlib:
Equiv.Perm.sign- the sign of a permutation as a group homomorphism to ℤˣalternatingGroup- the alternating group (kernel of the sign homomorphism)
We provide:
Equiv.Perm.IsEven- a permutation is even if its sign is 1Equiv.Perm.IsOdd- a permutation is odd if its sign is -1
Main results #
Properties of the sign (Proposition prop.perm.sign.props) #
Equiv.Perm.sign_one(a): sign(id) = 1Equiv.Perm.sign_swap(b): sign(t_{i,j}) = -1 for distinct i, jEquiv.Perm.sign_cycle(c): sign of a k-cycle is (-1)^(k-1)Equiv.Perm.sign_mul(d): sign(στ) = sign(σ) · sign(τ)sign_prod_list(e): sign of a product equals product of signsEquiv.Perm.sign_inv(f): sign(σ⁻¹) = sign(σ)sign_eq_prod_pairs(g): sign as product over pairsprod_diff_comp_perm(h): product formula for differences
The sign homomorphism (Corollary cor.perm.sign.hom) #
Equiv.Perm.signis a group homomorphism from Sₙ to {1, -1}
The alternating group (Corollary cor.perm.altgp) #
alternatingGroup.normal- the alternating group is normal in Sₙ
Counting even/odd permutations (Corollary cor.perm.num-even) #
card_alternatingGroup- |Aₙ| = n!/2 for n ≥ 2sum_sign_eq_zero- Σ_{σ ∈ Sₙ} sign(σ) = 0 for n ≥ 2
Sign for finite sets (Proposition prop.perm.sign.X) #
- Sign can be defined for permutations of any finite set X, independent of chosen bijection
References #
- [Darij Grinberg, Notes on the combinatorial fundamentals of algebra][detnotes]
- [Neil Strickland, Combinatorics and algebra][Strick13]
Tags #
permutation, sign, signature, alternating group, parity
Definition of sign #
The sign of a permutation σ is (-1)^ℓ(σ) where ℓ(σ) is the length (number of inversions).
In Mathlib, this is Equiv.Perm.sign.
Definition (def.perm.sign): For n ∈ ℕ, the sign of σ ∈ Sₙ is (-1)^ℓ(σ). It is denoted (-1)^σ, sgn(σ), sign(σ), or ε(σ).
Proof that sign σ = (-1)^ℓ(σ) #
The fundamental theorem connecting the Mathlib definition of Equiv.Perm.sign
(which uses a product formula) with the textbook definition sign(σ) = (-1)^ℓ(σ)
where ℓ(σ) is the number of inversions.
This formalizes Definition (def.perm.sign).
The sign of a permutation equals (-1)^ℓ(σ) where ℓ(σ) is the number of inversions.
Definition (def.perm.sign): The sign of σ ∈ Sₙ is defined as (-1)^ℓ(σ), where ℓ(σ) is the length (number of inversions) of σ.
This theorem proves that Mathlib's Equiv.Perm.sign equals the textbook definition.
Corollary: sign as an integer equals (-1)^invCount. Definition (def.perm.sign)
A permutation is even if its sign is 1 (equivalently, if its length is even). Definition (def.perm.even-odd)
Equations
- σ.IsEven = (Equiv.Perm.sign σ = 1)
Instances For
A permutation is odd if its sign is -1 (equivalently, if its length is odd). Definition (def.perm.even-odd)
Equations
- σ.IsOdd = (Equiv.Perm.sign σ = -1)
Instances For
The identity permutation is even. This is a useful base case when reasoning about permutation parity.
The identity permutation is not odd.
A transposition (swap) is an odd permutation.
This provides a cleaner interface when working with the IsOdd predicate
rather than directly with sign values.
Every permutation is either even or odd. This follows from the fact that sign takes values in {1, -1}.
A permutation cannot be both even and odd.
Properties of the sign (Proposition prop.perm.sign.props) #
(a) The sign of the identity permutation is 1. Proposition (prop.perm.sign.props)(a)
(b) The sign of a transposition is -1. Proposition (prop.perm.sign.props)(b)
(c) The sign of a k-cycle is (-1)^(k-1). Proposition (prop.perm.sign.props)(c)
This follows from the fact that a k-cycle has support of size k and sign(σ) = -(-1)^|support(σ)| for cycles.
(f) The sign of the inverse equals the sign of the permutation. Proposition (prop.perm.sign.props)(f)
Product formula for sign (Proposition prop.perm.sign.props (g) and (h)) #
(g) For σ ∈ Sₙ: sign(σ) = ∏_{1 ≤ i < j ≤ n} (σ(i) - σ(j)) / (i - j)
(h) For any x₁, ..., xₙ in a commutative ring and σ ∈ Sₙ: ∏{1 ≤ i < j ≤ n} (x{σ(i)} - x_{σ(j)}) = sign(σ) · ∏_{1 ≤ i < j ≤ n} (xᵢ - xⱼ)
(h) Product of differences under permutation. Proposition (prop.perm.sign.props)(h)
For any elements x₁, ..., xₙ of a commutative ring and σ ∈ Sₙ: ∏{i < j} (x{σ(i)} - x_{σ(j)}) = sign(σ) · ∏_{i < j} (xᵢ - xⱼ)
(g) Sign as a product over pairs. Proposition (prop.perm.sign.props)(g)
For σ ∈ Sₙ: sign(σ) = ∏_{1 ≤ i < j ≤ n} (σ(i) - σ(j)) / (i - j)
We state this in a slightly different but equivalent form using the indicator function.
The sign homomorphism (Corollary cor.perm.sign.hom) #
The map σ ↦ sign(σ) from Sₙ to {1, -1} is a group homomorphism.
This is captured by Equiv.Perm.sign : Perm α →* ℤˣ being a MonoidHom.
Corollary (cor.perm.sign.hom) The sign is a group homomorphism from Sₙ to {1, -1}.
In Mathlib, this is expressed by Equiv.Perm.sign being a MonoidHom.
The alternating group (Corollary cor.perm.altgp) #
The set of even permutations forms a normal subgroup of Sₙ, called the alternating group.
Corollary (cor.perm.altgp) The set of all even permutations in Sₙ is a normal subgroup. This is the alternating group Aₙ.
Counting even and odd permutations (Corollary cor.perm.num-even) #
For n ≥ 2, the number of even permutations equals the number of odd permutations, and both equal n!/2.
Corollary (cor.perm.num-even) The number of even permutations in Sₙ equals n!/2 for n ≥ 2. More precisely, |Aₙ| = (card α)!/2.
The number of odd permutations equals the number of even permutations. This follows from the bijection σ ↦ σ * swap(a,b) for any distinct a, b.
Equation (eq.cor.perm.num-even.sum-sign) The sum of signs over all permutations is 0 for n ≥ 2.
∑_{σ ∈ Sₙ} sign(σ) = 0 for n ≥ 2
Sign for permutations of arbitrary finite sets (Proposition prop.perm.sign.X) #
The sign can be defined for permutations of any finite set X, not just [n]. Given a bijection φ : X → [n], we define sign_φ(σ) = sign(φ ∘ σ ∘ φ⁻¹). This is independent of the choice of φ.
Proposition (prop.perm.sign.X)(a) The sign of a permutation of a finite set is independent of the chosen bijection.
For any bijections φ₁, φ₂ : X → [n], we have sign_{φ₁}(σ) = sign_{φ₂}(σ).
Proposition (prop.perm.sign.X)(b) The identity permutation of any finite set has sign 1.