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.

Tags

ring aut

@[reducible, inline]

abbrev RingAut (R : Type u_1) [Mul R] [Add R] : Type u_1

The group of ring automorphisms.

Equations

• RingAut R = (R ≃+* R)

instance RingAut.instGroup (R : Type u_1) [Mul R] [Add R] : Group (RingAut 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

• RingAut.instGroup R = Group.mk ⋯

instance RingAut.instInhabited (R : Type u_1) [Mul R] [Add R] : Inhabited (RingAut R)

Equations

• RingAut.instInhabited R = { default := 1 }

def RingAut.toAddAut (R : Type u_1) [Mul R] [Add R] : RingAut R →* AddAut R

Monoid homomorphism from ring automorphisms to additive automorphisms.

Equations

• RingAut.toAddAut R = { toFun := RingEquiv.toAddEquiv, map_one' := ⋯, map_mul' := ⋯ }

def RingAut.toMulAut (R : Type u_1) [Mul R] [Add R] : RingAut R →* MulAut R

Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

Equations

• RingAut.toMulAut R = { toFun := RingEquiv.toMulEquiv, map_one' := ⋯, map_mul' := ⋯ }

def RingAut.toPerm (R : Type u_1) [Mul R] [Add R] : RingAut R →* Equiv.Perm R

Monoid homomorphism from ring automorphisms to permutations.

Equations

• RingAut.toPerm R = { toFun := RingEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }