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 Algebra/Ring/Equiv.lean so that GroupTheory.Perm is free to use equivalences (and other files that use them) before the group structure is defined.

Tags

RingAut

@[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' := ⋯ }

instance RingAut.applyMulSemiringAction {R : Type u_2} [Semiring R] : MulSemiringAction (RingAut R) R

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

Equations

• RingAut.applyMulSemiringAction = MulSemiringAction.mk ⋯ ⋯

@[simp]

theorem RingAut.smul_def {R : Type u_2} [Semiring R] (f : RingAut R) (r : R) : f • r = f r

instance RingAut.apply_faithfulSMul {R : Type u_2} [Semiring R] : FaithfulSMul (RingAut R) R

Equations

• ⋯ = ⋯

def MulSemiringAction.toRingAut (G : Type u_1) (R : Type u_2) [Group G] [Semiring R] [MulSemiringAction G R] : G →* RingAut R

Each element of the group defines a ring automorphism.

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

Equations

• MulSemiringAction.toRingAut G R = { toFun := MulSemiringAction.toRingEquiv G R, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulSemiringAction.toRingAut_apply (G : Type u_1) (R : Type u_2) [Group G] [Semiring R] [MulSemiringAction G R] (x : G) : (MulSemiringAction.toRingAut G R) x = MulSemiringAction.toRingEquiv G R x