ker_eq_top_of_isEmpty — Mathlib

English

If Y is affine, the kernel of f: X ⟶ Y is determined by the kernel of the induced ring map on global sections; explicitly, ker f = ofIdealTop( ker (f.appTop.hom) ).

Русский

Если Y аффинна, ядро f определяется по ядру сопряжённого кольмона на глобальных секциях: ker f = ofIdealTop( ker (f.appTop.hom) ).

LaTeX

$$f.\\ker = \\mathrm{ofIdealTop}(\\ker(f.appTop.hom))$$

Lean4

theorem ker_eq_top_of_isEmpty (f : X.Hom Y) [IsEmpty X] : f.ker = ⊤ :=
  top_le_iff.mp (le_ofIdeals_iff.mpr fun U x _ ↦ by simpa using Subsingleton.elim _ _)

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