map_π_liftedConeElement — Mathlib

English

For each index i, mapping by π_i on the lifted cone yields the i-th component of F applied to the diagram.

Русский

Для каждого индекса i отображение π_i на поднятом конусе даёт i-ю компоненту F от диаграммы.

LaTeX

$$$\forall i:\, I,\ A.map (\mathrm{limit.\pi}(F \circ (\mathrm{CategoryOfElements.\pi } A)) i) (\mathrm{liftedConeElement} F) = (F.obj i).snd$$$

Lean4

@[simp]
theorem map_π_liftedConeElement (i : I) : A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd :=
  by
  have := congrFun (preservesLimitIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)
  simp_all [liftedConeElement]

Похожие утверждения