vanishingIdeal_range_comap — Mathlib

English

For a ring hom f, the vanishing ideal of the range of comap f equals the radical of the kernel of f.

Русский

Для гомоморфизма f: R→S: vanishingIdeal(Set.range(comap f)) = Rad(ker f).

LaTeX

$$$$ \operatorname{vanishingIdeal}(\operatorname{Set.range}(\operatorname{comap} f)) = \operatorname{radical}(\ker f). $$$$

Lean4

theorem vanishingIdeal_range_comap : vanishingIdeal (Set.range (comap f)) = (RingHom.ker f).radical :=
  by
  ext x
  rw [RingHom.ker_eq_comap_bot, ← Ideal.comap_radical, Ideal.radical_eq_sInf]
  simp only [mem_vanishingIdeal, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff, comap_asIdeal,
    Ideal.mem_comap, bot_le, true_and, Submodule.mem_sInf, Set.mem_setOf_eq]
  exact ⟨fun H I hI ↦ H ⟨I, hI⟩, fun H I ↦ H I.1 I.2⟩

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