Mathlib.Algebra.Ring.Action.Invariant

Module docstring

{"# 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.

IsInvariantSubring structure

Full source

/-- A typeclass for subrings invariant under a `MulSemiringAction`. -/
class IsInvariantSubring : Prop where
  smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S

Invariant Subring under Monoid Action

Informal description

A subring $ S $ of a ring $ R $ is called *invariant under a monoid action* if for every element $ m $ in the monoid $ M $ and every element $ s $ in $ S $, the action of $ m $ on $ s $ (denoted $ m \cdot s $) remains in $ S $. This means the subring $ S $ is fixed elementwise by the action of $ M $.

IsInvariantSubring.toMulSemiringAction instance

[IsInvariantSubring M S] : MulSemiringAction M S

Full source

instance IsInvariantSubring.toMulSemiringAction [IsInvariantSubring M S] :
    MulSemiringAction M S where
  smul m x := ⟨m • ↑x, IsInvariantSubring.smul_mem m x.2⟩
  one_smul s := Subtype.eq <| one_smul M (s : R)
  mul_smul m₁ m₂ s := Subtype.eq <| mul_smul m₁ m₂ (s : R)
  smul_add m s₁ s₂ := Subtype.eq <| smul_add m (s₁ : R) (s₂ : R)
  smul_zero m := Subtype.eq <| smul_zero m
  smul_one m := Subtype.eq <| smul_one m
  smul_mul m s₁ s₂ := Subtype.eq <| smul_mul' m (s₁ : R) (s₂ : R)

Multiplicative Semiring Action on Invariant Subrings

Informal description

For any monoid $M$ acting on a ring $R$ via a multiplicative semiring action, if a subring $S$ of $R$ is invariant under this action, then $S$ inherits a multiplicative semiring action from $M$.

IsInvariantSubring.subtypeHom definition

: U →+*[M] R'

Full source

/-- The canonical inclusion from an invariant subring. -/
def IsInvariantSubring.subtypeHom : U →+*[M] R' :=
  { U.subtype with map_smul' := fun _ _ ↦ rfl }

Equivariant inclusion of an invariant subring

Informal description

Given a monoid $M$ acting on a ring $R$ via a multiplicative semiring action, and an invariant subring $U$ of $R$ (meaning $m \cdot u \in U$ for all $m \in M$ and $u \in U$), the canonical inclusion homomorphism from $U$ to $R$ is equivariant with respect to the action of $M$. This means the inclusion map preserves both the ring structure and the action of $M$, where the action on $U$ is the restriction of the action on $R$.

IsInvariantSubring.coe_subtypeHom theorem

: (IsInvariantSubring.subtypeHom M U : U → R') = Subtype.val

Full source

@[simp]
theorem IsInvariantSubring.coe_subtypeHom :
    (IsInvariantSubring.subtypeHom M U : U → R') = Subtype.val := rfl

Underlying Function of Equivariant Inclusion Homomorphism for Invariant Subrings

Informal description

Let $M$ be a monoid acting on a ring $R$ via a multiplicative semiring action, and let $U$ be an invariant subring of $R$ under this action. The underlying function of the equivariant inclusion homomorphism from $U$ to $R$ is equal to the canonical inclusion map $\text{Subtype.val} \colon U \to R$.

IsInvariantSubring.coe_subtypeHom' theorem

: ((IsInvariantSubring.subtypeHom M U) : U →+* R') = U.subtype

Full source

@[simp]
theorem IsInvariantSubring.coe_subtypeHom' :
    ((IsInvariantSubring.subtypeHom M U) : U →+* R') = U.subtype := rfl

Equivariant inclusion homomorphism coincides with canonical inclusion for invariant subrings

Informal description

The underlying ring homomorphism of the equivariant inclusion homomorphism from an invariant subring $U$ to the ring $R'$ is equal to the canonical inclusion homomorphism of $U$ into $R'$.