algebraMap_mem_graded — Mathlib

English

In a graded setting, the image of the base algebra under algebraMap lands in the degree-zero component.

Русский

В градационной системе образ алгебры через algebraMap лежит в нулевой компоненте.

LaTeX

$$$\text{algebraMap } S \to R(s) \in A_0$$$

Lean4

theorem algebraMap_mem_graded [Zero ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R)
    [SetLike.GradedOne A] (s : S) : algebraMap S R s ∈ A 0 :=
  by
  rw [Algebra.algebraMap_eq_smul_one]
  exact (A 0).smul_mem s <| SetLike.one_mem_graded _

Похожие утверждения