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 , MulAction , SMul :
Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

    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_3) (R : Type u_4) :
      {x : Monoid M} → {x_1 : Semiring R} → [h : MulSemiringAction M R] → MulDistribMulAction M R
      Equations
      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
        @[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
        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