instFaithfulSMulCore — Mathlib

English

Let R and S be commutative rings with R-algebra structure on S, and P be an algebra presentation over R. Then the core subalgebra P.Core has a faithful action of R, i.e., the scalar action of R on P.Core is injective.

Русский

Пусть R и S — коммутативные кольца, на S задана структура R-алгебры, и P — презентация по отношению к R. Тогда ядро P-Core имеет верное действие скаляров R, то есть действие R на P.Core является инъективным.

LaTeX

$$$\\forall r \\in R,\\ (\\forall x \\in P^{\\mathrm{Core}},\\ r \\cdot x = 0) \\Rightarrow r = 0$$$

Lean4

instance : FaithfulSMul P.Core R :=
  inferInstanceAs <| FaithfulSMul P.core R

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