ofRestrict — Mathlib

English

The left projection in the left pullback cone is an open immersion.

Русский

Левая проекция в левой предельной схеме открытого вложения является открытым вложением.

LaTeX

$$IsOpenImmersion (pullbackConeOfLeft f g).fst$$

Lean4

instance ofRestrict {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier} (hf : IsOpenEmbedding f) :
    IsOpenImmersion (Y.ofRestrict hf) where
  base_open := hf
  c_iso
    U := by
    dsimp
    have : (Opens.map f).obj (hf.isOpenMap.functor.obj U) = U :=
      by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    convert_to IsIso (Y.presheaf.map (𝟙 _))
    · congr
    · -- Porting note: was `apply Subsingleton.helim; rw [this]`
            -- See https://github.com/leanprover/lean4/issues/2273

      congr
      · simp only
        congr
      apply Subsingleton.helim
      rw [this]
    · infer_instance

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