Documentation

Mathlib.Algebra.GroupRingAction.Invariant

Subrings invariant under an action #

class IsInvariantSubring (M : Type u_1) {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (S : Subring R) :
  • smul_mem : ∀ (m : M) {x : R}, x Sm x S

A typeclass for subrings invariant under a MulSemiringAction.

Instances
    instance IsInvariantSubring.toMulSemiringAction (M : Type u_1) {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (S : Subring R) [IsInvariantSubring M S] :
    MulSemiringAction M { x // x S }
    Equations
    def IsInvariantSubring.subtypeHom (M : Type u_1) [Monoid M] {R' : Type u_2} [Ring R'] [MulSemiringAction M R'] (U : Subring R') [IsInvariantSubring M U] :
    { x // x U } →+*[M] R'

    The canonical inclusion from an invariant subring.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem IsInvariantSubring.coe_subtypeHom (M : Type u_1) [Monoid M] {R' : Type u_2} [Ring R'] [MulSemiringAction M R'] (U : Subring R') [IsInvariantSubring M U] :
      ↑(IsInvariantSubring.subtypeHom M U) = Subtype.val