Lean4
/-- The constructed `pullbackConeOfLeft` is indeed limiting. -/
def pullbackConeOfLeftIsLimit : IsLimit (pullbackConeOfLeft f g) :=
PullbackCone.isLimitAux' _ fun s =>
by
refine
⟨LocallyRingedSpace.Hom.mk
(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.1 g.1
(PullbackCone.mk _ _ (congr_arg LocallyRingedSpace.Hom.toShHom s.condition)))
?_,
LocallyRingedSpace.Hom.ext' (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst f.1 g.1 _),
LocallyRingedSpace.Hom.ext' (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 _), ?_⟩
· intro x
have :=
PresheafedSpace.stalkMap.congr_hom _ _
(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1
(PullbackCone.mk s.fst.1 s.snd.1 (congr_arg LocallyRingedSpace.Hom.toShHom s.condition)))
x
change _ = _ ≫ s.snd.1.stalkMap x at this
rw [PresheafedSpace.stalkMap.comp, ← IsIso.eq_inv_comp] at this
rw [this]
infer_instance
· intro m _ h₂
rw [← cancel_mono (pullbackConeOfLeft f g).snd]
exact
h₂.trans <|
LocallyRingedSpace.Hom.ext'
(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg LocallyRingedSpace.Hom.toShHom s.condition).symm
