eq_bot_of_comap_eq_bot — Mathlib

English

If comap of I is bottom, then I is bottom.

Русский

Если образ обратного образа I равен нулю, то сам I равен нулю.

LaTeX

$$$$I^{\mathrm{comap}} = \bot \Rightarrow I = \bot.$$$$

Lean4

theorem eq_bot_of_comap_eq_bot [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S]
    (hI : I.comap (algebraMap R S) = ⊥) : I = ⊥ :=
  by
  refine eq_bot_iff.2 fun x hx => ?_
  by_cases hx0 : x = 0
  · exact hx0.symm ▸ Ideal.zero_mem ⊥
  · exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

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