comapIso_hom_fst — Mathlib

English

In a closed immersion square, the kernel of the fst projection in the pullback equals the comap of the kernel of i along f.

Русский

В квадрате замкнутых вложений ядро проекции fst в вытяжке равно comap ядра i по f.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem comapIso_hom_fst (I : Y.IdealSheafData) (f : X ⟶ Y) :
    (I.comapIso f).hom ≫ pullback.fst _ _ = (I.comap f).subschemeι := by
  rw [← comapIso_inv_subschemeι, Iso.hom_inv_id_assoc]

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