mathlib3 documentation

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 #

mul_aut, add_aut

@[reducible]

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

Type u_1

The group of multiplicative automorphisms.

Equations

mul_aut M = (M ≃* M)

@[reducible]

def add_aut (M : Type u_1) [has_add M] :

Type u_1

The group of additive automorphisms.

Equations

add_aut M = (M ≃+ M)

@[protected, instance]

def mul_aut.group (M : Type u_2) [has_mul M] :

group (mul_aut 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

mul_aut.group M = {mul := λ (g h : M ≃* M), h.trans g, mul_assoc := _, one := mul_equiv.refl M _inst_1, one_mul := _, mul_one := _, npow := npow_rec {mul := λ (g h : M ≃* M), h.trans g}, npow_zero' := _, npow_succ' := _, inv := mul_equiv.symm _inst_1, div := λ (a b : M ≃* M), a * b.symm, div_eq_mul_inv := _, zpow := zpow_rec {inv := mul_equiv.symm _inst_1}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

@[protected, instance]

def mul_aut.inhabited (M : Type u_2) [has_mul M] :

inhabited (mul_aut M)

Equations

mul_aut.inhabited M = {default := 1}

@[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₂ = mul_equiv.trans e₂ e₁

theorem mul_aut.one_def (M : Type u_2) [has_mul M] :

1 = mul_equiv.refl M

theorem mul_aut.inv_def (M : Type u_2) [has_mul M] (e₁ : mul_aut M) :

e₁⁻¹ = mul_equiv.symm 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] :

mul_aut M →* equiv.perm M

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

Equations

mul_aut.to_perm M = {to_fun := mul_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}

@[protected, instance]

def mul_aut.apply_mul_distrib_mul_action {M : Type u_1} [monoid M] :

mul_distrib_mul_action (mul_aut M) M

The tautological action by mul_aut M on M.

This generalizes function.End.apply_mul_action.

Equations

mul_aut.apply_mul_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := λ (_x : mul_aut M) (_y : M), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}

@[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]

def mul_aut.apply_has_faithful_smul {M : Type u_1} [monoid M] :

has_faithful_smul (mul_aut M) M

mul_aut.apply_mul_action is faithful.

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

G →* mul_aut 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

mul_aut.conj = {to_fun := λ (g : G), {to_fun := λ (h : G), g * h * g⁻¹, inv_fun := λ (h : G), g⁻¹ * h * g, left_inv := _, right_inv := _, map_mul' := _}, map_one' := _, map_mul' := _}

@[simp]

theorem mul_aut.conj_apply {G : Type u_3} [group G] (g h : G) :

⇑(⇑mul_aut.conj g) h = g * h * g⁻¹

@[simp]

theorem mul_aut.conj_symm_apply {G : Type u_3} [group G] (g h : G) :

⇑(mul_equiv.symm (⇑mul_aut.conj g)) h = g⁻¹ * h * g

@[simp]

theorem mul_aut.conj_inv_apply {G : Type u_3} [group G] (g h : G) :

⇑(⇑mul_aut.conj g)⁻¹ h = g⁻¹ * h * g

@[protected, instance]

def add_aut.group (A : Type u_1) [has_add A] :

group (add_aut A)

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

add_aut.group A = {mul := λ (g h : A ≃+ A), h.trans g, mul_assoc := _, one := add_equiv.refl A _inst_1, one_mul := _, mul_one := _, npow := npow_rec {mul := λ (g h : A ≃+ A), h.trans g}, npow_zero' := _, npow_succ' := _, inv := add_equiv.symm _inst_1, div := λ (a b : A ≃+ A), a * b.symm, div_eq_mul_inv := _, zpow := zpow_rec {inv := add_equiv.symm _inst_1}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

@[protected, instance]

def add_aut.inhabited (A : Type u_1) [has_add A] :

inhabited (add_aut A)

Equations

add_aut.inhabited A = {default := 1}

@[simp]

theorem add_aut.coe_mul (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :

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

@[simp]

theorem add_aut.coe_one (A : Type u_1) [has_add A] :

theorem add_aut.mul_def (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :

e₁ * e₂ = add_equiv.trans e₂ e₁

theorem add_aut.one_def (A : Type u_1) [has_add A] :

1 = add_equiv.refl A

theorem add_aut.inv_def (A : Type u_1) [has_add A] (e₁ : add_aut A) :

e₁⁻¹ = add_equiv.symm 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]

theorem add_aut.apply_inv_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :

⇑e⁻¹ (⇑e a) = a

@[simp]

theorem add_aut.inv_apply_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :

⇑e (⇑e⁻¹ a) = a

def add_aut.to_perm (A : Type u_1) [has_add A] :

add_aut A →* equiv.perm A

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

Equations

add_aut.to_perm A = {to_fun := add_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}

@[protected, instance]

def add_aut.apply_distrib_mul_action {A : Type u_1} [add_monoid A] :

distrib_mul_action (add_aut A) A

The tautological action by add_aut A on A.

This generalizes function.End.apply_mul_action.

Equations

add_aut.apply_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := λ (_x : add_aut A) (_y : A), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

@[protected, simp]

theorem add_aut.smul_def {A : Type u_1} [add_monoid A] (f : add_aut A) (a : A) :

f • a = ⇑f a

@[protected, instance]

def add_aut.apply_has_faithful_smul {A : Type u_1} [add_monoid A] :

has_faithful_smul (add_aut A) A

add_aut.apply_distrib_mul_action is faithful.

def add_aut.conj {G : Type u_3} [add_group G] :

G →+ additive (add_aut G)

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

Equations

add_aut.conj = {to_fun := λ (g : G), ⇑additive.of_mul {to_fun := λ (h : G), g + h + -g, inv_fun := λ (h : G), -g + h + g, left_inv := _, right_inv := _, map_add' := _}, map_zero' := _, map_add' := _}

@[simp]

theorem add_aut.conj_apply {G : Type u_3} [add_group G] (g h : G) :

⇑(⇑add_aut.conj g) h = g + h + -g

@[simp]

theorem add_aut.conj_symm_apply {G : Type u_3} [add_group G] (g h : G) :

⇑(add_equiv.symm (⇑add_aut.conj g)) h = -g + h + g

@[simp]

theorem add_aut.conj_inv_apply {G : Type u_3} [add_group G] (g h : G) :

(⇑-⇑add_aut.conj g) h = -g + h + g