Documentation

Mathlib.Algebra.GroupRingAction.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

class MulSemiringAction (M : Type u) (R : Type v) [inst : Monoid M] [inst : Semiring R] extends DistribMulAction :
Type (maxuv)
  • Multipliying 1 by a scalar gives 1

    smul_one : ∀ (g : M), g 1 = 1
  • Scalara multiplication distributes across multiplication

    smul_mul : ∀ (g : M) (x y : R), g (x * y) = g x * g y

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

Instances
    instance MulSemiringAction.toMulDistribMulAction (M : Type u_1) [inst : Monoid M] (R : Type v) [inst : Semiring R] [h : MulSemiringAction M R] :
    Equations
    @[simp]
    theorem MulSemiringAction.toRingHom_apply (M : Type u_1) [inst : Monoid M] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction M R] (x : M) :
    ∀ (x : R), ↑(MulSemiringAction.toRingHom M R x) x = x x
    def MulSemiringAction.toRingHom (M : Type u_1) [inst : Monoid M] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction M R] (x : M) :
    R →+* R

    Each element of the monoid defines a semiring homomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem toRingHom_injective (M : Type u_1) [inst : Monoid M] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction M R] [inst : FaithfulSMul M R] :
    @[simp]
    theorem MulSemiringAction.toRingEquiv_apply (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) :
    ∀ (a : R), ↑(MulSemiringAction.toRingEquiv G R x) a = x a
    @[simp]
    theorem MulSemiringAction.toRingEquiv_symm_apply (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) :
    ∀ (a : R), ↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G R x)) a = x⁻¹ a
    def MulSemiringAction.toRingEquiv (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) :
    R ≃+* R

    Each element of the group defines a semiring isomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    def MulSemiringAction.compHom {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (R : Type v) [inst : Semiring R] (f : N →* M) [inst : MulSemiringAction M R] :

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem smul_inv'' {M : Type u_1} [inst : Monoid M] {F : Type v} [inst : DivisionRing F] [inst : MulSemiringAction M F] (x : M) (m : F) :
    x m⁻¹ = (x m)⁻¹

    Note that smul_inv' refers to the group case, and smul_inv has an additional inverse on x.