mathlib3 documentation

algebra.ring.aut

Ring 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 ring_aut R := ring_equiv R R.

Implementation notes #

The definition of multiplication in the automorphism group 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/ring so that group_theory.perm is free to use equivalences (and other files that use them) before the group structure is defined.

Tags #

ring_aut

@[reducible]

def ring_aut (R : Type u_1) [has_mul R] [has_add R] :

Type u_1

The group of ring automorphisms.

Equations

ring_aut R = (R ≃+* R)

@[protected, instance]

def ring_aut.group (R : Type u_1) [has_mul R] [has_add R] :

group (ring_aut R)

The group operation on automorphisms of a ring is defined by λ g h, ring_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations

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

@[protected, instance]

def ring_aut.inhabited (R : Type u_1) [has_mul R] [has_add R] :

inhabited (ring_aut R)

Equations

ring_aut.inhabited R = {default := 1}

def ring_aut.to_add_aut (R : Type u_1) [has_mul R] [has_add R] :

ring_aut R →* add_aut R

Monoid homomorphism from ring automorphisms to additive automorphisms.

Equations

ring_aut.to_add_aut R = {to_fun := ring_equiv.to_add_equiv _inst_2, map_one' := _, map_mul' := _}

def ring_aut.to_mul_aut (R : Type u_1) [has_mul R] [has_add R] :

ring_aut R →* mul_aut R

Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

Equations

ring_aut.to_mul_aut R = {to_fun := ring_equiv.to_mul_equiv _inst_2, map_one' := _, map_mul' := _}

def ring_aut.to_perm (R : Type u_1) [has_mul R] [has_add R] :

ring_aut R →* equiv.perm R

Monoid homomorphism from ring automorphisms to permutations.

Equations

ring_aut.to_perm R = {to_fun := ring_equiv.to_equiv _inst_2, map_one' := _, map_mul' := _}

@[protected, instance]

def ring_aut.apply_mul_semiring_action {R : Type u_2} [semiring R] :

mul_semiring_action (ring_aut R) R

The tautological action by the group of automorphism of a ring R on R.

Equations

ring_aut.apply_mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (_x : ring_aut R) (_y : R), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}

@[protected, simp]

theorem ring_aut.smul_def {R : Type u_2} [semiring R] (f : ring_aut R) (r : R) :

f • r = ⇑f r

@[protected, instance]

def ring_aut.apply_has_faithful_smul {R : Type u_2} [semiring R] :

has_faithful_smul (ring_aut R) R

@[simp]

theorem mul_semiring_action.to_ring_aut_apply (G : Type u_1) (R : Type u_2) [group G] [semiring R] [mul_semiring_action G R] (x : G) :

⇑(mul_semiring_action.to_ring_aut G R) x = mul_semiring_action.to_ring_equiv G R x

def mul_semiring_action.to_ring_aut (G : Type u_1) (R : Type u_2) [group G] [semiring R] [mul_semiring_action G R] :

G →* ring_aut R

Each element of the group defines a ring automorphism.

This is a stronger version of distrib_mul_action.to_add_aut and mul_distrib_mul_action.to_mul_aut.

Equations

mul_semiring_action.to_ring_aut G R = {to_fun := mul_semiring_action.to_ring_equiv G R _inst_3, map_one' := _, map_mul' := _}