Documentation

Mathlib.Algebra.Ring.Action.Invariant

Subrings invariant under an action #

If a monoid acts on a ring via a MulSemiringAction, then IsInvariantSubring is a predicate on subrings asserting that the subring is fixed elementwise by the action.

source
🔶 coverage
class IsInvariantSubring (M : Type u_1) {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (S : Subring R) :
Prop

A typeclass for subrings invariant under a MulSemiringAction.

  • smul_mem (m : M) {x : R} : x ∈ S → m • x ∈ S
Instances
    source
    🔸 coverage
    @[implicit_reducible]
    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 ↥S
    source
    🔸 coverage
    def IsInvariantSubring.subtypeHom (M : Type u_1) [Monoid M] {R' : Type u_2} [Ring R'] [MulSemiringAction M R'] (U : Subring R') [IsInvariantSubring M U] :
    ↥U →+*[M] R'

    The canonical inclusion from an invariant subring.

    Instances For
      source
      📐 coverage
      @[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] :
      ⇑(subtypeHom M U) = Subtype.val
      source
      📐 coverage
      @[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] :
      ↑(subtypeHom M U) = U.subtype