coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation

English

An auxiliary construction to relate a diagram functor and a cone after evaluating at a cover, used to prove preservation of limits by a diagram functor.

Русский

Вспомогательное построение для связи диаграммного функтора и конуса после оценки над покрытием, используемое при доказательстве сохранения предelиментов диаграммным фактором.

LaTeX

$$$\text{coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation}$$$

Lean4

/-- An auxiliary definition to be used in the proof of the fact that
`J.diagramFunctor D X` preserves limits. -/
@[simps]
def coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation {X : C} {K : Type s} [SmallCategory K] {F : K ⥤ Cᵒᵖ ⥤ D}
    {W : J.Cover X} (i : W.Arrow) (E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))) :
    Cone (F ⋙ (evaluation _ _).obj (op i.Y)) where
  pt := E.pt
  π :=
    { app := fun k => E.π.app k ≫ Multiequalizer.ι (W.index (F.obj k)) i
      naturality := by
        intro a b f
        dsimp
        rw [Category.id_comp, Category.assoc, ← E.w f]
        dsimp [diagramNatTrans]
        simp only [Multiequalizer.lift_ι, Category.assoc] }

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