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)
:
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 ↥S
Equations
- IsInvariantSubring.toMulSemiringAction M S = { smul := fun (m : M) (x : ↥S) => ⟨m • ↑x, ⋯⟩, one_smul := ⋯, mul_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]
:
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]
:
@[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]
: