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

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

The group of ring automorphisms.

Equations
@[protected, instance]
def ring_aut.group (R : Type u_1) [has_mul R] [has_add 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
@[protected, instance]
def ring_aut.inhabited (R : Type u_1) [has_mul R] [has_add R] :
Equations
def ring_aut.to_add_aut (R : Type u_1) [has_mul R] [has_add R] :

Monoid homomorphism from ring automorphisms to additive automorphisms.

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

Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

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

Monoid homomorphism from ring automorphisms to permutations.

Equations