English
Under a commutative square of closed immersions with a given kernel equality, the square is a pullback.
Русский
При коммутирующем квадрате замкнутых вложений и заданном равенстве ядер квадрат является вытяжкой.
LaTeX
$$IsPullback iX Zf f iY$$
Lean4
/-- To show that the pullback of the closed immersion `iX` along `f` is the closed immersion
`iY`, it suffices to check that the preimage of `ker iY` under `f` is `ker iX`. -/
theorem _root_.AlgebraicGeometry.isPullback_of_isClosedImmersion {ZX ZY X Y : Scheme} (iX : ZX ⟶ X) (iY : ZY ⟶ Y)
(Zf : ZX ⟶ ZY) (f : X ⟶ Y) [IsClosedImmersion iX] [IsClosedImmersion iY] (h : iX ≫ f = Zf ≫ iY)
(h' : iY.ker.comap f = iX.ker) : IsPullback iX Zf f iY :=
by
suffices IsIso (pullback.lift _ _ h) by
simpa using
(IsPullback.of_vert_isIso
(show CommSq iX (pullback.lift iX Zf h) (𝟙 X) (pullback.fst _ _) from ⟨by simp⟩)).paste_vert
(IsPullback.of_hasPullback f iY)
refine IsClosedImmersion.isIso_of_ker_eq iX (pullback.fst f iY) _ (by simp) ?_
rw [ker_fst_of_isClosedImmersion, h']
