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

@[reducible]

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

The group of additive automorphisms.

Equations

• AddAut M = (M ≃+ M)

@[reducible]

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

The group of multiplicative automorphisms.

Equations

• MulAut M = (M ≃* M)

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

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

Equations

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

@[simp]

theorem MulAut.coe_mul (M : Type u_2) [Mul M] (e₁ : MulAut M) (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₁ : MulAut M) (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₁ : MulAut M) (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

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

instance MulAut.applyMulDistribMulAction {M : Type u_4} [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_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.

Equations

• @MulAut.apply_faithfulSMul = @MulAut.apply_faithfulSMul.proof_1

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 : G) (h : G) : ↑(↑MulAut.conj g) h = g * h * g⁻¹

@[simp]

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

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 (_ : ∀ (a : AddAut A), a⁻¹ * a = 1)

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

Equations

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

@[simp]

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

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

instance AddAut.applyDistribMulAction {A : Type u_4} [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_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.

Equations

• @AddAut.apply_faithfulSMul = @AddAut.apply_faithfulSMul.proof_1

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 : 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 : 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 : G) (h : G) : ↑(↑Additive.toMul (↑AddAut.conj g))⁻¹ h = -g + h + g