English
For a diagram F with shape I, the map that sends a lifted cone element along the limit lift coincides with the lifted element; i.e., the map respects the cone structure.
Русский
Для диаграммы F формы I отображение, отправляющее поднятый конусной элемент вдоль подъёма предела, совпадает с поднятым элементом; т.е. отображение сохраняет структуру конуса.
LaTeX
$$$\text{map_lift_mapCone }(c) : A.map(\lim\! (F \cdot (\pi A)) \big((\pi A).mapCone c\bigr))\; c.pt.snd = liftedConeElement F$$$
Lean4
@[simp]
theorem map_lift_mapCone (c : Cone F) : A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd = liftedConeElement F :=
by
apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective
ext i
have h₁ := congrFun (preservesLimitIso_hom_π A (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
have h₂ := (c.π.app i).property
simp_all [← FunctorToTypes.map_comp_apply, liftedConeElement]
