fac — Mathlib

English

For a cone s over the enriched hom diagram, the lift exhibits the correct π components at each index j.

Русский

Для конуса s над диаграммой обогащённых гом, подъём (lift) задаёт корректные π‑компоненты на каждом индексе j.

LaTeX

$$$\\text{fac}(j) : \\mathrm{lift}(s) \\;\\circ\\; \\pi_j = s_j$$$

Lean4

theorem fac (j : J) : lift s ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j :=
  by
  dsimp [coneFunctorEnrichedHom]
  ext k
  have := s.w k.hom
  dsimp at this
  simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, lift, functorEnrichedHom_obj, assoc, end_.lift_π,
    Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id, ← this,
    Under.map_obj_right, Under.mk_right]
  congr
  simp [Under.map, Comma.mapLeft]
  rfl

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