functorCategory — Mathlib

English

For any K, if W is stable under limits of shape K, then the functor category W.functorCategory J is stable under limits of shape K.

Русский

Для любого K, если W устойчиво к пределам формы K, то категория-функтор W.functorCategory J устойчива к пределам формы K.

LaTeX

$$$\forall K, (W.IsStableUnderLimitsOfShape K) \Rightarrow (W.functorCategory J).IsStableUnderLimitsOfShape K$$$

Lean4

instance functorCategory {K : Type u'} [Category.{v'} K] [W.IsStableUnderColimitsOfShape K] (J : Type u'')
    [Category.{v''} J] [HasColimitsOfShape K C] : (W.functorCategory J).IsStableUnderColimitsOfShape K where
  condition X₁ X₂ _ _ hc₁ hc₂ f hf φ hφ
    j :=
    MorphismProperty.colimitsOfShape_le _
      (colimitsOfShape.mk' (X₁ ⋙ (evaluation _ _).obj j) (X₂ ⋙ (evaluation _ _).obj j) _ _ (isColimitOfPreserves _ hc₁)
        (isColimitOfPreserves _ hc₂) (Functor.whiskerRight f _) (fun k ↦ hf k j) (φ.app j) (fun k ↦ congr_app (hφ k) j))

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