English
If i1: Z1 → X and i2: Z2 → X are closed immersions with f: Z1 → Z2 such that f ≫ i2 = i1 and i1.ker = i2.ker, then f is an isomorphism.
Русский
Если i1, i2 — замкнутые вложения в X и f: Z1 → Z2 удовлетворяет f ≫ i2 = i1 и ядра равны, тогда f — изоморфизм.
LaTeX
$$$(i_1,i_2,f)\\text{ с } i_1.ker = i_2.ker\\Rightarrow IsIso(f)$$$
Lean4
theorem isIso_of_ker_eq {Z₁ Z₂ X : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [IsClosedImmersion i₁] [IsClosedImmersion i₂]
(f : Z₁ ⟶ Z₂) (h : f ≫ i₂ = i₁) (h' : i₁.ker = i₂.ker) : IsIso f :=
by
let f' : MorphismProperty.Over.mk ⊤ i₁ ‹_› ⟶ .mk ⊤ i₂ ‹_› := MorphismProperty.Over.homMk f h
suffices h : IsIso f'.op by
rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..), ←
isIso_iff_of_reflects_iso _ (Over.forget _)] at h
rw [← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor]
simpa [IsClosedImmersion.overEquivIdealSheafData] using ⟨homOfLE h'.le, by simp, by simp⟩
