map_ne_bot_of_ne_bot — Mathlib

English

Let I be a nonzero ideal of R. Then its image under the algebra map algebraMap R S is nonzero, provided S is nontrivial and has no zero smul divisors.

Русский

Пусть I — ненулевой идеал R. Тогда его образ под алгебраическим отображением algebraMap R S не нулевой, если S ненулевое и не имеет делителей нулевого умножения.

LaTeX

$$$$ I \\neq \\bot \\Rightarrow \\operatorname{map}(\\text{algebraMap } R S)\\,I \\neq \\bot. $$$$

Lean4

theorem map_ne_bot_of_ne_bot {S : Type*} [Ring S] [Nontrivial S] [Algebra R S] [NoZeroSMulDivisors R S] {I : Ideal R}
    (h : I ≠ ⊥) : map (algebraMap R S) I ≠ ⊥ :=
  (map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)).mp.mt h

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