# 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

source
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

Instances

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

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

Instances For

source
@[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✝
source
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)
source
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 := ⋯ }

source
@[simp]
theorem RingHom.smul_def (R : Type v) [Semiring R] (f : R →+* R) (a : R) :
f • a = f a
source
instance RingHom.applyFaithfulSMul (R : Type v) [Semiring R] :
FaithfulSMul (R →+* R) R

`RingHom.applyMulSemiringAction` is faithful.

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

Instances For