English
The snd projection in the left lift pullback is an open immersion.
Русский
В snd проекции левого подъема открытое вложение.
LaTeX
$$IsOpenImmersion (pullbackConeOfLeftLift f g).snd$$
Lean4
/-- (Implementation.) Any cone over `cospan f g` indeed factors through the constructed cone.
-/
def pullbackConeOfLeftLift : s.pt ⟶ (pullbackConeOfLeft f g).pt
where
base := pullback.lift s.fst.base s.snd.base (congr_arg (fun x => PresheafedSpace.Hom.base x) s.condition)
c :=
{ app := fun U =>
s.snd.c.app _ ≫
s.pt.presheaf.map
(eqToHom
(by
dsimp only [Opens.map, IsOpenMap.functor, Functor.op]
congr 2
let s' : PullbackCone f.base g.base :=
PullbackCone.mk s.fst.base s.snd.base (congr_arg Hom.base s.condition)
have : _ = s.snd.base := limit.lift_π s' WalkingCospan.right
conv_lhs =>
rw [← this]
dsimp [s']
rw [Function.comp_def, ← Set.preimage_preimage]
rw [Set.preimage_image_eq _ (TopCat.snd_isOpenEmbedding_of_left hf.base_open g.base).injective]
rfl))
naturality := fun U V i => by
erw [s.snd.c.naturality_assoc]
rw [Category.assoc]
erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
congr 1 }
-- this lemma is not a `simp` lemma, because it is an implementation detail
