English
A closed immersion f: X → Y is an isomorphism onto its image.
Русский
Замкнутое вложение f: X → Y есть изоморфизм от X к образу f.
LaTeX
$$$IsClosedImmersion(f)\\Rightarrow IsIso(f^{\\text{toImage}}).$$$
Lean4
instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f] : IsIso f.toImage :=
by
have :=
@of_comp_isClosedImmersion _ _ _ f.toImage f.imageι inferInstance
(by rw [Scheme.Hom.toImage_imageι]; infer_instance)
have : IsHomeomorph f.toImage.base :=
isHomeomorph_iff_isEmbedding_surjective.mpr
⟨f.toImage.isEmbedding,
by
rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
exact f.toImage.denseRange.closure_eq⟩
refine isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩
· exact inferInstanceAs (IsIso (TopCat.isoOfHomeo this.homeomorph).hom)
· intro x
refine ⟨?_, f.toImage.stalkMap_surjective x⟩
change
Function.Injective
(CommRingCat.Hom.hom
(((TopCat.Presheaf.stalkFunctor CommRingCat (f.toImage.base x)).map f.toImage.c) ≫
X.presheaf.stalkPushforward _ _ x))
simp only [TopCat.Presheaf.stalkFunctor_obj, CommRingCat.hom_comp, RingHom.coe_comp]
refine .comp ?_ (f.stalkFunctor_toImage_injective _)
have :=
TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing CommRingCat (f := f.toImage.base)
f.toImage.isEmbedding.isInducing X.presheaf x
exact ((ConcreteCategory.isIso_iff_bijective _).mp this).1