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.

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

@[instance_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

Equations

• IsInvariantSubring.toMulSemiringAction M S = { smul := fun (m : M) (x : ↥S) => ⟨m • ↑x, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

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' := ⋯ }

@[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

@[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