# Documentation

Mathlib.Algebra.Ring.Aut

# Ring automorphisms #

This file defines the automorphism group structure on RingAut R := RingEquiv R R.

## Implementation notes #

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

## Tags #

RingAut

def RingAut (R : Type u_1) [inst : Mul R] [inst : Add R] :
Type u_1

The group of ring automorphisms.

Equations
instance RingAut.instGroupRingAut (R : Type u_1) [inst : Mul R] [inst : Add R] :

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

Equations
instance RingAut.instInhabitedRingAut (R : Type u_1) [inst : Mul R] [inst : Add R] :
Equations
• = { default := 1 }
def RingAut.toAddAut (R : Type u_1) [inst : Mul R] [inst : Add R] :

Monoid homomorphism from ring automorphisms to additive automorphisms.

Equations
• One or more equations did not get rendered due to their size.
def RingAut.toMulAut (R : Type u_1) [inst : Mul R] [inst : Add R] :

Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

Equations
• One or more equations did not get rendered due to their size.
def RingAut.toPerm (R : Type u_1) [inst : Mul R] [inst : Add R] :

Monoid homomorphism from ring automorphisms to permutations.

Equations
• One or more equations did not get rendered due to their size.
instance RingAut.applyMulSemiringAction {R : Type u_1} [inst : ] :

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

Equations
@[simp]
theorem RingAut.smul_def {R : Type u_1} [inst : ] (f : ) (r : R) :
f r = f r
instance RingAut.apply_faithfulSMul {R : Type u_1} [inst : ] :
Equations
@[simp]
theorem MulSemiringAction.toRingAut_apply (G : Type u_1) (R : Type u_2) [inst : ] [inst : ] [inst : ] (x : G) :
↑() x =
def MulSemiringAction.toRingAut (G : Type u_1) (R : Type u_2) [inst : ] [inst : ] [inst : ] :
G →*

Each element of the group defines a ring automorphism.

This is a stronger version of DistribMulAction.toAddAut and MulDistribMulAction.toMulAut.

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