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) : Prop

• smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S

A typeclass for subrings invariant under a MulSemiringAction.

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

• IsInvariantSubring.toMulSemiringAction M S = MulSemiringAction.mk (_ : ∀ (m : M), m • 1 = 1) (_ : ∀ (m : M) (s₁ s₂ : { x // x ∈ S }), m • (s₁ * s₂) = m • s₁ * m • 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] : { 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.

@[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] : MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom M U) = Subring.subtype U