comap_ne_bot — Mathlib

English

If I is nonzero and algebraic over R in S, then its comap is nonzero.

Русский

Если I неравно нулю и алгебраически над R в S, то его образ по обратному образу не равен нулю.

LaTeX

$$$$I \neq 0 \Rightarrow I^{\mathrm{comap}} \neq \bot.$$$$

Lean4

theorem comap_ne_bot [Nontrivial R] {I : Ideal A} (I_ne_bot : I ≠ ⊥) : I.comap (algebraMap R A) ≠ ⊥ :=
  let ⟨x, x_mem, x_ne_zero⟩ := I.ne_bot_iff.mp I_ne_bot
  comap_ne_bot_of_integral_mem x_ne_zero x_mem (IsIntegralClosure.isIntegral R S x)

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