Group action on rings

This file defines the typeclass of monoid acting on semirings MulSemiringAction M R.

An example of a MulSemiringAction is the action of the Galois group Gal(L/K) on the big field L. Note that Algebra does not in general satisfy the axioms of MulSemiringAction.

Implementation notes

There is no separate typeclass for group acting on rings, group acting on fields, etc. They are all grouped under MulSemiringAction.

Note

The corresponding typeclass of subrings invariant under such an action, IsInvariantSubring, is defined in Mathlib/Algebra/Ring/Action/Invariant.lean.

Tags

group action

class MulSemiringAction (M : Type u) (R : Type v) [Monoid M] [Semiring R] extends DistribMulAction M R : Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction: it expresses the interplay between the action and both addition and multiplication on the target. Two key axioms are g • (x + y) = (g • x) + (g • y) and g • (x * y) = (g • x) * (g • y).

A typical use case is the action of a Galois group $Gal(L/K)$ on the field L.

• smul : M → R → R
• one_smul (b : R) : 1 • b = b
• mul_smul (x y : M) (b : R) : (x * y) • b = x • y • b
• smul_zero (a : M) : a • 0 = 0
• smul_add (a : M) (x y : R) : a • (x + y) = a • x + a • y
• smul_one (g : M) : g • 1 = 1

  Multiplying 1 by a scalar gives 1

• smul_mul (g : M) (x y : R) : g • (x * y) = g • x * g • y

  Scalar multiplication distributes across multiplication

@[instance 100]

instance MulSemiringAction.toMulDistribMulAction (M : Type u_3) (R : Type u_4) {x✝ : Monoid M} {x✝¹ : Semiring R} [h : MulSemiringAction M R] : MulDistribMulAction M R

Equations

• MulSemiringAction.toMulDistribMulAction M R = { toMulAction := h.toMulAction, smul_mul := ⋯, smul_one := ⋯ }

def MulSemiringAction.toRingHom (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] (x : M) : R →+* R

Each element of the monoid defines a semiring homomorphism.

Equations

• MulSemiringAction.toRingHom M R x = { toMonoidHom := MulDistribMulAction.toMonoidHom R x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MulSemiringAction.toRingHom_apply (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] (x : M) (x✝ : R) : (toRingHom M R x) x✝ = x • x✝

theorem toRingHom_injective (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] [FaithfulSMul M R] : Function.Injective (MulSemiringAction.toRingHom M R)

instance RingHom.applyMulSemiringAction (R : Type v) [Semiring R] : MulSemiringAction (R →+* R) R

The tautological action by R →+* R on R.

This generalizes Function.End.applyMulAction.

Equations

• RingHom.applyMulSemiringAction R = { smul := fun (x1 : R →+* R) (x2 : R) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

@[simp]

theorem RingHom.smul_def (R : Type v) [Semiring R] (f : R →+* R) (a : R) : f • a = f a

instance RingHom.applyFaithfulSMul (R : Type v) [Semiring R] : FaithfulSMul (R →+* R) R

RingHom.applyMulSemiringAction is faithful.

@[reducible, inline]

abbrev MulSemiringAction.compHom {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (R : Type v) [Semiring R] (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R

Compose a MulSemiringAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Equations

• MulSemiringAction.compHom R f = { toDistribMulAction := DistribMulAction.compHom R f, smul_one := ⋯, smul_mul := ⋯ }