Mathlib.Algebra.Ring.Action.Basic

Module docstring

{"# 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

MulSemiringAction structure

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

Full source

/-- Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`. -/
class MulSemiringAction (M : Type u) (R : Type v) [Monoid M] [Semiring R] extends
  DistribMulAction M R where
  /-- Multipliying `1` by a scalar gives `1` -/
  smul_one : ∀ g : M, (g • (1 : R) : R) = 1
  /-- Scalar multiplication distributes across multiplication -/
  smul_mul : ∀ (g : M) (x y : R), g • (x * y) = g • x * g • y

Multiplicative action of a monoid on a semiring

Informal description

The structure `MulSemiringAction M R` represents a multiplicative action of a monoid `M` on a semiring `R`. This action combines the properties of a distributive multiplicative action (i.e., compatibility with addition and scalar multiplication) with those of a multiplicative action that preserves multiplication. Specifically, for any element `m ∈ M`, the action of `m` on `R` is a semiring homomorphism.

MulSemiringAction.toMulDistribMulAction instance

(M R) {_ : Monoid M} {_ : Semiring R} [h : MulSemiringAction M R] : MulDistribMulAction M R

Full source

instance (priority := 100) MulSemiringAction.toMulDistribMulAction
    (M R) {_ : Monoid M} {_ : Semiring R} [h : MulSemiringAction M R] :
    MulDistribMulAction M R :=
  { h with }

Multiplicative Semiring Action Implies Multiplicative Distributive Action

Informal description

For any monoid $M$ and semiring $R$ with a multiplicative semiring action of $M$ on $R$, this action is also a multiplicative distributive action of $M$ on $R$.

MulSemiringAction.toRingHom definition

[MulSemiringAction M R] (x : M) : R →+* R

Full source

/-- Each element of the monoid defines a semiring homomorphism. -/
@[simps!]
def MulSemiringAction.toRingHom [MulSemiringAction M R] (x : M) : R →+* R :=
  { MulDistribMulAction.toMonoidHom R x, DistribMulAction.toAddMonoidHom R x with }

Semiring homomorphism induced by monoid action

Informal description

For any monoid $ M $ acting multiplicatively on a semiring $ R $, each element $ x \in M $ induces a semiring homomorphism $ R \to R $ that preserves both the additive and multiplicative structures of $ R $. Specifically, this homomorphism satisfies: - $ x \cdot (a + b) = x \cdot a + x \cdot b $ (additive preservation) - $ x \cdot (a * b) = (x \cdot a) * (x \cdot b) $ (multiplicative preservation) - $ x \cdot 0 = 0 $ (preservation of zero) - $ x \cdot 1 = 1 $ (preservation of multiplicative identity)

toRingHom_injective theorem

[MulSemiringAction M R] [FaithfulSMul M R] : Function.Injective (MulSemiringAction.toRingHom M R)

Full source

theorem toRingHom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
    Function.Injective (MulSemiringAction.toRingHom M R) := fun _ _ h =>
  eq_of_smul_eq_smul fun r => RingHom.ext_iff.1 h r

Injectivity of the Ring Homomorphism Map from a Faithful Multiplicative Action

Informal description

Let $M$ be a monoid acting multiplicatively on a semiring $R$ via a `MulSemiringAction`. If the scalar multiplication action of $M$ on $R$ is faithful (i.e., distinct elements of $M$ act differently on $R$), then the map sending each $x \in M$ to its induced ring homomorphism $R \to R$ is injective.

RingHom.applyMulSemiringAction instance

: MulSemiringAction (R →+* R) R

Full source

/-- The tautological action by `R →+* R` on `R`.

This generalizes `Function.End.applyMulAction`. -/
instance RingHom.applyMulSemiringAction : MulSemiringAction (R →+* R) R where
  smul := (· <| ·)
  smul_one := map_one
  smul_mul := map_mul
  smul_zero := RingHom.map_zero
  smul_add := RingHom.map_add
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Tautological Action of Ring Endomorphisms on a Semiring

Informal description

For any semiring $R$, the monoid of ring endomorphisms $R \to+* R$ acts on $R$ via the tautological action where each endomorphism $f$ acts on an element $a \in R$ by $f \cdot a = f(a)$. This action preserves both the additive and multiplicative structures of $R$.

RingHom.smul_def theorem

(f : R →+* R) (a : R) : f • a = f a

Full source

@[simp]
protected theorem RingHom.smul_def (f : R →+* R) (a : R) : f • a = f a :=
  rfl

Scalar Multiplication Action of Ring Endomorphisms via Evaluation

Informal description

For any ring homomorphism $f \colon R \to R$ and any element $a \in R$, the scalar multiplication action of $f$ on $a$ is equal to the evaluation of $f$ at $a$, i.e., $f \cdot a = f(a)$.

RingHom.applyFaithfulSMul instance

: FaithfulSMul (R →+* R) R

Full source

/-- `RingHom.applyMulSemiringAction` is faithful. -/
instance RingHom.applyFaithfulSMul : FaithfulSMul (R →+* R) R :=
  ⟨fun {_ _} h => RingHom.ext h⟩

Faithfulness of Ring Endomorphism Action on a Semiring

Informal description

For any semiring $R$, the action of the monoid of ring endomorphisms $R \to+* R$ on $R$ via function application is faithful. That is, distinct ring endomorphisms act differently on $R$.

MulSemiringAction.compHom abbrev

(f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R

Full source

/-- Compose a `MulSemiringAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances]. -/
abbrev MulSemiringAction.compHom (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R :=
  { DistribMulAction.compHom R f, MulDistribMulAction.compHom R f with }

Induced Multiplicative Semiring Action via Monoid Homomorphism

Informal description

Given a monoid homomorphism $f \colon N \to M$ and a multiplicative semiring action of $M$ on a semiring $R$, the composition of this action with $f$ defines a multiplicative semiring action of $N$ on $R$. Specifically, for any $n \in N$ and $r \in R$, the action is given by $n \bullet r = f(n) \bullet r$.