algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul

English

Let A, B be commutative semirings with A acting on B via a faithful A-module structure, and suppose S is a submonoid of A contained in the non-zero-divisors A⁰. Then the image of S under the algebra map to B consists of non-zero-divisors of B.

Русский

Пусть A, B — коммутативные полукольца, существуют скаляры A на B через верную (faithful) A-модульную структуру, и пусть S ⊆ A⁰ является подмонойдом A, заключенным в множество ненулевых делителей. Тогда образ S под алгебраическим отображением в B состоит из ненулевых делителей B.

LaTeX

$$$\operatorname{algebraMapSubmonoid} \, B \, S \leq B^0$$$

Lean4

theorem algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul {A : Type*} (B : Type*) [CommSemiring A] [CommSemiring B]
    [Algebra A B] [NoZeroDivisors B] [FaithfulSMul A B] {S : Submonoid A} (hS : S ≤ A⁰) :
    algebraMapSubmonoid B S ≤ B⁰ :=
  map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective A B) hS

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