ideal_ker_le — Mathlib

English

For any morphism f: X → Y, the range of the base map is contained in the support of the kernel of f.

Русский

Для любой стрелы f: X → Y образ на уровне базовых окружений содержится в поддержке ядра f.

LaTeX

$$\\operatorname{range}(f\\.base) \\subseteq f.\\ker.\\mathrm{support}$$

Lean4

theorem ideal_ker_le (f : X.Hom Y) (U : Y.affineOpens) : f.ker.ideal U ≤ RingHom.ker (f.app U).hom :=
  ideal_ofIdeals_le _ _

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