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

ink

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

The group of ring automorphisms.

Equations

• RingAut R = (R ≃+* R)

ink

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

ink

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

Equations

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

ink

def RingAut.toAddAut (R : Type u_1) [inst : Mul R] [inst : 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.

ink

def RingAut.toMulAut (R : Type u_1) [inst : Mul R] [inst : 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.

ink

def RingAut.toPerm (R : Type u_1) [inst : Mul R] [inst : 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.

ink

instance RingAut.applyMulSemiringAction {R : Type u_1} [inst : 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)

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

def MulSemiringAction.toRingAut (G : Type u_1) (R : Type u_2) [inst : Group G] [inst : Semiring R] [inst : 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.