pullbackConeOfLeft — Mathlib

Lean4
/-- An explicit pullback cone over `cospan f g` if `f` is an open immersion. -/
def pullbackConeOfLeft : PullbackCone f g :=
  by
  refine PullbackCone.mk ?_ (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_
  · use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1
    intro x
    have :=
      PresheafedSpace.stalkMap.congr_hom _ _ (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition f.1 g.1) x
    rw [PresheafedSpace.stalkMap.comp, PresheafedSpace.stalkMap.comp] at this
    rw [← IsIso.eq_inv_comp] at this
    rw [this]
    dsimp
    infer_instance
  · exact LocallyRingedSpace.Hom.ext' (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)
Похожие утверждения