comap_comp — Mathlib

English

If a square with closed immersions iX, iY commutes up to Zf and a kernel equality holds, then the square is a pullback.

Русский

Если квадрат с замкнутыми вложениями iX, iY коммутирует до Zf и выполняется равенство ядер, то квадрат является вытяжкой.

LaTeX

$$$\text{IsPullback } iX Zf f iY$ given $iX ≫ f = Zf ≫ iY$ and $iY.ker.comap f = iX.ker$$$

Lean4

@[simp]
theorem comap_comp (I : Z.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z) : I.comap (f ≫ g) = (I.comap g).comap f :=
  by
  let e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
    asIso (pullback.map _ _ _ _ (𝟙 _) (I.comapIso g).hom (𝟙 _) (by simp) (by simp)) ≪≫ pullbackRightPullbackFstIso _ _ _
  rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]
  simp [e]

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