Mathlib.Algebra.Ring.Aut

Module docstring

{"# 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 "}

RingAut abbrev

Full source

/-- The group of ring automorphisms. -/
abbrev RingAut := RingEquiv R R

Group of Ring Automorphisms $\text{RingAut}(R)$

Informal description

The group of ring automorphisms of a ring $R$, denoted $\text{RingAut}(R)$, consists of all ring isomorphisms from $R$ to itself, equipped with the group structure where multiplication is given by composition of maps.

RingAut.instGroup instance

: Group (RingAut R)

Full source

/-- 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)`. -/
instance : Group (RingAut R) where
  mul g h := RingEquiv.trans h g
  one := RingEquiv.refl R
  inv := RingEquiv.symm
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl
  inv_mul_cancel := RingEquiv.self_trans_symm

Group Structure on Ring Automorphisms

Informal description

The set of ring automorphisms $\text{RingAut}(R)$ of a ring $R$ forms a group under composition of maps, where the identity element is the identity automorphism and the inverse of an automorphism is its inverse map.

RingAut.instInhabited instance

: Inhabited (RingAut R)

Full source

instance : Inhabited (RingAut R) :=
  ⟨1⟩

Nonemptiness of the Ring Automorphism Group

Informal description

For any ring $R$, the set of ring automorphisms $\text{RingAut}(R)$ is nonempty, as it contains at least the identity automorphism.

RingAut.toAddAut definition

: RingAut R →* AddAut R

Full source

/-- Monoid homomorphism from ring automorphisms to additive automorphisms. -/
def toAddAut : RingAutRingAut R →* AddAut R where
  toFun := RingEquiv.toAddEquiv
  map_one' := rfl
  map_mul' _ _ := rfl

Ring automorphism to additive automorphism homomorphism

Informal description

The monoid homomorphism from the group of ring automorphisms $\text{RingAut}(R)$ to the group of additive automorphisms $\text{AddAut}(R)$, which maps each ring automorphism to its underlying additive group automorphism.

RingAut.toMulAut definition

: RingAut R →* MulAut R

Full source

/-- Monoid homomorphism from ring automorphisms to multiplicative automorphisms. -/
def toMulAut : RingAutRingAut R →* MulAut R where
  toFun := RingEquiv.toMulEquiv
  map_one' := rfl
  map_mul' _ _ := rfl

Ring automorphism to multiplicative automorphism homomorphism

Informal description

The monoid homomorphism from the group of ring automorphisms $\text{RingAut}(R)$ to the group of multiplicative automorphisms $\text{MulAut}(R)$, which maps each ring automorphism to its underlying multiplicative automorphism. This homomorphism preserves the identity and composition of automorphisms.

RingAut.toPerm definition

: RingAut R →* Equiv.Perm R

Full source

/-- Monoid homomorphism from ring automorphisms to permutations. -/
def toPerm : RingAutRingAut R →* Equiv.Perm R where
  toFun := RingEquiv.toEquiv
  map_one' := rfl
  map_mul' _ _ := rfl

Ring automorphism to permutation homomorphism

Informal description

The monoid homomorphism from the group of ring automorphisms $\text{RingAut}(R)$ to the group of permutations $\text{Perm}(R)$, mapping each ring automorphism to its underlying bijective function.