Documentation

Mathlib.Algebra.Ring.Action.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) :

A typeclass for subrings invariant under a MulSemiringAction.

  • smul_mem : ∀ (m : M) {x : R}, x Sm x S
Instances
    theorem IsInvariantSubring.smul_mem {M : Type u_1} {R : Type u_2} :
    ∀ {inst : Monoid M} {inst_1 : Ring R} {inst_2 : MulSemiringAction M R} {S : Subring R} [self : IsInvariantSubring M S] (m : M) {x : R}, x Sm x S
    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.

    Equations
    • IsInvariantSubring.subtypeHom M U = { toFun := (↑U.subtype).toFun, map_smul' := , map_zero' := , map_add' := , map_one' := , map_mul' := }
    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
      @[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).toRingHom = U.subtype