Documentation

Mathlib.Algebra.Ring.Action.Basic

Group action on rings #

This file defines the typeclass of monoid acting on semirings MulSemiringAction M R, and the corresponding typeclass of invariant subrings.

Note that Algebra does not 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.

Tags #

group action, invariant subring

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

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

  • 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

    Multipliying 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
    theorem MulSemiringAction.smul_one {M : Type u} {R : Type v} :
    ∀ {inst : Monoid M} {inst_1 : Semiring R} [self : MulSemiringAction M R] (g : M), g • 1 = 1

    Multipliying 1 by a scalar gives 1

    source
    theorem MulSemiringAction.smul_mul {M : Type u} {R : Type v} :
    ∀ {inst : Monoid M} {inst_1 : Semiring R} [self : MulSemiringAction M R] (g : M) (x y : R), g • (x * y) = g • x * g • y

    Scalar multiplication distributes across multiplication

    source
    @[instance 100]
    instance MulSemiringAction.toMulDistribMulAction (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [h : MulSemiringAction M R] :
    MulDistribMulAction M R
    Equations
    source
    @[simp]
    theorem MulSemiringAction.toRingHom_apply (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] (x : M) :
    ∀ (x_1 : R), (MulSemiringAction.toRingHom M R x) x_1 = x • x_1
    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
    Instances For
      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
      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.

      Equations
      • ⋯ = ⋯
      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
      Instances For