closure_range_comap — Mathlib

English

The closure of the range of comap f is equal to the zero locus of the radical of ker f.

Русский

Замыкание образа comap f совпадает с нулевой локус по радикалу ядра f.

LaTeX

$$$$ \mathrm{closure}(\operatorname{range}(\operatorname{comap} f)) = \mathrm{zeroLocus}(\operatorname{radical}(\ker f)). $$$$

Lean4

theorem closure_range_comap : closure (Set.range (comap f)) = zeroLocus (RingHom.ker f) := by
  rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_range_comap, zeroLocus_radical]

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