mathlib documentation

algebra.ring.aut

Ring automorphisms #

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

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' := _}