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

@[reducible]

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

The group of ring automorphisms.

Equations

• RingAut R = (R ≃+* R)

instance RingAut.instGroupRingAut (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.instGroupRingAut R = Group.mk (_ : ∀ (a : RingAut R), a⁻¹ * a = 1)

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

Equations

• RingAut.instInhabitedRingAut 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

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

def RingAut.toMulAut (R : Type u_1) [Mul R] [Add R] : RingAut R →* MulAut 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) [Mul R] [Add R] : RingAut R →* Equiv.Perm 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_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 (_ : ∀ (f : R ≃+* R), ↑f 1 = 1) (_ : ∀ (e : R ≃+* R) (x y : R), ↑e (x * y) = ↑e x * ↑e y)

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

• @RingAut.apply_faithfulSMul = @RingAut.apply_faithfulSMul.proof_1

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

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

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