instIsIsoSchemeToImage — Mathlib

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

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