comapIso_inv_subschemeι — Mathlib

English

For a scheme Y with an ideal data I and a morphism f: X → Y, the relation (I.comapIso f)^{-1} followed by (I.comap f).subschemeι coincides with the first projection of the pullback.

Русский

Для схемы Y с данными идеала I и морфизмом f: X → Y, отношение (I.comapIso f)^{-1} затем (I.comap f).subschemeι совпадает с первой проекцией вытяжки.

LaTeX

$$$(I.comapIso f).inv \cdot (I.comap f).subschemeι = pullback.fst _ _$$$

Lean4

@[reassoc (attr := simp)]
theorem comapIso_inv_subschemeι (I : Y.IdealSheafData) (f : X ⟶ Y) :
    (I.comapIso f).inv ≫ (I.comap f).subschemeι = pullback.fst _ _ :=
  (pullback.fst f I.subschemeι).toImage_imageι

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