Structures · Category theory
CategoryTheory.CreatesColimit
Dual of definition 3.3.1 of [Riehl].
We say that F creates colimits of K if, given any limit cocone c for
K ⋙ F (i.e. below) we can lift it to a cocone "above", and further that F
reflects limits for K.
If F reflects isomorphisms, it suffices to show only that the lifted cocone is
a limit - see createsColimitOfReflectsIso.
- Defined in
- Mathlib.CategoryTheory.Limits.Creates
- Shape
- 2 explicit arguments · adds lifts
Extends1
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- AlgebraicGeometry.Scheme
- CategoryTheory.CostructuredArrow
- CategoryTheory.Monad.Algebra
- CategoryTheory.MorphismProperty.Over
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- CategoryTheory.hasColimit_of_created
- CategoryTheory.liftColimit
- CategoryTheory.liftedColimitIsColimit
- CategoryTheory.Limits.HasPushout.of_createsColimit
- CategoryTheory.inhabitedLiftsToColimit
- CategoryTheory.Limits.createsLimitUnop
- CategoryTheory.liftsToColimitOfCreates
- CategoryTheory.Limits.createsLimitOp
- CategoryTheory.Limits.createsLimitOfRightOp
- CategoryTheory.liftedColimitMapsToOriginal
- CategoryTheory.CreatesColimit.toReflectsColimit
- CategoryTheory.Limits.createsLimitLeftOp
- CategoryTheory.Limits.createsLimitOfLeftOp
- CategoryTheory.CreatesColimit.lifts
- CategoryTheory.Functor.Final.createsColimitOfComp
- CategoryTheory.Limits.createsLimitOfOp
- CategoryTheory.createsColimitOfIsoDiagram
- CategoryTheory.Limits.createsLimitOfUnop
- CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
- CategoryTheory.Functor.Final.compCreatesColimit
- CategoryTheory.preservesColimit_comp_of_createsColimit
- CategoryTheory.compCreatesColimit
- CategoryTheory.createsColimitOfNatIso
- CategoryTheory.Limits.createsLimitRightOp