# Documentation

Mathlib.Algebra.Hom.Aut

# Multiplicative and additive group automorphisms #

This file defines the automorphism group structure on AddAut R := AddEquiv R R and MulAut R := MulEquiv R R.

## Implementation notes #

The definition of multiplication in the automorphism groups agrees with function composition, multiplication in Equiv.Perm, and multiplication in CategoryTheory.End, but not with CategoryTheory.comp.

This file is kept separate from Data/Equiv/MulAdd so that GroupTheory.Perm is free to use equivalences (and other files that use them) before the group structure is defined.

## Tags #

Type u_1

Equations
def MulAut (M : Type u_1) [inst : Mul M] :
Type u_1

The group of multiplicative automorphisms.

Equations
instance MulAut.instGroupMulAut (M : Type u_1) [inst : Mul M] :

The group operation on multiplicative automorphisms is defined by g h => MulEquiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations
instance MulAut.instInhabitedMulAut (M : Type u_1) [inst : Mul M] :
Equations
• = { default := 1 }
@[simp]
theorem MulAut.coe_mul (M : Type u_1) [inst : Mul M] (e₁ : ) (e₂ : ) :
↑(e₁ * e₂) = e₁ e₂
@[simp]
theorem MulAut.coe_one (M : Type u_1) [inst : Mul M] :
1 = id
theorem MulAut.mul_def (M : Type u_1) [inst : Mul M] (e₁ : ) (e₂ : ) :
e₁ * e₂ = MulEquiv.trans e₂ e₁
theorem MulAut.one_def (M : Type u_1) [inst : Mul M] :
theorem MulAut.inv_def (M : Type u_1) [inst : Mul M] (e₁ : ) :
e₁⁻¹ =
@[simp]
theorem MulAut.mul_apply (M : Type u_1) [inst : Mul M] (e₁ : ) (e₂ : ) (m : M) :
↑(e₁ * e₂) m = e₁ (e₂ m)
@[simp]
theorem MulAut.one_apply (M : Type u_1) [inst : Mul M] (m : M) :
1 m = m
@[simp]
theorem MulAut.apply_inv_self (M : Type u_1) [inst : Mul M] (e : ) (m : M) :
e (e⁻¹ m) = m
@[simp]
theorem MulAut.inv_apply_self (M : Type u_1) [inst : Mul M] (e : ) (m : M) :
e⁻¹ (e m) = m
def MulAut.toPerm (M : Type u_1) [inst : Mul M] :

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

Equations
• One or more equations did not get rendered due to their size.
instance MulAut.applyMulDistribMulAction {M : Type u_1} [inst : ] :

The tautological action by MulAut M on M.

This generalizes Function.End.applyMulAction.

Equations
@[simp]
theorem MulAut.smul_def {M : Type u_1} [inst : ] (f : ) (a : M) :
f a = f a
instance MulAut.apply_faithfulSMul {M : Type u_1} [inst : ] :

MulAut.applyDistribMulAction is faithful.

Equations
def MulAut.conj {G : Type u_1} [inst : ] :
G →*

Group conjugation, MulAut.conj g h = g * h * g⁻¹⁻¹, as a monoid homomorphism mapping multiplication in G into multiplication in the automorphism group MulAut G. See also the type ConjAct G for any group G, which has a MulAction (ConjAct G) G instance where conj G acts on G by conjugation.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem MulAut.conj_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑(MulAut.conj g) h = g * h * g⁻¹
@[simp]
theorem MulAut.conj_symm_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑(MulEquiv.symm (MulAut.conj g)) h = g⁻¹ * h * g
@[simp]
theorem MulAut.conj_inv_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
(MulAut.conj g)⁻¹ h = g⁻¹ * h * g

The group operation on additive automorphisms is defined by g h => AddEquiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations
Equations
• = { default := 1 }
@[simp]
theorem AddAut.coe_mul (A : Type u_1) [inst : Add A] (e₁ : ) (e₂ : ) :
↑(e₁ * e₂) = e₁ e₂
@[simp]
1 = id
theorem AddAut.mul_def (A : Type u_1) [inst : Add A] (e₁ : ) (e₂ : ) :
e₁ * e₂ = AddEquiv.trans e₂ e₁
theorem AddAut.inv_def (A : Type u_1) [inst : Add A] (e₁ : ) :
e₁⁻¹ =
@[simp]
theorem AddAut.mul_apply (A : Type u_1) [inst : Add A] (e₁ : ) (e₂ : ) (a : A) :
↑(e₁ * e₂) a = e₁ (e₂ a)
@[simp]
theorem AddAut.one_apply (A : Type u_1) [inst : Add A] (a : A) :
1 a = a
@[simp]
theorem AddAut.apply_inv_self (A : Type u_1) [inst : Add A] (e : ) (a : A) :
e⁻¹ (e a) = a
@[simp]
theorem AddAut.inv_apply_self (A : Type u_1) [inst : Add A] (e : ) (a : A) :
e (e⁻¹ a) = a

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

Equations
• One or more equations did not get rendered due to their size.
instance AddAut.applyDistribMulAction {A : Type u_1} [inst : ] :

The tautological action by AddAut A on A.

This generalizes Function.End.applyMulAction.

Equations
@[simp]
theorem AddAut.smul_def {A : Type u_1} [inst : ] (f : ) (a : A) :
f a = f a
instance AddAut.apply_faithfulSMul {A : Type u_1} [inst : ] :

AddAut.applyDistribMulAction is faithful.

Equations
def AddAut.conj {G : Type u_1} [inst : ] :

Additive group conjugation, AddAut.conj g h = g + h - g, as an additive monoid homomorphism mapping addition in G into multiplication in the automorphism group AddAut G (written additively in order to define the map).

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddAut.conj_apply {G : Type u_1} [inst : ] (g : G) (h : G) :