Multiplicative and additive group automorphisms #
This file defines the automorphism group structure on add_aut R := add_equiv R R
and
mul_aut R := mul_equiv R R
.
Implementation notes #
The definition of multiplication in the automorphism groups agrees with function composition,
multiplication in equiv.perm
, and multiplication in category_theory.End
, but not with
category_theory.comp
.
This file is kept separate from data/equiv/mul_add
so that group_theory.perm
is free to use
equivalences (and other files that use them) before the group structure is defined.
Tags #
mul_aut, add_aut
The group operation on multiplicative automorphisms is defined by
λ g h, mul_equiv.trans h g
.
This means that multiplication agrees with composition, (g*h)(x) = g (h x)
.
Equations
- mul_aut.group M = {mul := λ (g h : M ≃* M), h.trans g, mul_assoc := _, one := mul_equiv.refl M _inst_1, one_mul := _, mul_one := _, npow := npow_rec {mul := λ (g h : M ≃* M), h.trans g}, npow_zero' := _, npow_succ' := _, inv := mul_equiv.symm _inst_1, div := λ (a b : M ≃* M), a * b.symm, div_eq_mul_inv := _, gpow := gpow_rec {inv := mul_equiv.symm _inst_1}, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}
Equations
- mul_aut.inhabited M = {default := 1}
Monoid hom from the group of multiplicative automorphisms to the group of permutations.
Equations
- mul_aut.to_perm M = {to_fun := mul_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}
Group conjugation, mul_aut.conj g h = g * h * g⁻¹
, as a monoid homomorphism
mapping multiplication in G
into multiplication in the automorphism group mul_aut G
.
The group operation on additive automorphisms is defined by
λ g h, add_equiv.trans h g
.
This means that multiplication agrees with composition, (g*h)(x) = g (h x)
.
Equations
- add_aut.group A = {mul := λ (g h : A ≃+ A), h.trans g, mul_assoc := _, one := add_equiv.refl A _inst_1, one_mul := _, mul_one := _, npow := npow_rec {mul := λ (g h : A ≃+ A), h.trans g}, npow_zero' := _, npow_succ' := _, inv := add_equiv.symm _inst_1, div := λ (a b : A ≃+ A), a * b.symm, div_eq_mul_inv := _, gpow := gpow_rec {inv := add_equiv.symm _inst_1}, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}
Equations
- add_aut.inhabited A = {default := 1}
Monoid hom from the group of multiplicative automorphisms to the group of permutations.
Equations
- add_aut.to_perm A = {to_fun := add_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}
Additive group conjugation, add_aut.conj g h = g + h - g
, as an additive monoid
homomorphism mapping addition in G
into multiplication in the automorphism group add_aut G
(written additively in order to define the map).