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/*
.
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
.
Instances For
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
.
Instances For
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) }
Instances For
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.
Instances For
This computably represents the fact that any permutation can be represented as the product of a list of transpositions.
Instances For
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.
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.
signBijAux f ⟨a, b⟩
returns the pair consisting of f a
and f b
in decreasing order.
Instances For
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)
Instances For
When the multiset s : Multiset α
contains all nonfixed points of the permutation f : Perm α
,
signAux2 f _
recursively calculates the sign of f
.
Instances For
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.
Instances For
If we apply prod_extendRight a (σ a)
for all a : α
in turn,
we get prod_congrRight σ
.