algebra.hom.aut

# Multiplicative and additive group automorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[reducible]
def mul_aut (M : Type u_1) [has_mul M] :
Type u_1

The group of multiplicative automorphisms.

Equations
@[reducible]
Type u_1

Equations
@[protected, instance]
def mul_aut.group (M : Type u_2) [has_mul M] :

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
@[protected, instance]
def mul_aut.inhabited (M : Type u_2) [has_mul M] :
Equations
@[simp]
theorem mul_aut.coe_mul (M : Type u_2) [has_mul M] (e₁ e₂ : mul_aut M) :
(e₁ * e₂) = e₁ e₂
@[simp]
theorem mul_aut.coe_one (M : Type u_2) [has_mul M] :
theorem mul_aut.mul_def (M : Type u_2) [has_mul M] (e₁ e₂ : mul_aut M) :
e₁ * e₂ = e₁
theorem mul_aut.one_def (M : Type u_2) [has_mul M] :
theorem mul_aut.inv_def (M : Type u_2) [has_mul M] (e₁ : mul_aut M) :
e₁⁻¹ =
@[simp]
theorem mul_aut.mul_apply (M : Type u_2) [has_mul M] (e₁ e₂ : mul_aut M) (m : M) :
(e₁ * e₂) m = e₁ (e₂ m)
@[simp]
theorem mul_aut.one_apply (M : Type u_2) [has_mul M] (m : M) :
1 m = m
@[simp]
theorem mul_aut.apply_inv_self (M : Type u_2) [has_mul M] (e : mul_aut M) (m : M) :
e (e⁻¹ m) = m
@[simp]
theorem mul_aut.inv_apply_self (M : Type u_2) [has_mul M] (e : mul_aut M) (m : M) :
e⁻¹ (e m) = m
def mul_aut.to_perm (M : Type u_2) [has_mul M] :

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations
@[protected, instance]

The tautological action by mul_aut M on M.

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
theorem mul_aut.smul_def {M : Type u_1} [monoid M] (f : mul_aut M) (a : M) :
f a = f a
@[protected, instance]

mul_aut.apply_mul_action is faithful.

def mul_aut.conj {G : Type u_3} [group G] :
G →*

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. See also the type conj_act G for any group G, which has a mul_action (conj_act G) G instance where conj G acts on G by conjugation.

Equations
@[simp]
theorem mul_aut.conj_apply {G : Type u_3} [group G] (g h : G) :
h = g * h * g⁻¹
@[simp]
theorem mul_aut.conj_symm_apply {G : Type u_3} [group G] (g h : G) :
h = g⁻¹ * h * g
@[simp]
theorem mul_aut.conj_inv_apply {G : Type u_3} [group G] (g h : G) :
⁻¹ h = g⁻¹ * h * g
@[protected, instance]

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
@[protected, instance]
Equations
@[simp]
(e₁ * e₂) = e₁ e₂
@[simp]
e₁ * e₂ = e₁
e₁⁻¹ =
@[simp]
theorem add_aut.mul_apply (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) (a : A) :
(e₁ * e₂) a = e₁ (e₂ a)
@[simp]
theorem add_aut.one_apply (A : Type u_1) [has_add A] (a : A) :
1 a = a
@[simp]
e⁻¹ (e a) = a
@[simp]
e (e⁻¹ a) = a

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations
@[protected, instance]

The tautological action by add_aut A on A.

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
f a = f a
@[protected, instance]