Theorems · Inductive type · category theory
CategoryTheory.Limits.ReflectsFiniteColimits
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → PropA functor is said to reflect finite colimits, if it reflects all colimits of shape J,
where J : Type is a finite category.
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
Cited by21
Results whose statement or proof uses this declaration.
- CategoryTheory.HasExactLimitsOfShape.domain_of_functorstatement and proof · cited by 1
- CategoryTheory.Limits.ReflectsFiniteColimits.casesOnstatement and proof · cited by 0
- CategoryTheory.Limits.ReflectsFiniteColimits.recOnstatement and proof · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_leftOpstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_of_leftOpstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_of_opstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_of_rightOpstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_of_unopstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_opstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_rightOpstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteColimits_unopstatement · cited by 0
- CategoryTheory.Limits.reflectsFiniteLimits_leftOpstatement and proof · cited by 0