ker_fst_of_isClosedImmersion — Mathlib

English

In a pullback along a closed immersion, the kernel of fst equals the pullback of the kernel of the immersion.

Русский

При вытяжке вдоль замкнутого вложения ядро fst равно вытяжке ядра вложения.

LaTeX

$$$\ker(\text{pullback.fst } f i) = i.ker. comap f$$$

Lean4

theorem ker_fst_of_isClosedImmersion (i : Z ⟶ Y) (f : X ⟶ Y) [IsClosedImmersion i] :
    (pullback.fst f i).ker = i.ker.comap f := by
  delta IdealSheafData.comap
  rw [← Hom.ker_comp_of_isIso (pullback.map f i f i.imageι (𝟙 _) (i.toImage) (𝟙 _) (by simp) (by simp)),
    pullback.lift_fst, Category.comp_id]

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