The group of permutations (self-equivalences) of a type α
#
This file defines the group
structure on equiv.perm α
.
Equations
- equiv.perm.perm_group = {mul := λ (f g : equiv.perm α), equiv.trans g f, mul_assoc := _, one := equiv.refl α, one_mul := _, mul_one := _, inv := equiv.symm α, div := div_inv_monoid.div._default (λ (f g : equiv.perm α), equiv.trans g f) equiv.perm.perm_group._proof_4 (equiv.refl α) equiv.perm.perm_group._proof_5 equiv.perm.perm_group._proof_6 equiv.symm, div_eq_mul_inv := _, mul_left_inv := _}
Lemmas about mixing perm
with equiv
. Because we have multiple ways to express
equiv.refl
, equiv.symm
, and equiv.trans
, we want simp lemmas for every combination.
The assumption made here is that if you're using the group structure, you want to preserve it after
simp.
Lemmas about equiv.perm.sum_congr
re-expressed via the group structure.
equiv.perm.sum_congr
as a monoid_hom
, with its two arguments bundled into a single prod
.
This is particularly useful for its monoid_hom.range
projection, which is the subgroup of
permutations which do not exchange elements between α
and β
.
Equations
- equiv.perm.sum_congr_hom α β = {to_fun := λ (a : equiv.perm α × equiv.perm β), a.fst.sum_congr a.snd, map_one' := _, map_mul' := _}
Lemmas about equiv.perm.sigma_congr_right
re-expressed via the group structure.
equiv.perm.sigma_congr_right
as a monoid_hom
.
This is particularly useful for its monoid_hom.range
projection, which is the subgroup of
permutations which do not exchange elements between fibers.
Equations
- equiv.perm.sigma_congr_right_hom β = {to_fun := equiv.perm.sigma_congr_right (λ (a : α), β a), map_one' := _, map_mul' := _}
equiv.perm.subtype_congr
as a monoid_hom
.
Equations
- equiv.perm.subtype_congr_hom p = {to_fun := λ (pair : equiv.perm {a // p a} × equiv.perm {a // ¬p a}), pair.fst.subtype_congr pair.snd, map_one' := _, map_mul' := _}
If the permutation f
fixes the subtype {x // p x}
, then this returns the permutation
on {x // p x}
induced by f
.
The inclusion map of permutations on a subtype of α
into permutations of α
,
fixing the other points.
Equations
Left-multiplying a permutation with swap i j
twice gives the original permutation.
This specialization of swap_mul_self
is useful when using cosets of permutations.
Right-multiplying a permutation with swap i j
twice gives the original permutation.
This specialization of swap_mul_self
is useful when using cosets of permutations.
A stronger version of mul_right_injective
A stronger version of mul_left_injective