Theorems · Theorem · category theory
CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [F.IsCardinalAccessible κ]
(J : Type w) [inst_4 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ],
CategoryTheory.Limits.PreservesColimitsOfShape J F- Defined in
- Mathlib.CategoryTheory.Presentable.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Factstatement and proof · cited by 2,726
- Cardinalstatement and proof · cited by 2,598
- CategoryTheory.SmallCategorystatement and proof · cited by 480
- Cardinal.IsRegularstatement and proof · cited by 282
- CategoryTheory.Limits.PreservesColimitsOfShapestatement · cited by 222
- CategoryTheory.IsCardinalFilteredstatement and proof · cited by 69
- CategoryTheory.Functor.IsCardinalAccessiblestatement and proof · cited by 19
- CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShapeproof · cited by 1
Cited by6
Results whose statement or proof uses this declaration.
- CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentableproof · cited by 2
- CategoryTheory.Functor.isCardinalAccessible_of_natIsoproof · cited by 2
- CategoryTheory.Functor.isCardinalAccessible_of_leproof · cited by 1
- CategoryTheory.Functor.isCardinalAccessible_of_isLimitproof · cited by 1