Theorems · Theorem · category theory

CategoryTheory.StructuredArrow.isClosedUnderLimitsOfShape

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} J] {P : CategoryTheory.MorphismProperty T} [P.RespectsIso]
  [CategoryTheory.Limits.PreservesLimitsOfShape J L] [CategoryTheory.Limits.HasLimitsOfShape J A]
  (c : (D : CategoryTheory.Functor J T) → [CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.Cone D)
  (hc :
    (D : CategoryTheory.Functor J T) →
      [inst_6 : CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.IsLimit (c D)),
  (∀ (D : CategoryTheory.Functor J T) [inst_6 : CategoryTheory.Limits.HasLimit D] {X : T}
      (s : (CategoryTheory.Functor.const J).obj X ⟶ D),
      (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })) →
    ∀ (X : T), (CategoryTheory.MorphismProperty.structuredArrowObj L P).IsClosedUnderLimitsOfShape J

Defined in

Mathlib.CategoryTheory.Limits.MorphismProperty

Cited by

0 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MorphismProperty.RespectsIsoCategoryTheory.Limits.PreservesLimitsOfShapeCategoryTheory.Limits.HasLimitsOfShape