Theorems · Theorem · category theory

CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T}
  [CategoryTheory.Limits.HasPullbacks A] [CategoryTheory.Limits.HasPullbacks T]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan L] (X : T)
  [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderLimitsOfShape
    CategoryTheory.Limits.WalkingCospan

Defined in

Mathlib.CategoryTheory.Limits.MorphismProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.PreservesLimitsOfShapeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.HasOfPostcompProperty