functorCategory — Mathlib

English

If W is stable under limits of shape K, then (W.functorCategory J) is stable under limits of shape K.

Русский

Если W устойчиво к пределам формы K, то (W.functorCategory J) устойчиво к пределам формы K.

LaTeX

$$$W.IsStableUnderLimitsOfShape K ⇒ (W.functorCategory J).IsStableUnderLimitsOfShape K$$$

Lean4

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

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