English
The forgetful functor from the open immersion world to the base category preserves limits that arise from the left hand side of a pullback diagram.
Русский
Обратная по отношению к открытому вложению очистка сохраняет пределы, полученные слева от диаграммы pullback.
LaTeX
$$$\text{PreservesLimit}(\mathrm{cospan}\ f\ g,\ \mathrm{forget})$$$
Lean4
instance forget_preservesLimitsOfLeft : PreservesLimit (cospan f g) (forget C) :=
preservesLimit_of_preserves_limit_cone (pullbackConeOfLeftIsLimit f g)
(by
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).toFun
refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))
fapply Cones.ext
· exact Iso.refl _
change ∀ j, _ = 𝟙 _ ≫ _ ≫ _
simp_rw [Category.id_comp]
rintro (_ | _ | _) <;> symm
· simp only [limit.cone_x, Functor.const_obj_obj, cospan_one, Functor.comp_obj, forget_obj, Functor.mapCone_pt,
Functor.mapCone_π_app, PullbackCone.condition_one, forget_map, comp_base, cospan_left, cospan_right,
Functor.comp_map, cospan_map_inl, cospan_map_inr, diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]
tauto
· exact Category.comp_id _
· exact Category.comp_id _)
