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

Tags

ring aut

@[instance_reducible]

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 = { smul := fun (x1 : RingAut R) (x2 : R) => x1 x2, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

@[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

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] (a : G) : (toRingAut G R) a = (toRingEquiv G R) a