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 #

MulAut, AddAut

def AddAut (M : Type u_1) [inst : Add M] :

Type u_1

The group of additive automorphisms.

Equations

AddAut M = (M ≃+ M)

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

Type u_1

The group of multiplicative automorphisms.

Equations

MulAut M = (M ≃* M)

instance MulAut.instGroupMulAut (M : Type u_1) [inst : 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.instGroupMulAut M = Group.mk (_ : ∀ (a : MulAut M), a⁻¹ * a = 1)

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

Inhabited (MulAut M)

Equations

MulAut.instInhabitedMulAut M = { default := 1 }

@[simp]

theorem MulAut.coe_mul (M : Type u_1) [inst : Mul M] (e₁ : MulAut M) (e₂ : MulAut M) :

↑(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₁ : MulAut M) (e₂ : MulAut M) :

e₁ * e₂ = MulEquiv.trans e₂ e₁

theorem MulAut.one_def (M : Type u_1) [inst : Mul M] :

1 = MulEquiv.refl M

theorem MulAut.inv_def (M : Type u_1) [inst : Mul M] (e₁ : MulAut M) :

e₁⁻¹ = MulEquiv.symm e₁

@[simp]

theorem MulAut.mul_apply (M : Type u_1) [inst : Mul M] (e₁ : MulAut M) (e₂ : MulAut M) (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 : MulAut M) (m : M) :

↑e (↑e⁻¹ m) = m

@[simp]

theorem MulAut.inv_apply_self (M : Type u_1) [inst : Mul M] (e : MulAut M) (m : M) :

↑e⁻¹ (↑e m) = m

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

MulAut M →* Equiv.Perm 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 : Monoid M] :

MulDistribMulAction (MulAut M) M

The tautological action by MulAut M on M.

This generalizes Function.End.applyMulAction.

Equations

MulAut.applyMulDistribMulAction = MulDistribMulAction.mk (_ : ∀ (f : M ≃* M) (x y : M), ↑f (x * y) = ↑f x * ↑f y) (_ : ∀ (h : M ≃* M), ↑h 1 = 1)

@[simp]

theorem MulAut.smul_def {M : Type u_1} [inst : Monoid M] (f : MulAut M) (a : M) :

f • a = ↑f a

instance MulAut.apply_faithfulSMul {M : Type u_1} [inst : Monoid M] :

FaithfulSMul (MulAut M) M

MulAut.applyDistribMulAction is faithful.

Equations

@MulAut.apply_faithfulSMul = @MulAut.apply_faithfulSMul.proof_1

def MulAut.conj {G : Type u_1} [inst : 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_1} [inst : Group G] (g : G) (h : G) :

↑(↑MulAut.conj g) h = g * h * g⁻¹

@[simp]

theorem MulAut.conj_symm_apply {G : Type u_1} [inst : Group G] (g : G) (h : G) :

↑(MulEquiv.symm (↑MulAut.conj g)) h = g⁻¹ * h * g

@[simp]

theorem MulAut.conj_inv_apply {G : Type u_1} [inst : Group G] (g : G) (h : G) :

↑(↑MulAut.conj g)⁻¹ h = g⁻¹ * h * g

instance AddAut.group (A : Type u_1) [inst : 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 (_ : ∀ (a : AddAut A), a⁻¹ * a = 1)

instance AddAut.instInhabitedAddAut (A : Type u_1) [inst : Add A] :

Inhabited (AddAut A)

Equations

AddAut.instInhabitedAddAut A = { default := 1 }

@[simp]

theorem AddAut.coe_mul (A : Type u_1) [inst : Add A] (e₁ : AddAut A) (e₂ : AddAut A) :

↑(e₁ * e₂) = ↑e₁ ∘ ↑e₂

@[simp]

theorem AddAut.coe_one (A : Type u_1) [inst : Add A] :

↑1 = id

theorem AddAut.mul_def (A : Type u_1) [inst : Add A] (e₁ : AddAut A) (e₂ : AddAut A) :

e₁ * e₂ = AddEquiv.trans e₂ e₁

theorem AddAut.one_def (A : Type u_1) [inst : Add A] :

1 = AddEquiv.refl A

theorem AddAut.inv_def (A : Type u_1) [inst : Add A] (e₁ : AddAut A) :

e₁⁻¹ = AddEquiv.symm e₁

@[simp]

theorem AddAut.mul_apply (A : Type u_1) [inst : Add A] (e₁ : AddAut A) (e₂ : AddAut A) (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 : AddAut A) (a : A) :

↑e⁻¹ (↑e a) = a

@[simp]

theorem AddAut.inv_apply_self (A : Type u_1) [inst : Add A] (e : AddAut A) (a : A) :

↑e (↑e⁻¹ a) = a

def AddAut.toPerm (A : Type u_1) [inst : Add A] :

AddAut A →* Equiv.Perm 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 : AddMonoid A] :

DistribMulAction (AddAut A) A

The tautological action by AddAut A on A.

This generalizes Function.End.applyMulAction.

Equations

AddAut.applyDistribMulAction = DistribMulAction.mk (_ : ∀ (h : A ≃+ A), ↑h 0 = 0) (_ : ∀ (f : A ≃+ A) (x y : A), ↑f (x + y) = ↑f x + ↑f y)

@[simp]

theorem AddAut.smul_def {A : Type u_1} [inst : AddMonoid A] (f : AddAut A) (a : A) :

f • a = ↑f a

instance AddAut.apply_faithfulSMul {A : Type u_1} [inst : AddMonoid A] :

FaithfulSMul (AddAut A) A

AddAut.applyDistribMulAction is faithful.

Equations

@AddAut.apply_faithfulSMul = @AddAut.apply_faithfulSMul.proof_1

def AddAut.conj {G : Type u_1} [inst : 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_1} [inst : AddGroup G] (g : G) (h : G) :

↑(↑Additive.toMul (↑AddAut.conj g)) h = g + h + -g

@[simp]

theorem AddAut.conj_symm_apply {G : Type u_1} [inst : AddGroup G] (g : G) (h : G) :

↑(AddEquiv.symm (↑AddAut.conj g)) h = -g + h + g

@[simp]

theorem AddAut.conj_inv_apply {G : Type u_1} [inst : AddGroup G] (g : G) (h : G) :

↑(↑Additive.toMul (↑AddAut.conj g))⁻¹ h = -g + h + g