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 Mathlib/Algebra/Group/Equiv/* so that Mathlib.GroupTheory.Perm is free to use equivalences (and other files that use them) before the group structure is defined.

Tags

MulAut, AddAut

@[reducible]

def MulAut (M : Type u_4) [Mul M] : Type u_4

The group of multiplicative automorphisms.

Equations

• MulAut M = (M ≃* M)

@[reducible]

def AddAut (M : Type u_4) [Add M] : Type u_4

The group of additive automorphisms.

Equations

• AddAut M = (M ≃+ M)

instance MulAut.instGroup (M : Type u_2) [Mul M] : Group (MulAut 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

• MulAut.instGroup M = Group.mk ⋯

instance MulAut.instInhabited (M : Type u_2) [Mul M] : Inhabited (MulAut M)

Equations

• MulAut.instInhabited M = { default := 1 }

@[simp]

theorem MulAut.coe_mul (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem MulAut.coe_one (M : Type u_2) [Mul M] : ⇑1 = id

theorem MulAut.mul_def (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) : e₁ * e₂ = MulEquiv.trans e₂ e₁

theorem MulAut.one_def (M : Type u_2) [Mul M] : 1 = MulEquiv.refl M

theorem MulAut.inv_def (M : Type u_2) [Mul M] (e₁ : MulAut M) : e₁⁻¹ = MulEquiv.symm e₁

@[simp]

theorem MulAut.mul_apply (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) (m : M) : (e₁ * e₂) m = e₁ (e₂ m)

@[simp]

theorem MulAut.one_apply (M : Type u_2) [Mul M] (m : M) : 1 m = m

@[simp]

theorem MulAut.apply_inv_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) : e (e⁻¹ m) = m

@[simp]

theorem MulAut.inv_apply_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) : e⁻¹ (e m) = m

def MulAut.toPerm (M : Type u_2) [Mul M] : MulAut M →* Equiv.Perm M

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

Equations

• MulAut.toPerm M = { toFun := MulEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

instance MulAut.applyMulAction {M : Type u_4} [Monoid M] : MulAction (MulAut M) M

The tautological action by MulAut M on M.

This generalizes Function.End.applyMulAction.

Equations

• MulAut.applyMulAction = MulAction.mk ⋯ ⋯

@[simp]

theorem MulAut.smul_def {M : Type u_4} [Monoid M] (f : MulAut M) (a : M) : f • a = f a

instance MulAut.apply_faithfulSMul {M : Type u_4} [Monoid M] : FaithfulSMul (MulAut M) M

MulAut.applyDistribMulAction is faithful.

def MulAut.conj {G : Type u_3} [Group G] : G →* MulAut 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_3} [Group G] (g h : G) : (MulAut.conj g) h = g * h * g⁻¹

@[simp]

theorem MulAut.conj_symm_apply {G : Type u_3} [Group G] (g h : G) : (MulEquiv.symm (MulAut.conj g)) h = g⁻¹ * h * g

@[simp]

theorem MulAut.conj_inv_apply {G : Type u_3} [Group G] (g h : G) : (MulAut.conj g)⁻¹ h = g⁻¹ * h * g

def MulAut.congr {G : Type u_3} [Group G] {H : Type u_4} [Group H] (ϕ : G ≃* H) : MulAut G ≃* MulAut H

Isomorphic groups have isomorphic automorphism groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulAut.congr_apply {G : Type u_3} [Group G] {H : Type u_4} [Group H] (ϕ : G ≃* H) (f : MulAut G) : (MulAut.congr ϕ) f = ϕ.symm.trans (MulEquiv.trans f ϕ)

@[simp]

theorem MulAut.congr_symm_apply {G : Type u_3} [Group G] {H : Type u_4} [Group H] (ϕ : G ≃* H) (f : MulAut H) : (MulAut.congr ϕ).symm f = ϕ.trans (MulEquiv.trans f ϕ.symm)

instance AddAut.group (A : Type u_1) [Add A] : Group (AddAut A)

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

• AddAut.group A = Group.mk ⋯

instance AddAut.instInhabited (A : Type u_1) [Add A] : Inhabited (AddAut A)

Equations

• AddAut.instInhabited A = { default := 1 }

@[simp]

theorem AddAut.coe_mul (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem AddAut.coe_one (A : Type u_1) [Add A] : ⇑1 = id

theorem AddAut.mul_def (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) : e₁ * e₂ = AddEquiv.trans e₂ e₁

theorem AddAut.one_def (A : Type u_1) [Add A] : 1 = AddEquiv.refl A

theorem AddAut.inv_def (A : Type u_1) [Add A] (e₁ : AddAut A) : e₁⁻¹ = AddEquiv.symm e₁

@[simp]

theorem AddAut.mul_apply (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) (a : A) : (e₁ * e₂) a = e₁ (e₂ a)

@[simp]

theorem AddAut.one_apply (A : Type u_1) [Add A] (a : A) : 1 a = a

@[simp]

theorem AddAut.apply_inv_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) : e⁻¹ (e a) = a

@[simp]

theorem AddAut.inv_apply_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) : e (e⁻¹ a) = a

def AddAut.toPerm (A : Type u_1) [Add A] : AddAut A →* Equiv.Perm A

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

Equations

• AddAut.toPerm A = { toFun := AddEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

instance AddAut.applyMulAction {A : Type u_4} [AddMonoid A] : MulAction (AddAut A) A

The tautological action by AddAut A on A.

This generalizes Function.End.applyMulAction.

Equations

• AddAut.applyMulAction = MulAction.mk ⋯ ⋯

@[simp]

theorem AddAut.smul_def {A : Type u_4} [AddMonoid A] (f : AddAut A) (a : A) : f • a = f a

instance AddAut.apply_faithfulSMul {A : Type u_4} [AddMonoid A] : FaithfulSMul (AddAut A) A

AddAut.applyDistribMulAction is faithful.

def AddAut.conj {G : Type u_3} [AddGroup G] : G →+ Additive (AddAut G)

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_3} [AddGroup G] (g h : G) : (Additive.toMul (AddAut.conj g)) h = g + h + -g

@[simp]

theorem AddAut.conj_symm_apply {G : Type u_3} [AddGroup G] (g h : G) : (AddEquiv.symm (AddAut.conj g)) h = -g + h + g

@[simp]

theorem AddAut.conj_inv_apply {G : Type u_3} [AddGroup G] (g h : G) : (Additive.toMul (AddAut.conj g))⁻¹ h = -g + h + g

def AddAut.congr {G : Type u_3} [AddGroup G] {H : Type u_4} [AddGroup H] (ϕ : G ≃+ H) : AddAut G ≃* AddAut H

Isomorphic additive groups have isomorphic automorphism groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddAut.congr_apply {G : Type u_3} [AddGroup G] {H : Type u_4} [AddGroup H] (ϕ : G ≃+ H) (f : AddAut G) : (AddAut.congr ϕ) f = ϕ.symm.trans (AddEquiv.trans f ϕ)

@[simp]

theorem AddAut.congr_symm_apply {G : Type u_3} [AddGroup G] {H : Type u_4} [AddGroup H] (ϕ : G ≃+ H) (f : AddAut H) : (AddAut.congr ϕ).symm f = ϕ.trans (AddEquiv.trans f ϕ.symm)

def MulAutMultiplicative (G : Type u_3) [AddGroup G] : MulAut (Multiplicative G) ≃* AddAut G

Multiplicative G and G have isomorphic automorphism groups.

Equations

• MulAutMultiplicative G = { toEquiv := AddEquiv.toMultiplicative.symm, map_mul' := ⋯ }

@[simp]

theorem MulAutMultiplicative_symm_apply_symm_apply (G : Type u_3) [AddGroup G] (a✝ : G ≃+ G) (a : Multiplicative G) : (MulEquiv.symm ((MulAutMultiplicative G).symm a✝)) a = Multiplicative.ofAdd (a✝.symm (Multiplicative.toAdd a))

@[simp]

theorem MulAutMultiplicative_apply_symm_apply (G : Type u_3) [AddGroup G] (a✝ : Multiplicative G ≃* Multiplicative G) (a : G) : (AddEquiv.symm ((MulAutMultiplicative G) a✝)) a = Multiplicative.toAdd (a✝.symm (Multiplicative.ofAdd a))

@[simp]

theorem MulAutMultiplicative_apply_apply (G : Type u_3) [AddGroup G] (a✝ : Multiplicative G ≃* Multiplicative G) (a : G) : ((MulAutMultiplicative G) a✝) a = Multiplicative.toAdd (a✝ (Multiplicative.ofAdd a))

@[simp]

theorem MulAutMultiplicative_symm_apply_apply (G : Type u_3) [AddGroup G] (a✝ : G ≃+ G) (a : Multiplicative G) : ((MulAutMultiplicative G).symm a✝) a = Multiplicative.ofAdd (a✝ (Multiplicative.toAdd a))

def AddAutAdditive (G : Type u_3) [Group G] : AddAut (Additive G) ≃* MulAut G

Additive G and G have isomorphic automorphism groups.

Equations

• AddAutAdditive G = { toEquiv := MulEquiv.toAdditive.symm, map_mul' := ⋯ }

@[simp]

theorem AddAutAdditive_apply_symm_apply (G : Type u_3) [Group G] (a✝ : Additive G ≃+ Additive G) (a : G) : (MulEquiv.symm ((AddAutAdditive G) a✝)) a = Additive.toMul (a✝.symm (Additive.ofMul a))

@[simp]

theorem AddAutAdditive_symm_apply_apply (G : Type u_3) [Group G] (a✝ : G ≃* G) (a : Additive G) : ((AddAutAdditive G).symm a✝) a = Additive.ofMul (a✝ (Additive.toMul a))

@[simp]

theorem AddAutAdditive_symm_apply_symm_apply (G : Type u_3) [Group G] (a✝ : G ≃* G) (a : Additive G) : (AddEquiv.symm ((AddAutAdditive G).symm a✝)) a = Additive.ofMul (a✝.symm (Additive.toMul a))

@[simp]

theorem AddAutAdditive_apply_apply (G : Type u_3) [Group G] (a✝ : Additive G ≃+ Additive G) (a : G) : ((AddAutAdditive G) a✝) a = Additive.toMul (a✝ (Additive.ofMul a))