Module docstring
{"# Creating (co)limits
We say that F creates limits of K if, given any limit cone c for K ⋙ F
(i.e. below) we can lift it to a cone \"above\", and further that F reflects
limits for K.
"}
CategoryTheory.LiftableCone
structure
(K : J ⥤ C) (F : C ⥤ D) (c : Cone (K ⋙ F))
Full source
/-- Define the lift of a cone: For a cone `c` for `K ⋙ F`, give a cone for `K`
which is a lift of `c`, i.e. the image of it under `F` is (iso) to `c`.
We will then use this as part of the definition of creation of limits:
every limit cone has a lift.
Note this definition is really only useful when `c` is a limit already.
-/
structure LiftableCone (K : J ⥤ C) (F : C ⥤ D) (c : Cone (K ⋙ F)) where
/-- a cone in the source category of the functor -/
liftedCone : Cone K
/-- the isomorphism expressing that `liftedCone` lifts the given cone -/
validLift : F.mapCone liftedCone ≅ cInformal description
Given a functor $F \colon C \to D$ and a diagram $K \colon J \to C$, a `LiftableCone` structure provides a way to lift a cone $c$ over the composition $K \circ F$ to a cone over $K$ itself, such that the image of this lifted cone under $F$ is isomorphic to $c$. This is particularly meaningful when $c$ is already a limit cone.
CategoryTheory.LiftableCocone
structure
(K : J ⥤ C) (F : C ⥤ D) (c : Cocone (K ⋙ F))
Full source
/-- Define the lift of a cocone: For a cocone `c` for `K ⋙ F`, give a cocone for
`K` which is a lift of `c`, i.e. the image of it under `F` is (iso) to `c`.
We will then use this as part of the definition of creation of colimits:
every limit cocone has a lift.
Note this definition is really only useful when `c` is a colimit already.
-/
structure LiftableCocone (K : J ⥤ C) (F : C ⥤ D) (c : Cocone (K ⋙ F)) where
/-- a cocone in the source category of the functor -/
liftedCocone : Cocone K
/-- the isomorphism expressing that `liftedCocone` lifts the given cocone -/
validLift : F.mapCocone liftedCocone ≅ cInformal description
Given a functor \( F : C \to D \) and a diagram \( K : J \to C \), a structure that provides a lift of a colimit cocone \( c \) for the composition \( K \circ F \) to a cocone for \( K \). This means there exists a cocone for \( K \) whose image under \( F \) is isomorphic to \( c \). This structure is particularly useful when \( c \) is already a colimit cocone, as part of the definition of colimit creation by \( F \).
CategoryTheory.CreatesLimit
structure
(K : J ⥤ C) (F : C ⥤ D) extends ReflectsLimit K F
Full source
/-- Definition 3.3.1 of [Riehl].
We say that `F` creates limits of `K` if, given any limit cone `c` for `K ⋙ F`
(i.e. below) we can lift it to a cone "above", and further that `F` reflects
limits for `K`.
If `F` reflects isomorphisms, it suffices to show only that the lifted cone is
a limit - see `createsLimitOfReflectsIso`.
-/
class CreatesLimit (K : J ⥤ C) (F : C ⥤ D) extends ReflectsLimit K F where
/-- any limit cone can be lifted to a cone above -/
lifts : ∀ c, IsLimit c → LiftableCone K F cInformal description
A functor $F \colon C \to D$ creates limits of a diagram $K \colon J \to C$ if, given any limit cone for the composition $K \circ F$ in $D$, there exists a lift of this cone to a cone in $C$ over $K$, and furthermore $F$ reflects limits of $K$.
If $F$ reflects isomorphisms, it is sufficient to verify that the lifted cone is a limit in $C$.
CategoryTheory.CreatesLimitsOfShape
structure
(J : Type w) [Category.{w'} J] (F : C ⥤ D)
Full source
/-- `F` creates limits of shape `J` if `F` creates the limit of any diagram
`K : J ⥤ C`.
-/
class CreatesLimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) where
CreatesLimit : ∀ {K : J ⥤ C}, CreatesLimit K F := by infer_instanceInformal description
A functor $F \colon C \to D$ creates limits of shape $J$ if, for any diagram $K \colon J \to C$, the functor $F$ can lift any limit cone of the composition $K \circ F$ to a limit cone of $K$ in $C$, and $F$ reflects limits for $K$.
CategoryTheory.CreatesLimitsOfSize
structure
(F : C ⥤ D)
Full source
/-- `F` creates limits if it creates limits of shape `J` for any `J`. -/
@[nolint checkUnivs, pp_with_univ]
class CreatesLimitsOfSize (F : C ⥤ D) where
CreatesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], CreatesLimitsOfShape J F := by
infer_instanceInformal description
A functor $F \colon C \to D$ creates limits of any size if, given any limit cone in $D$ for the composition $K \circ F$ (where $K$ is a diagram in $C$), there exists a lift to a limit cone in $C$, and $F$ reflects limits for $K$.
CategoryTheory.CreatesLimits
abbrev
(F : C ⥤ D)
Full source
/-- `F` creates small limits if it creates limits of shape `J` for any small `J`. -/
abbrev CreatesLimits (F : C ⥤ D) :=
CreatesLimitsOfSize.{v₂, v₂} FInformal description
A functor $F \colon C \to D$ creates small limits if, for any small category $J$ and any diagram $K \colon J \to C$, given a limit cone for the composition $K \circ F \colon J \to D$, there exists a lift to a limit cone for $K$ in $C$, and $F$ reflects limits for $K$.
CategoryTheory.CreatesColimit
structure
(K : J ⥤ C) (F : C ⥤ D) extends ReflectsColimit K F
Full source
/-- 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`.
-/
class CreatesColimit (K : J ⥤ C) (F : C ⥤ D) extends ReflectsColimit K F where
/-- any limit cocone can be lifted to a cocone above -/
lifts : ∀ c, IsColimit c → LiftableCocone K F cInformal description
A functor $F \colon C \to D$ creates colimits of a diagram $K \colon J \to C$ if, given any colimit cocone for the composition $K \circ F \colon J \to D$, there exists a colimit cocone for $K$ that is mapped by $F$ to the given cocone, and $F$ reflects colimits of $K$.
CategoryTheory.CreatesColimitsOfShape
structure
(J : Type w) [Category.{w'} J] (F : C ⥤ D)
Full source
/-- `F` creates colimits of shape `J` if `F` creates the colimit of any diagram
`K : J ⥤ C`.
-/
class CreatesColimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) where
CreatesColimit : ∀ {K : J ⥤ C}, CreatesColimit K F := by infer_instanceInformal description
A functor $F \colon C \to D$ creates colimits of shape $J$ if for any diagram $K \colon J \to C$, the functor $F$ can lift any colimit cone of the composed diagram $K \circ F$ to a colimit cone of $K$ in $C$, and $F$ reflects colimits for $K$.
CategoryTheory.CreatesColimitsOfSize
structure
(F : C ⥤ D)
Full source
/-- `F` creates colimits if it creates colimits of shape `J` for any small `J`. -/
@[nolint checkUnivs, pp_with_univ]
class CreatesColimitsOfSize (F : C ⥤ D) where
CreatesColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], CreatesColimitsOfShape J F := by
infer_instanceInformal description
A functor $F \colon C \to D$ creates colimits of any size if, given any colimit cocone for the composition $K \circ F$ (where $K$ is a functor from some small category $J$ to $C$), there exists a colimit cocone for $K$ that maps to the original cocone under $F$, and $F$ reflects colimits for $K$.
CategoryTheory.CreatesColimits
abbrev
(F : C ⥤ D)
Full source
/-- `F` creates small colimits if it creates colimits of shape `J` for any small `J`. -/
abbrev CreatesColimits (F : C ⥤ D) :=
CreatesColimitsOfSize.{v₂, v₂} FInformal description
A functor $F \colon C \to D$ creates small colimits if, for any small category $J$ and any diagram $K \colon J \to C$, given a colimit cocone for the composition $K \circ F$ in $D$, there exists a colimit cocone for $K$ in $C$ that maps to the original cocone under $F$, and $F$ reflects colimits for $K$.
CategoryTheory.liftLimit
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) : Cone K
Full source
/-- `liftLimit t` is the cone for `K` given by lifting the limit `t` for `K ⋙ F`. -/
def liftLimit {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) :
Cone K :=
(CreatesLimit.lifts c t).liftedConeInformal description
Given a functor $F \colon C \to D$ that creates limits of a diagram $K \colon J \to C$, and given a limit cone $c$ for the composition $K \circ F$ in $D$ with proof $t$ that $c$ is indeed a limit, the function `liftLimit` constructs a cone for $K$ in $C$ that lifts $c$ through $F$.
CategoryTheory.liftedLimitMapsToOriginal
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) : F.mapCone (liftLimit t) ≅ c
Full source
/-- The lifted cone has an image isomorphic to the original cone. -/
def liftedLimitMapsToOriginal {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)}
(t : IsLimit c) : F.mapCone (liftLimit t) ≅ c :=
(CreatesLimit.lifts c t).validLiftInformal description
Given a functor $F \colon C \to D$ that creates limits of a diagram $K \colon J \to C$, and given a limit cone $c$ for the composition $K \circ F$ in $D$ with proof $t$ that $c$ is indeed a limit, the image of the lifted cone under $F$ is isomorphic to the original cone $c$.
In other words, the isomorphism `liftedLimitMapsToOriginal` witnesses that the cone obtained by applying $F$ to the lifted limit cone is isomorphic to the original limit cone in $D$.
CategoryTheory.liftedLimitMapsToOriginal_inv_map_π
theorem
{K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) (j : J) :
(liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j
Full source
lemma liftedLimitMapsToOriginal_inv_map_π
{K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) (j : J) :
(liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j := by
rw [show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j
from (by simp), ← Category.assoc, ← Cone.category_comp_hom]
simpInformal description
Given a functor $F \colon C \to D$ that creates limits of a diagram $K \colon J \to C$, a limit cone $c$ for the composition $K \circ F$ with proof $t$ that $c$ is a limit, and an object $j \in J$, the inverse of the isomorphism `liftedLimitMapsToOriginal` composed with the image under $F$ of the projection morphism from the lifted cone at $j$ equals the projection morphism from $c$ at $j$.
In symbols, if $\varphi$ denotes the isomorphism `liftedLimitMapsToOriginal`, then $\varphi^{-1} \circ F(\pi_j) = \pi_j$, where $\pi_j$ is the projection from the (lifted) cone at $j$.
CategoryTheory.liftedLimitIsLimit
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) : IsLimit (liftLimit t)
Full source
/-- The lifted cone is a limit. -/
def liftedLimitIsLimit {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)}
(t : IsLimit c) : IsLimit (liftLimit t) :=
isLimitOfReflects _ (IsLimit.ofIsoLimit t (liftedLimitMapsToOriginal t).symm)Informal description
Given a functor \( F \colon C \to D \) that creates limits of a diagram \( K \colon J \to C \), and given a limit cone \( c \) for the composition \( K \circ F \) in \( D \) with proof \( t \) that \( c \) is indeed a limit, the lifted cone \( \text{liftLimit } t \) is a limit cone in \( C \).
This is established by reflecting the limit property through \( F \) and using the isomorphism between the image of the lifted cone and the original cone \( c \).
CategoryTheory.hasLimit_of_created
theorem
(K : J ⥤ C) (F : C ⥤ D) [HasLimit (K ⋙ F)] [CreatesLimit K F] : HasLimit K
Full source
/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit. -/
theorem hasLimit_of_created (K : J ⥤ C) (F : C ⥤ D) [HasLimit (K ⋙ F)] [CreatesLimit K F] :
HasLimit K :=
HasLimit.mk
{ cone := liftLimit (limit.isLimit (K ⋙ F))
isLimit := liftedLimitIsLimit _ }Informal description
Given a diagram $K \colon J \to C$ and a functor $F \colon C \to D$, if the composition $K \circ F$ has a limit and $F$ creates the limit of $K$, then $K$ has a limit in $C$.
CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
theorem
(F : C ⥤ D) [HasLimitsOfShape J D] [CreatesLimitsOfShape J F] : HasLimitsOfShape J C
Full source
/-- If `F` creates limits of shape `J`, and `D` has limits of shape `J`, then
`C` has limits of shape `J`.
-/
theorem hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (F : C ⥤ D) [HasLimitsOfShape J D]
[CreatesLimitsOfShape J F] : HasLimitsOfShape J C :=
⟨fun G => hasLimit_of_created G F⟩Informal description
Let $F \colon C \to D$ be a functor between categories. If $D$ has limits of shape $J$ and $F$ creates limits of shape $J$, then $C$ has limits of shape $J$.
CategoryTheory.hasLimits_of_hasLimits_createsLimits
theorem
(F : C ⥤ D) [HasLimitsOfSize.{w, w'} D] [CreatesLimitsOfSize.{w, w'} F] : HasLimitsOfSize.{w, w'} C
Full source
/-- If `F` creates limits, and `D` has all limits, then `C` has all limits. -/
theorem hasLimits_of_hasLimits_createsLimits (F : C ⥤ D) [HasLimitsOfSize.{w, w'} D]
[CreatesLimitsOfSize.{w, w'} F] : HasLimitsOfSize.{w, w'} C :=
⟨fun _ _ => hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape F⟩Informal description
Let $F \colon C \to D$ be a functor between categories. If $D$ has all limits (of any size) and $F$ creates all limits (of any size), then $C$ has all limits (of any size).
CategoryTheory.liftColimit
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)} (t : IsColimit c) : Cocone K
Full source
/-- `liftColimit t` is the cocone for `K` given by lifting the colimit `t` for `K ⋙ F`. -/
def liftColimit {K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)}
(t : IsColimit c) : Cocone K :=
(CreatesColimit.lifts c t).liftedCoconeInformal description
Given a functor \( F \colon C \to D \) that creates colimits of a diagram \( K \colon J \to C \), and a colimit cocone \( c \) for the composition \( K \circ F \colon J \to D \), the construction `liftColimit t` produces a cocone for \( K \) that is mapped by \( F \) to \( c \). This cocone is obtained by lifting the colimit data from \( D \) back to \( C \).
CategoryTheory.liftedColimitMapsToOriginal
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)} (t : IsColimit c) : F.mapCocone (liftColimit t) ≅ c
Full source
/-- The lifted cocone has an image isomorphic to the original cocone. -/
def liftedColimitMapsToOriginal {K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)}
(t : IsColimit c) : F.mapCocone (liftColimit t) ≅ c :=
(CreatesColimit.lifts c t).validLiftInformal description
Given a functor \( F \colon C \to D \) that creates colimits of a diagram \( K \colon J \to C \), and a colimit cocone \( c \) for the composition \( K \circ F \colon J \to D \), the image of the lifted cocone \( \text{liftColimit } t \) under \( F \) is isomorphic to the original cocone \( c \).
CategoryTheory.liftedColimitIsColimit
definition
{K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)} (t : IsColimit c) : IsColimit (liftColimit t)
Full source
/-- The lifted cocone is a colimit. -/
def liftedColimitIsColimit {K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)}
(t : IsColimit c) : IsColimit (liftColimit t) :=
isColimitOfReflects _ (IsColimit.ofIsoColimit t (liftedColimitMapsToOriginal t).symm)Informal description
Given a functor \( F \colon C \to D \) that creates colimits of a diagram \( K \colon J \to C \), and a colimit cocone \( c \) for the composition \( K \circ F \colon J \to D \), the lifted cocone \( \text{liftColimit } t \) is a colimit cocone for \( K \). This means that the colimit property is preserved when lifting the colimit data from \( D \) back to \( C \).
CategoryTheory.hasColimit_of_created
theorem
(K : J ⥤ C) (F : C ⥤ D) [HasColimit (K ⋙ F)] [CreatesColimit K F] : HasColimit K
Full source
/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit. -/
theorem hasColimit_of_created (K : J ⥤ C) (F : C ⥤ D) [HasColimit (K ⋙ F)] [CreatesColimit K F] :
HasColimit K :=
HasColimit.mk
{ cocone := liftColimit (colimit.isColimit (K ⋙ F))
isColimit := liftedColimitIsColimit _ }Informal description
Let $K \colon J \to C$ be a diagram and $F \colon C \to D$ a functor that creates colimits of $K$. If the composition $K \circ F \colon J \to D$ has a colimit, then $K$ has a colimit in $C$.
CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape
theorem
(F : C ⥤ D) [HasColimitsOfShape J D] [CreatesColimitsOfShape J F] : HasColimitsOfShape J C
Full source
/-- If `F` creates colimits of shape `J`, and `D` has colimits of shape `J`, then
`C` has colimits of shape `J`.
-/
theorem hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (F : C ⥤ D)
[HasColimitsOfShape J D] [CreatesColimitsOfShape J F] : HasColimitsOfShape J C :=
⟨fun G => hasColimit_of_created G F⟩Informal description
Let $F \colon C \to D$ be a functor that creates colimits of shape $J$, and suppose $D$ has colimits of shape $J$. Then $C$ also has colimits of shape $J$.
CategoryTheory.hasColimits_of_hasColimits_createsColimits
theorem
(F : C ⥤ D) [HasColimitsOfSize.{w, w'} D] [CreatesColimitsOfSize.{w, w'} F] : HasColimitsOfSize.{w, w'} C
Full source
/-- If `F` creates colimits, and `D` has all colimits, then `C` has all colimits. -/
theorem hasColimits_of_hasColimits_createsColimits (F : C ⥤ D) [HasColimitsOfSize.{w, w'} D]
[CreatesColimitsOfSize.{w, w'} F] : HasColimitsOfSize.{w, w'} C :=
⟨fun _ _ => hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape F⟩Informal description
Let $F \colon C \to D$ be a functor that creates colimits of any size, and suppose $D$ has colimits of any size. Then $C$ also has colimits of any size.
CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape
instance
(F : C ⥤ D) [CreatesLimitsOfShape J F] : ReflectsLimitsOfShape J F
Full source
instance (priority := 10) reflectsLimitsOfShapeOfCreatesLimitsOfShape (F : C ⥤ D)
[CreatesLimitsOfShape J F] : ReflectsLimitsOfShape J F where
Informal description
For any functor $F \colon C \to D$ that creates limits of shape $J$, $F$ also reflects limits of shape $J$.
CategoryTheory.reflectsLimitsOfCreatesLimits
instance
(F : C ⥤ D) [CreatesLimitsOfSize.{w, w'} F] : ReflectsLimitsOfSize.{w, w'} F
Full source
instance (priority := 10) reflectsLimitsOfCreatesLimits (F : C ⥤ D)
[CreatesLimitsOfSize.{w, w'} F] : ReflectsLimitsOfSize.{w, w'} F where
Informal description
For any functor $F \colon C \to D$ that creates limits of any size, $F$ also reflects limits of any size.
CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape
instance
(F : C ⥤ D) [CreatesColimitsOfShape J F] : ReflectsColimitsOfShape J F
Full source
instance (priority := 10) reflectsColimitsOfShapeOfCreatesColimitsOfShape (F : C ⥤ D)
[CreatesColimitsOfShape J F] : ReflectsColimitsOfShape J F where
Informal description
For any functor $F \colon C \to D$ that creates colimits of shape $J$, $F$ also reflects colimits of shape $J$.
CategoryTheory.reflectsColimitsOfCreatesColimits
instance
(F : C ⥤ D) [CreatesColimitsOfSize.{w, w'} F] : ReflectsColimitsOfSize.{w, w'} F
Full source
instance (priority := 10) reflectsColimitsOfCreatesColimits (F : C ⥤ D)
[CreatesColimitsOfSize.{w, w'} F] : ReflectsColimitsOfSize.{w, w'} F where
Informal description
For any functor $F \colon C \to D$ that creates colimits of any size, $F$ also reflects colimits of any size.
CategoryTheory.LiftsToLimit
structure
(K : J ⥤ C) (F : C ⥤ D) (c : Cone (K ⋙ F)) (t : IsLimit c) extends
LiftableCone K F c
Full source
/-- A helper to show a functor creates limits. In particular, if we can show
that for any limit cone `c` for `K ⋙ F`, there is a lift of it which is
a limit and `F` reflects isomorphisms, then `F` creates limits.
Usually, `F` creating limits says that _any_ lift of `c` is a limit, but
here we only need to show that our particular lift of `c` is a limit.
-/
structure LiftsToLimit (K : J ⥤ C) (F : C ⥤ D) (c : Cone (K ⋙ F)) (t : IsLimit c) extends
LiftableCone K F c where
/-- the lifted cone is limit -/
makesLimit : IsLimit liftedConeInformal description
A structure that extends `LiftableCone` to include the property that a given cone `c` over the composition `K ⋙ F` is a limit cone, and provides a lift of this cone to a cone over `K` in the original category. This means that for a functor `F : C ⥤ D` and a diagram `K : J ⥤ C`, if `c` is a limit cone for `K ⋙ F`, then `LiftsToLimit` provides a cone over `K` that lifts `c` and maintains the limit property.
CategoryTheory.LiftsToColimit
structure
(K : J ⥤ C) (F : C ⥤ D) (c : Cocone (K ⋙ F)) (t : IsColimit c) extends
LiftableCocone K F c
Full source
/-- A helper to show a functor creates colimits. In particular, if we can show
that for any limit cocone `c` for `K ⋙ F`, there is a lift of it which is
a limit and `F` reflects isomorphisms, then `F` creates colimits.
Usually, `F` creating colimits says that _any_ lift of `c` is a colimit, but
here we only need to show that our particular lift of `c` is a colimit.
-/
structure LiftsToColimit (K : J ⥤ C) (F : C ⥤ D) (c : Cocone (K ⋙ F)) (t : IsColimit c) extends
LiftableCocone K F c where
/-- the lifted cocone is colimit -/
makesColimit : IsColimit liftedCoconeInformal description
Given a functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), a colimit cocone \( c \) of the composition \( K \circ F \), and a proof that \( c \) is indeed a colimit, the structure `LiftsToColimit` provides a lift of \( c \) to a cocone over \( K \) in \( C \), extending the structure `LiftableCocone`.
CategoryTheory.createsLimitOfReflectsIso
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] (h : ∀ c t, LiftsToLimit K F c t) : CreatesLimit K F
Full source
/-- If `F` reflects isomorphisms and we can lift any limit cone to a limit cone,
then `F` creates limits.
In particular here we don't need to assume that F reflects limits.
-/
def createsLimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms]
(h : ∀ c t, LiftsToLimit K F c t) : CreatesLimit K F where
lifts c t := (h c t).toLiftableCone
toReflectsLimit :=
{ reflects := fun {d} hd => ⟨by
let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
let i : F.mapCone d' ≅ F.mapCone d :=
(h (F.mapCone d) hd).toLiftableCone.validLift
let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
let f : d ⟶ d' := hd'.liftConeMorphism d
have : (Cones.functoriality K F).map f = i.inv :=
(hd.ofIsoLimit i.symm).uniq_cone_morphism
haveI : IsIso ((Cones.functoriality K F).map f) := by
rw [this]
infer_instance
haveI : IsIso f := isIso_of_reflects_iso f (Cones.functoriality K F)
exact IsLimit.ofIsoLimit hd' (asIso f).symm⟩ }Informal description
Given a functor $F \colon C \to D$ that reflects isomorphisms and a diagram $K \colon J \to C$, if for every limit cone $c$ of $K \circ F$ and a proof $t$ that $c$ is indeed a limit, there exists a lift of $c$ to a limit cone over $K$ in $C$, then $F$ creates limits of $K$.
CategoryTheory.createsLimitOfReflectsIso'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] {c : Cone (K ⋙ F)} (hc : IsLimit c) (h : LiftsToLimit K F c hc) :
CreatesLimit K F
Full source
/-- If `F` reflects isomorphisms and we can lift a single limit cone to a limit cone, then `F`
creates limits. Note that unlike `createsLimitOfReflectsIso`, to apply this result it is
necessary to know that `K ⋙ F` actually has a limit. -/
def createsLimitOfReflectsIso' {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms]
{c : Cone (K ⋙ F)} (hc : IsLimit c) (h : LiftsToLimit K F c hc) : CreatesLimit K F :=
createsLimitOfReflectsIso fun _ t =>
{ liftedCone := h.liftedCone
validLift := h.validLift ≪≫ IsLimit.uniqueUpToIso hc t
makesLimit := h.makesLimit }Informal description
Given a functor \( F \colon C \to D \) that reflects isomorphisms, a diagram \( K \colon J \to C \), a limit cone \( c \) of the composition \( K \circ F \), and a proof \( h \) that \( c \) can be lifted to a limit cone over \( K \) in \( C \), then \( F \) creates limits of \( K \).
The lifted cone is constructed such that its image under \( F \) is isomorphic to \( c \), and it is verified to be a limit cone in \( C \).
CategoryTheory.createsLimitOfReflectsIsomorphismsOfPreserves
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] [HasLimit K] [PreservesLimit K F] : CreatesLimit K F
Full source
/-- If `F` reflects isomorphisms, and we already know that the limit exists in the source and `F`
preserves it, then `F` creates that limit. -/
def createsLimitOfReflectsIsomorphismsOfPreserves {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms]
[HasLimit K] [PreservesLimit K F] : CreatesLimit K F :=
createsLimitOfReflectsIso' (isLimitOfPreserves F (limit.isLimit _))
⟨⟨_, Iso.refl _⟩, limit.isLimit _⟩Informal description
Given a functor \( F \colon C \to D \) that reflects isomorphisms, a diagram \( K \colon J \to C \), and assuming that \( K \) has a limit in \( C \) and \( F \) preserves this limit, then \( F \) creates limits of \( K \).
CategoryTheory.createsLimitOfFullyFaithfulOfLift'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cone (K ⋙ F)} (hl : IsLimit l) (c : Cone K) (i : F.mapCone c ≅ l) :
CreatesLimit K F
Full source
/--
When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to exhibit a lift
of a limit cone for `K ⋙ F`.
-/
def createsLimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
{l : Cone (K ⋙ F)} (hl : IsLimit l) (c : Cone K) (i : F.mapCone c ≅ l) :
CreatesLimit K F :=
createsLimitOfReflectsIso' hl ⟨⟨c, i⟩, isLimitOfReflects F (IsLimit.ofIsoLimit hl i.symm)⟩Informal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), a limit cone \( l \) of the composition \( K \circ F \), a cone \( c \) over \( K \), and an isomorphism \( i \) between the image of \( c \) under \( F \) and \( l \), then \( F \) creates limits of \( K \).
The construction relies on the fact that \( F \) reflects isomorphisms and the lifted cone \( c \) is verified to be a limit cone in \( C \) by transporting the limit structure along the isomorphism \( i \).
CategoryTheory.createsLimitOfFullyFaithfulOfLift
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] [HasLimit (K ⋙ F)] (c : Cone K) (i : F.mapCone c ≅ limit.cone (K ⋙ F)) :
CreatesLimit K F
Full source
/-- When `F` is fully faithful, and `HasLimit (K ⋙ F)`, to show that `F` creates the limit for `K`
it suffices to exhibit a lift of the chosen limit cone for `K ⋙ F`.
-/
def createsLimitOfFullyFaithfulOfLift {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
[HasLimit (K ⋙ F)] (c : Cone K) (i : F.mapCone c ≅ limit.cone (K ⋙ F)) :
CreatesLimit K F :=
createsLimitOfFullyFaithfulOfLift' (limit.isLimit _) c iInformal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), and assuming the composition \( K \circ F \) has a limit in \( D \), if there exists a cone \( c \) over \( K \) in \( C \) and an isomorphism \( i \) between the image of \( c \) under \( F \) and the limit cone of \( K \circ F \), then \( F \) creates limits of \( K \).
This means that \( F \) not only lifts the limit cone from \( D \) to \( C \) but also ensures that the lifted cone is indeed a limit in \( C \).
CategoryTheory.createsLimitOfFullyFaithfulOfIso'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cone (K ⋙ F)} (hl : IsLimit l) (X : C) (i : F.obj X ≅ l.pt) :
CreatesLimit K F
Full source
/--
When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to show that a
limit point is in the essential image of `F`.
-/
def createsLimitOfFullyFaithfulOfIso' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
{l : Cone (K ⋙ F)} (hl : IsLimit l) (X : C) (i : F.obj X ≅ l.pt) : CreatesLimit K F :=
createsLimitOfFullyFaithfulOfLift' hl
{ pt := X
π :=
{ app := fun j => F.preimage (i.hom ≫ l.π.app j)
naturality := fun Y Z f =>
F.map_injective <| by
dsimp
simpa using (l.w f).symm } }
(Cones.ext i fun j => by simp only [Functor.map_preimage, Functor.mapCone_π_app])Informal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), a limit cone \( l \) of the composition \( K \circ F \), an object \( X \) in \( C \), and an isomorphism \( i \) between \( F(X) \) and the apex of \( l \), then \( F \) creates limits of \( K \).
The construction uses the isomorphism \( i \) to lift the limit cone \( l \) to a cone in \( C \) with apex \( X \), and the fully faithfulness of \( F \) ensures that this lifted cone is indeed a limit cone in \( C \).
CategoryTheory.createsLimitOfFullyFaithfulOfIso
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] [HasLimit (K ⋙ F)] (X : C) (i : F.obj X ≅ limit (K ⋙ F)) :
CreatesLimit K F
Full source
/-- When `F` is fully faithful, and `HasLimit (K ⋙ F)`, to show that `F` creates the limit for `K`
it suffices to show that the chosen limit point is in the essential image of `F`.
-/
def createsLimitOfFullyFaithfulOfIso {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
[HasLimit (K ⋙ F)] (X : C) (i : F.obj X ≅ limit (K ⋙ F)) : CreatesLimit K F :=
createsLimitOfFullyFaithfulOfIso' (limit.isLimit _) X iInformal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), and assuming the composition \( K \circ F \) has a limit in \( D \), if there exists an object \( X \) in \( C \) and an isomorphism \( i \) between \( F(X) \) and the limit of \( K \circ F \), then \( F \) creates limits of \( K \).
This means that \( F \) can lift the limit cone from \( D \) to \( C \) using the isomorphism \( i \), and the fully faithfulness of \( F \) ensures that the lifted cone is indeed a limit cone in \( C \).
CategoryTheory.createsLimitOfFullyFaithfulOfPreserves
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] [HasLimit K] [PreservesLimit K F] : CreatesLimit K F
Full source
/-- A fully faithful functor that preserves a limit that exists also creates the limit. -/
def createsLimitOfFullyFaithfulOfPreserves {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
[HasLimit K] [PreservesLimit K F] : CreatesLimit K F :=
createsLimitOfFullyFaithfulOfLift' (isLimitOfPreserves _ (limit.isLimit K)) _ (Iso.refl _)Informal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), and assuming that \( K \) has a limit in \( C \) which is preserved by \( F \), then \( F \) creates limits of \( K \).
This means that the existence of a limit cone for \( K \) in \( C \) and its preservation by \( F \) guarantees that \( F \) can lift any limit cone of \( K \circ F \) in \( D \) back to a limit cone in \( C \), and reflects limits of \( K \).
CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
instance
(K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F
Full source
/-- `F` preserves the limit of `K` if it creates the limit and `K ⋙ F` has the limit. -/
instance (priority := 100) preservesLimit_of_createsLimit_and_hasLimit (K : J ⥤ C) (F : C ⥤ D)
[CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F where
preserves t := ⟨IsLimit.ofIsoLimit (limit.isLimit _)
((liftedLimitMapsToOriginal (limit.isLimit _)).symm ≪≫
(Cones.functoriality K F).mapIso ((liftedLimitIsLimit (limit.isLimit _)).uniqueUpToIso t))⟩Informal description
A functor $F \colon C \to D$ preserves the limit of a diagram $K \colon J \to C$ if $F$ creates the limit of $K$ and the composition $K \circ F$ has a limit in $D$.
CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit
theorem
(K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesLimitOfCreatesLimitAndHasLimit (K : J ⥤ C) (F : C ⥤ D)
[CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F :=
preservesLimit_of_createsLimit_and_hasLimit _ _Informal description
Let $F \colon C \to D$ be a functor and $K \colon J \to C$ a diagram. If $F$ creates limits of $K$ and the composition $K \circ F$ has a limit in $D$, then $F$ preserves the limit of $K$.
CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
instance
(F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F
Full source
/-- `F` preserves the limit of shape `J` if it creates these limits and `D` has them. -/
instance (priority := 100) preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
(F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F where
Informal description
A functor $F \colon C \to D$ preserves limits of shape $J$ if $F$ creates limits of shape $J$ and $D$ has limits of shape $J$.
CategoryTheory.preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape
theorem
(F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape
(F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] :
PreservesLimitsOfShape J F :=
preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape _Informal description
Let $F \colon C \to D$ be a functor between categories. If $F$ creates limits of shape $J$ and $D$ has limits of shape $J$, then $F$ preserves limits of shape $J$.
CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits
instance
(F : C ⥤ D) [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] : PreservesLimitsOfSize.{w, w'} F
Full source
/-- `F` preserves limits if it creates limits and `D` has limits. -/
instance (priority := 100) preservesLimits_of_createsLimits_and_hasLimits (F : C ⥤ D)
[CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] :
PreservesLimitsOfSize.{w, w'} F where
Informal description
A functor $F \colon C \to D$ preserves limits of any size if $F$ creates limits of any size and $D$ has limits of that size.
CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits
theorem
(F : C ⥤ D) [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] : PreservesLimitsOfSize.{w, w'} F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesLimitsOfCreatesLimitsAndHasLimits (F : C ⥤ D)
[CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] :
PreservesLimitsOfSize.{w, w'} F :=
preservesLimits_of_createsLimits_and_hasLimits _Informal description
Let $F \colon C \to D$ be a functor between categories. If $F$ creates limits of any size and $D$ has limits of that size, then $F$ preserves limits of that size.
CategoryTheory.createsColimitOfReflectsIso
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] (h : ∀ c t, LiftsToColimit K F c t) : CreatesColimit K F
Full source
/-- If `F` reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then `F` creates colimits.
In particular here we don't need to assume that F reflects colimits.
-/
def createsColimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms]
(h : ∀ c t, LiftsToColimit K F c t) : CreatesColimit K F where
lifts c t := (h c t).toLiftableCocone
toReflectsColimit :=
{ reflects := fun {d} hd => ⟨by
let d' : Cocone K := (h (F.mapCocone d) hd).toLiftableCocone.liftedCocone
let i : F.mapCocone d' ≅ F.mapCocone d :=
(h (F.mapCocone d) hd).toLiftableCocone.validLift
let hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
let f : d' ⟶ d := hd'.descCoconeMorphism d
have : (Cocones.functoriality K F).map f = i.hom :=
(hd.ofIsoColimit i.symm).uniq_cocone_morphism
haveI : IsIso ((Cocones.functoriality K F).map f) := by
rw [this]
infer_instance
haveI := isIso_of_reflects_iso f (Cocones.functoriality K F)
exact IsColimit.ofIsoColimit hd' (asIso f)⟩ }Informal description
A functor \( F \colon C \to D \) that reflects isomorphisms creates colimits of a diagram \( K \colon J \to C \) if, for every colimit cocone \( c \) of \( K \circ F \) with proof \( t \) that \( c \) is a colimit, there exists a lift of \( c \) to a colimit cocone of \( K \). This means \( F \) not only lifts colimit cocones but also reflects colimits of \( K \).
CategoryTheory.createsColimitOfReflectsIso'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] {c : Cocone (K ⋙ F)} (hc : IsColimit c)
(h : LiftsToColimit K F c hc) : CreatesColimit K F
Full source
/-- If `F` reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then
`F` creates limits. Note that unlike `createsColimitOfReflectsIso`, to apply this result it is
necessary to know that `K ⋙ F` actually has a colimit. -/
def createsColimitOfReflectsIso' {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms]
{c : Cocone (K ⋙ F)} (hc : IsColimit c) (h : LiftsToColimit K F c hc) : CreatesColimit K F :=
createsColimitOfReflectsIso fun _ t =>
{ liftedCocone := h.liftedCocone
validLift := h.validLift ≪≫ IsColimit.uniqueUpToIso hc t
makesColimit := h.makesColimit }Informal description
Given a functor \( F \colon C \to D \) that reflects isomorphisms, a diagram \( K \colon J \to C \), a colimit cocone \( c \) of the composition \( K \circ F \), and a proof \( hc \) that \( c \) is a colimit, if there exists a lift \( h \) of \( c \) to a colimit cocone of \( K \), then \( F \) creates the colimit of \( K \).
CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves
definition
{K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] [HasColimit K] [PreservesColimit K F] : CreatesColimit K F
Full source
/-- If `F` reflects isomorphisms, and we already know that the colimit exists in the source and `F`
preserves it, then `F` creates that colimit. -/
def createsColimitOfReflectsIsomorphismsOfPreserves {K : J ⥤ C} {F : C ⥤ D}
[F.ReflectsIsomorphisms] [HasColimit K] [PreservesColimit K F] : CreatesColimit K F :=
createsColimitOfReflectsIso' (isColimitOfPreserves F (colimit.isColimit _))
⟨⟨_, Iso.refl _⟩, colimit.isColimit _⟩Informal description
Given a functor \( F \colon C \to D \) that reflects isomorphisms, a diagram \( K \colon J \to C \), and assuming that \( K \) has a colimit in \( C \) and \( F \) preserves this colimit, then \( F \) creates the colimit of \( K \). This means \( F \) not only lifts the colimit cocone from \( D \) back to \( C \) but also ensures that the lifted cocone is indeed a colimit in \( C \).
CategoryTheory.createsColimitOfFullyFaithfulOfLift'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cocone (K ⋙ F)} (hl : IsColimit l) (c : Cocone K)
(i : F.mapCocone c ≅ l) : CreatesColimit K F
Full source
/--
When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to exhibit a
lift of a colimit cocone for `K ⋙ F`.
-/
def createsColimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
{l : Cocone (K ⋙ F)} (hl : IsColimit l) (c : Cocone K) (i : F.mapCocone c ≅ l) :
CreatesColimit K F :=
createsColimitOfReflectsIso' hl ⟨⟨c, i⟩, isColimitOfReflects F (IsColimit.ofIsoColimit hl i.symm)⟩Informal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), a colimit cocone \( l \) of the composition \( K \circ F \), and a cocone \( c \) of \( K \) such that the image of \( c \) under \( F \) is isomorphic to \( l \), then \( F \) creates the colimit of \( K \).
CategoryTheory.createsColimitOfFullyFaithfulOfLift
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] [HasColimit (K ⋙ F)] (c : Cocone K)
(i : F.mapCocone c ≅ colimit.cocone (K ⋙ F)) : CreatesColimit K F
Full source
/--
When `F` is fully faithful, and `HasColimit (K ⋙ F)`, to show that `F` creates the colimit for `K`
it suffices to exhibit a lift of the chosen colimit cocone for `K ⋙ F`.
-/
def createsColimitOfFullyFaithfulOfLift {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
[HasColimit (K ⋙ F)] (c : Cocone K) (i : F.mapCocone c ≅ colimit.cocone (K ⋙ F)) :
CreatesColimit K F :=
createsColimitOfFullyFaithfulOfLift' (colimit.isColimit _) c iInformal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), and assuming the composition \( K \circ F \) has a colimit in \( D \), if there exists a cocone \( c \) of \( K \) whose image under \( F \) is isomorphic to the colimit cocone of \( K \circ F \), then \( F \) creates the colimit of \( K \). This means \( F \) lifts the colimit cocone from \( D \) back to \( C \) in a way that preserves the colimit structure.
CategoryTheory.createsColimitOfFullyFaithfulOfIso'
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cocone (K ⋙ F)} (hl : IsColimit l) (X : C) (i : F.obj X ≅ l.pt) :
CreatesColimit K F
Full source
/--
When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to show that
a colimit point is in the essential image of `F`.
-/
def createsColimitOfFullyFaithfulOfIso' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
{l : Cocone (K ⋙ F)} (hl : IsColimit l) (X : C) (i : F.obj X ≅ l.pt) : CreatesColimit K F :=
createsColimitOfFullyFaithfulOfLift' hl
{ pt := X
ι :=
{ app := fun j => F.preimage (l.ι.app j ≫ i.inv)
naturality := fun Y Z f =>
F.map_injective <| by
dsimp
simpa [← cancel_mono i.hom] using l.w f } }
(Cocones.ext i fun j => by simp)Informal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), a colimit cocone \( l \) of the composition \( K \circ F \), and an object \( X \) in \( C \) such that \( F(X) \) is isomorphic to the apex of \( l \), then \( F \) creates the colimit of \( K \). Specifically, the cocone over \( K \) with apex \( X \) and structure maps obtained by preimages under \( F \) of the structure maps of \( l \) composed with the isomorphism, is a colimit cocone for \( K \).
CategoryTheory.createsColimitOfFullyFaithfulOfIso
definition
{K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] [HasColimit (K ⋙ F)] (X : C) (i : F.obj X ≅ colimit (K ⋙ F)) :
CreatesColimit K F
Full source
/--
When `F` is fully faithful, and `HasColimit (K ⋙ F)`, to show that `F` creates the colimit for `K`
it suffices to show that the chosen colimit point is in the essential image of `F`.
-/
def createsColimitOfFullyFaithfulOfIso {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful]
[HasColimit (K ⋙ F)] (X : C) (i : F.obj X ≅ colimit (K ⋙ F)) : CreatesColimit K F :=
createsColimitOfFullyFaithfulOfIso' (colimit.isColimit _) X iInformal description
Given a fully faithful functor \( F \colon C \to D \), a diagram \( K \colon J \to C \), and assuming the composition \( K \circ F \) has a colimit in \( D \), if there exists an object \( X \) in \( C \) such that \( F(X) \) is isomorphic to the colimit of \( K \circ F \), then \( F \) creates the colimit of \( K \). This means \( F \) lifts the colimit from \( D \) back to \( C \) via the isomorphism \( i \).
CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
instance
(K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F
Full source
/-- `F` preserves the colimit of `K` if it creates the colimit and `K ⋙ F` has the colimit. -/
instance (priority := 100) preservesColimit_of_createsColimit_and_hasColimit (K : J ⥤ C) (F : C ⥤ D)
[CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F where
preserves t :=
⟨IsColimit.ofIsoColimit (colimit.isColimit _)
((liftedColimitMapsToOriginal (colimit.isColimit _)).symm ≪≫
(Cocones.functoriality K F).mapIso
((liftedColimitIsColimit (colimit.isColimit _)).uniqueUpToIso t))⟩Informal description
A functor $F \colon C \to D$ preserves the colimit of a diagram $K \colon J \to C$ if $F$ creates the colimit of $K$ and the composition $K \circ F \colon J \to D$ has a colimit.
CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit
theorem
(K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesColimitOfCreatesColimitAndHasColimit (K : J ⥤ C) (F : C ⥤ D)
[CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F :=
preservesColimit_of_createsColimit_and_hasColimit _ _Informal description
Let $K \colon J \to C$ be a diagram and $F \colon C \to D$ a functor. If $F$ creates colimits of $K$ and the composition $K \circ F \colon J \to D$ has a colimit, then $F$ preserves the colimit of $K$.
CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
instance
(F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] : PreservesColimitsOfShape J F
Full source
/-- `F` preserves the colimit of shape `J` if it creates these colimits and `D` has them. -/
instance (priority := 100) preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
(F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] :
PreservesColimitsOfShape J F where
Informal description
A functor $F \colon C \to D$ preserves colimits of shape $J$ if $F$ creates colimits of shape $J$ and $D$ has colimits of shape $J$.
CategoryTheory.preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape
theorem
(F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] : PreservesColimitsOfShape J F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape
(F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] :
PreservesColimitsOfShape J F :=
preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape _Informal description
Let $F \colon C \to D$ be a functor between categories. If $F$ creates colimits of shape $J$ and $D$ has colimits of shape $J$, then $F$ preserves colimits of shape $J$.
CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits
instance
(F : C ⥤ D) [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] : PreservesColimitsOfSize.{w, w'} F
Full source
/-- `F` preserves limits if it creates limits and `D` has limits. -/
instance (priority := 100) preservesColimits_of_createsColimits_and_hasColimits (F : C ⥤ D)
[CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] :
PreservesColimitsOfSize.{w, w'} F where
Informal description
A functor $F \colon C \to D$ preserves colimits of any size if $F$ creates colimits of that size and $D$ has colimits of that size.
CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits
theorem
(F : C ⥤ D) [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] : PreservesColimitsOfSize.{w, w'} F
Full source
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma preservesColimitsOfCreatesColimitsAndHasColimits (F : C ⥤ D)
[CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] :
PreservesColimitsOfSize.{w, w'} F :=
preservesColimits_of_createsColimits_and_hasColimits _Informal description
Let $F \colon C \to D$ be a functor between categories. If $F$ creates colimits of any size and $D$ has colimits of that size, then $F$ preserves colimits of that size.
CategoryTheory.createsLimitOfIsoDiagram
definition
{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [CreatesLimit K₁ F] : CreatesLimit K₂ F
Full source
/-- Transfer creation of limits along a natural isomorphism in the diagram. -/
def createsLimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [CreatesLimit K₁ F] :
CreatesLimit K₂ F :=
{ reflectsLimit_of_iso_diagram F h with
lifts := fun c t =>
let t' := (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) c).symm t
{ liftedCone := (Cones.postcompose h.hom).obj (liftLimit t')
validLift :=
Functor.mapConePostcomposeFunctor.mapConePostcompose F ≪≫
(Cones.postcompose (isoWhiskerRight h F).hom).mapIso (liftedLimitMapsToOriginal t') ≪≫
Cones.ext (Iso.refl _) fun j => by
dsimp
rw [Category.assoc, ← F.map_comp]
simp } }Informal description
Given functors \( K_1, K_2 \colon J \to C \) and a natural isomorphism \( h \colon K_1 \cong K_2 \), if a functor \( F \colon C \to D \) creates limits of the diagram \( K_1 \), then \( F \) also creates limits of the diagram \( K_2 \).
Specifically, for any limit cone \( c \) of \( K_2 \circ F \) in \( D \), the lifted cone for \( K_2 \) is constructed by postcomposing the lifted cone for \( K_1 \) with \( h \), and the isomorphism between the image of the lifted cone under \( F \) and the original cone \( c \) is preserved.
CategoryTheory.createsLimitOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesLimit K F] : CreatesLimit K G
Full source
/-- If `F` creates the limit of `K` and `F ≅ G`, then `G` creates the limit of `K`. -/
def createsLimitOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesLimit K F] : CreatesLimit K G where
lifts c t :=
{ liftedCone := liftLimit ((IsLimit.postcomposeInvEquiv (isoWhiskerLeft K h :) c).symm t)
validLift := by
refine (IsLimit.mapConeEquiv h ?_).uniqueUpToIso t
apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).symm
apply (IsLimit.postcomposeInvEquiv _ _).symm t }
toReflectsLimit := reflectsLimit_of_natIso _ hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates limits of a diagram \( K \colon J \to C \), then \( G \) also creates limits of \( K \).
Specifically, for any limit cone \( c \) of \( K \circ G \) in \( D \), the lifted cone for \( K \) is constructed by transporting the limit cone of \( K \circ F \) through the isomorphism \( h \), and the isomorphism between the image of the lifted cone under \( G \) and the original cone \( c \) is preserved.
CategoryTheory.createsLimitsOfShapeOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesLimitsOfShape J F] : CreatesLimitsOfShape J G
Full source
/-- If `F` creates limits of shape `J` and `F ≅ G`, then `G` creates limits of shape `J`. -/
def createsLimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesLimitsOfShape J F] :
CreatesLimitsOfShape J G where CreatesLimit := createsLimitOfNatIso hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates limits of shape \( J \), then \( G \) also creates limits of shape \( J \).
CategoryTheory.createsLimitsOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesLimitsOfSize.{w, w'} F] : CreatesLimitsOfSize.{w, w'} G
Full source
/-- If `F` creates limits and `F ≅ G`, then `G` creates limits. -/
def createsLimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesLimitsOfSize.{w, w'} F] :
CreatesLimitsOfSize.{w, w'} G where
CreatesLimitsOfShape := createsLimitsOfShapeOfNatIso hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates limits of any size, then \( G \) also creates limits of any size.
CategoryTheory.createsLimitsOfShapeOfEquiv
definition
{J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D) [CreatesLimitsOfShape J F] : CreatesLimitsOfShape J' F
Full source
/-- If `F` creates limits of shape `J` and `J ≌ J'`, then `F` creates limits of shape `J'`. -/
def createsLimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D)
[CreatesLimitsOfShape J F] : CreatesLimitsOfShape J' F where
CreatesLimit {K} :=
{ lifts c hc := by
refine ⟨(Cones.whiskeringEquivalence e).inverse.obj
(liftLimit (hc.whiskerEquivalence e)), ?_⟩
letI inner := (Cones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
(liftedLimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
refine ?_ ≪≫ inner ≪≫ ((Cones.whiskeringEquivalence e).unitIso.app c).symm
exact Cones.ext (Iso.refl _)
toReflectsLimit := have := reflectsLimitsOfShape_of_equiv e F; inferInstance }Informal description
Given an equivalence of categories $e \colon J \simeq J'$ and a functor $F \colon C \to D$ that creates limits of shape $J$, then $F$ also creates limits of shape $J'$.
Specifically, for any diagram $K \colon J' \to C$, the functor $F$ can lift any limit cone of the composition $K \circ F$ to a limit cone of $K$ in $C$, and $F$ reflects limits for $K$. The construction uses the equivalence $e$ to transfer the limit creation property from shape $J$ to shape $J'$.
CategoryTheory.createsColimitOfIsoDiagram
definition
{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [CreatesColimit K₁ F] : CreatesColimit K₂ F
Full source
/-- Transfer creation of colimits along a natural isomorphism in the diagram. -/
def createsColimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [CreatesColimit K₁ F] :
CreatesColimit K₂ F :=
{ reflectsColimit_of_iso_diagram F h with
lifts := fun c t =>
let t' := (IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) c).symm t
{ liftedCocone := (Cocones.precompose h.inv).obj (liftColimit t')
validLift :=
Functor.mapCoconePrecomposeFunctor.mapCoconePrecompose F ≪≫
(Cocones.precompose (isoWhiskerRight h F).inv).mapIso
(liftedColimitMapsToOriginal t') ≪≫
Cocones.ext (Iso.refl _) fun j => by
dsimp
rw [← F.map_comp_assoc]
simp } }Informal description
Given functors \( K_1, K_2 \colon J \to C \) and a natural isomorphism \( h \colon K_1 \cong K_2 \), if a functor \( F \colon C \to D \) creates colimits of the diagram \( K_1 \), then \( F \) also creates colimits of the diagram \( K_2 \).
Specifically, for any colimit cocone \( c \) of the composition \( K_2 \circ F \), the construction provides a colimit cocone for \( K_2 \) by precomposing with the inverse of \( h \) and using the colimit creation property for \( K_1 \). The lifted cocone is mapped by \( F \) to a cocone isomorphic to \( c \), ensuring that \( F \) reflects colimits for \( K_2 \).
CategoryTheory.createsColimitOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesColimit K F] : CreatesColimit K G
Full source
/-- If `F` creates the colimit of `K` and `F ≅ G`, then `G` creates the colimit of `K`. -/
def createsColimitOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesColimit K F] : CreatesColimit K G where
lifts c t :=
{ liftedCocone := liftColimit ((IsColimit.precomposeHomEquiv (isoWhiskerLeft K h :) c).symm t)
validLift := by
refine (IsColimit.mapCoconeEquiv h ?_).uniqueUpToIso t
apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).symm
apply (IsColimit.precomposeHomEquiv _ _).symm t }
toReflectsColimit := reflectsColimit_of_natIso _ hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates colimits of a diagram \( K \colon J \to C \), then \( G \) also creates colimits of \( K \).
Specifically, for any colimit cocone \( c \) of the composition \( K \circ G \), the construction provides a colimit cocone for \( K \) by lifting through \( F \) and using the isomorphism \( h \) to relate the results. The lifted cocone is mapped by \( G \) to a cocone isomorphic to \( c \), ensuring that \( G \) reflects colimits for \( K \).
CategoryTheory.createsColimitsOfShapeOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J G
Full source
/-- If `F` creates colimits of shape `J` and `F ≅ G`, then `G` creates colimits of shape `J`. -/
def createsColimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesColimitsOfShape J F] :
CreatesColimitsOfShape J G where CreatesColimit := createsColimitOfNatIso hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates colimits of shape \( J \), then \( G \) also creates colimits of shape \( J \).
Specifically, for any diagram \( K \colon J \to C \), the functor \( G \) can lift any colimit cocone of the composition \( K \circ G \) to a colimit cocone of \( K \) in \( C \), and \( G \) reflects colimits for \( K \). This property is inherited from \( F \) via the natural isomorphism \( h \).
CategoryTheory.createsColimitsOfNatIso
definition
{F G : C ⥤ D} (h : F ≅ G) [CreatesColimitsOfSize.{w, w'} F] : CreatesColimitsOfSize.{w, w'} G
Full source
/-- If `F` creates colimits and `F ≅ G`, then `G` creates colimits. -/
def createsColimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesColimitsOfSize.{w, w'} F] :
CreatesColimitsOfSize.{w, w'} G where
CreatesColimitsOfShape := createsColimitsOfShapeOfNatIso hInformal description
Given a natural isomorphism \( h \colon F \cong G \) between functors \( F, G \colon C \to D \), if \( F \) creates colimits of any size, then \( G \) also creates colimits of any size.
Specifically, for any diagram \( K \colon J \to C \), the functor \( G \) can lift any colimit cocone of the composition \( K \circ G \) to a colimit cocone of \( K \) in \( C \), and \( G \) reflects colimits for \( K \). This property is inherited from \( F \) via the natural isomorphism \( h \).
CategoryTheory.createsColimitsOfShapeOfEquiv
definition
{J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D) [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J' F
Full source
/-- If `F` creates colimits of shape `J` and `J ≌ J'`, then `F` creates colimits of shape `J'`. -/
def createsColimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D)
[CreatesColimitsOfShape J F] : CreatesColimitsOfShape J' F where
CreatesColimit {K} :=
{ lifts c hc := by
refine ⟨(Cocones.whiskeringEquivalence e).inverse.obj
(liftColimit (hc.whiskerEquivalence e)), ?_⟩
letI inner := (Cocones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
(liftedColimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
refine ?_ ≪≫ inner ≪≫ ((Cocones.whiskeringEquivalence e).unitIso.app c).symm
exact Cocones.ext (Iso.refl _)
toReflectsColimit := have := reflectsColimitsOfShape_of_equiv e F; inferInstance }Informal description
Given categories $J$ and $J'$ with an equivalence $e \colon J \simeq J'$, and a functor $F \colon C \to D$ that creates colimits of shape $J$, then $F$ also creates colimits of shape $J'$.
CategoryTheory.liftsToLimitOfCreates
definition
(K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] (c : Cone (K ⋙ F)) (t : IsLimit c) : LiftsToLimit K F c t
Full source
/-- If F creates the limit of K, any cone lifts to a limit. -/
def liftsToLimitOfCreates (K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] (c : Cone (K ⋙ F))
(t : IsLimit c) : LiftsToLimit K F c t where
liftedCone := liftLimit t
validLift := liftedLimitMapsToOriginal t
makesLimit := liftedLimitIsLimit tInformal description
Given a functor \( F \colon C \to D \) that creates limits of a diagram \( K \colon J \to C \), and given a limit cone \( c \) for the composition \( K \circ F \) in \( D \) with proof \( t \) that \( c \) is indeed a limit, the structure `LiftsToLimit` provides a cone over \( K \) that lifts \( c \) through \( F \), along with proofs that the lifted cone is a limit and that its image under \( F \) is isomorphic to \( c \).
CategoryTheory.liftsToColimitOfCreates
definition
(K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] (c : Cocone (K ⋙ F)) (t : IsColimit c) : LiftsToColimit K F c t
Full source
/-- If F creates the colimit of K, any cocone lifts to a colimit. -/
def liftsToColimitOfCreates (K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] (c : Cocone (K ⋙ F))
(t : IsColimit c) : LiftsToColimit K F c t where
liftedCocone := liftColimit t
validLift := liftedColimitMapsToOriginal t
makesColimit := liftedColimitIsColimit tInformal description
Given a functor \( F \colon C \to D \) that creates colimits of a diagram \( K \colon J \to C \), a colimit cocone \( c \) for the composition \( K \circ F \colon J \to D \), and a proof that \( c \) is indeed a colimit, the structure `liftsToColimitOfCreates` provides a lift of \( c \) to a cocone over \( K \) in \( C \). This lifted cocone is a colimit cocone for \( K \), and its image under \( F \) is isomorphic to \( c \).
CategoryTheory.idLiftsCone
definition
(c : Cone (K ⋙ 𝟭 C)) : LiftableCone K (𝟭 C) c
Full source
/-- Any cone lifts through the identity functor. -/
def idLiftsCone (c : Cone (K ⋙ 𝟭 C)) : LiftableCone K (𝟭 C) c where
liftedCone :=
{ pt := c.pt
π := c.π ≫ K.rightUnitor.hom }
validLift := Cones.ext (Iso.refl _)Informal description
Given a cone $c$ over the composition of a functor $K \colon J \to C$ with the identity functor $\text{id}_C \colon C \to C$, there exists a lift of $c$ to a cone over $K$ itself. The lifted cone has the same apex as $c$, and its cone morphisms are obtained by composing the cone morphisms of $c$ with the right unitor isomorphism of $K$. The lift is valid in the sense that the image of the lifted cone under the identity functor is isomorphic to $c$ via the identity isomorphism.
CategoryTheory.idCreatesLimits
instance
: CreatesLimitsOfSize.{w, w'} (𝟭 C)
Full source
/-- The identity functor creates all limits. -/
instance idCreatesLimits : CreatesLimitsOfSize.{w, w'} (𝟭 C) where
CreatesLimitsOfShape :=
{ CreatesLimit := { lifts := fun c _ => idLiftsCone c } }Informal description
The identity functor $\text{id}_C \colon C \to C$ creates all limits of any size. This means that for any functor $K \colon J \to C$ and any limit cone of the composition $K \circ \text{id}_C$, there exists a limit cone for $K$ that maps to the original cone under $\text{id}_C$, and $\text{id}_C$ reflects limits for $K$.
CategoryTheory.idLiftsCocone
definition
(c : Cocone (K ⋙ 𝟭 C)) : LiftableCocone K (𝟭 C) c
Full source
/-- Any cocone lifts through the identity functor. -/
def idLiftsCocone (c : Cocone (K ⋙ 𝟭 C)) : LiftableCocone K (𝟭 C) c where
liftedCocone :=
{ pt := c.pt
ι := K.rightUnitor.inv ≫ c.ι }
validLift := Cocones.ext (Iso.refl _)Informal description
Given a cocone $c$ for the composition of a functor $K \colon J \to C$ with the identity functor $\text{id}_C \colon C \to C$, there exists a lift of $c$ to a cocone for $K$ itself. The lifted cocone has the same apex as $c$, and its cocone morphisms are obtained by composing the cocone morphisms of $c$ with the inverse of the right unitor isomorphism of $K$. The lift is valid in the sense that the image of the lifted cocone under the identity functor is isomorphic to $c$ via the identity isomorphism.
CategoryTheory.idCreatesColimits
instance
: CreatesColimitsOfSize.{w, w'} (𝟭 C)
Full source
/-- The identity functor creates all colimits. -/
instance idCreatesColimits : CreatesColimitsOfSize.{w, w'} (𝟭 C) where
CreatesColimitsOfShape :=
{ CreatesColimit := { lifts := fun c _ => idLiftsCocone c } }Informal description
The identity functor $\text{id}_C \colon C \to C$ creates all colimits of any size. This means that for any functor $K \colon J \to C$ and any colimit cocone of the composition $K \circ \text{id}_C$, there exists a colimit cocone for $K$ that maps to the original cocone under $\text{id}_C$, and $\text{id}_C$ reflects colimits for $K$.
CategoryTheory.inhabitedLiftableCone
instance
(c : Cone (K ⋙ 𝟭 C)) : Inhabited (LiftableCone K (𝟭 C) c)
Full source
/-- Satisfy the inhabited linter -/
instance inhabitedLiftableCone (c : Cone (K ⋙ 𝟭 C)) : Inhabited (LiftableCone K (𝟭 C) c) :=
⟨idLiftsCone c⟩Informal description
For any cone $c$ over the composition of a functor $K \colon J \to C$ with the identity functor $\text{id}_C \colon C \to C$, the type of lifts of $c$ to a cone over $K$ is inhabited.
CategoryTheory.inhabitedLiftableCocone
instance
(c : Cocone (K ⋙ 𝟭 C)) : Inhabited (LiftableCocone K (𝟭 C) c)
Full source
instance inhabitedLiftableCocone (c : Cocone (K ⋙ 𝟭 C)) : Inhabited (LiftableCocone K (𝟭 C) c) :=
⟨idLiftsCocone c⟩Informal description
For any cocone $c$ of the composition of a functor $K \colon J \to C$ with the identity functor $\text{id}_C \colon C \to C$, there exists a lift of $c$ to a cocone for $K$.
CategoryTheory.inhabitedLiftsToLimit
instance
(K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] (c : Cone (K ⋙ F)) (t : IsLimit c) : Inhabited (LiftsToLimit _ _ _ t)
Full source
/-- Satisfy the inhabited linter -/
instance inhabitedLiftsToLimit (K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] (c : Cone (K ⋙ F))
(t : IsLimit c) : Inhabited (LiftsToLimit _ _ _ t) :=
⟨liftsToLimitOfCreates K F c t⟩Informal description
For any functor $F \colon C \to D$ that creates limits of a diagram $K \colon J \to C$, and any limit cone $c$ for the composition $K \circ F$ with proof $t$ that $c$ is a limit, the type of lifts of $c$ to a limit cone over $K$ is inhabited.
CategoryTheory.inhabitedLiftsToColimit
instance
(K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] (c : Cocone (K ⋙ F)) (t : IsColimit c) :
Inhabited (LiftsToColimit _ _ _ t)
Full source
instance inhabitedLiftsToColimit (K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] (c : Cocone (K ⋙ F))
(t : IsColimit c) : Inhabited (LiftsToColimit _ _ _ t) :=
⟨liftsToColimitOfCreates K F c t⟩Informal description
Given a functor $F \colon C \to D$ that creates colimits of a diagram $K \colon J \to C$, a colimit cocone $c$ for the composition $K \circ F \colon J \to D$, and a proof that $c$ is indeed a colimit, there exists a lift of $c$ to a cocone over $K$ in $C$.
CategoryTheory.compCreatesLimit
instance
[CreatesLimit K F] [CreatesLimit (K ⋙ F) G] : CreatesLimit K (F ⋙ G)
Full source
instance compCreatesLimit [CreatesLimit K F] [CreatesLimit (K ⋙ F) G] :
CreatesLimit K (F ⋙ G) where
lifts c t := by
let c' : Cone ((K ⋙ F) ⋙ G) := c
let t' : IsLimit c' := t
exact
{ liftedCone := liftLimit (liftedLimitIsLimit t')
validLift := (Cones.functoriality (K ⋙ F) G).mapIso
(liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
liftedLimitMapsToOriginal t' }Informal description
Given functors $F \colon C \to D$ and $G \colon D \to E$ such that $F$ creates limits of a diagram $K \colon J \to C$ and $G$ creates limits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ creates limits of $K$.
CategoryTheory.compCreatesLimitsOfShape
instance
[CreatesLimitsOfShape J F] [CreatesLimitsOfShape J G] : CreatesLimitsOfShape J (F ⋙ G)
Full source
instance compCreatesLimitsOfShape [CreatesLimitsOfShape J F] [CreatesLimitsOfShape J G] :
CreatesLimitsOfShape J (F ⋙ G) where CreatesLimit := inferInstanceInformal description
Given functors $F \colon C \to D$ and $G \colon D \to E$ that both create limits of shape $J$, their composition $F \circ G \colon C \to E$ also creates limits of shape $J$.
CategoryTheory.compCreatesLimits
instance
[CreatesLimitsOfSize.{w, w'} F] [CreatesLimitsOfSize.{w, w'} G] : CreatesLimitsOfSize.{w, w'} (F ⋙ G)
Full source
instance compCreatesLimits [CreatesLimitsOfSize.{w, w'} F] [CreatesLimitsOfSize.{w, w'} G] :
CreatesLimitsOfSize.{w, w'} (F ⋙ G) where CreatesLimitsOfShape := inferInstanceInformal description
Given functors $F \colon C \to D$ and $G \colon D \to E$ that both create limits of any size, their composition $F \circ G \colon C \to E$ also creates limits of any size.
CategoryTheory.compCreatesColimit
instance
[CreatesColimit K F] [CreatesColimit (K ⋙ F) G] : CreatesColimit K (F ⋙ G)
Full source
instance compCreatesColimit [CreatesColimit K F] [CreatesColimit (K ⋙ F) G] :
CreatesColimit K (F ⋙ G) where
lifts c t :=
let c' : Cocone ((K ⋙ F) ⋙ G) := c
let t' : IsColimit c' := t
{ liftedCocone := liftColimit (liftedColimitIsColimit t')
validLift :=
(Cocones.functoriality (K ⋙ F) G).mapIso
(liftedColimitMapsToOriginal (liftedColimitIsColimit t')) ≪≫
liftedColimitMapsToOriginal t' }Informal description
Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ creates colimits of a diagram $K \colon J \to C$ and $G$ creates colimits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ creates colimits of $K$.
CategoryTheory.compCreatesColimitsOfShape
instance
[CreatesColimitsOfShape J F] [CreatesColimitsOfShape J G] : CreatesColimitsOfShape J (F ⋙ G)
Full source
instance compCreatesColimitsOfShape [CreatesColimitsOfShape J F] [CreatesColimitsOfShape J G] :
CreatesColimitsOfShape J (F ⋙ G) where CreatesColimit := inferInstanceInformal description
Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ creates colimits of shape $J$ and $G$ creates colimits of shape $J$ for the composition $K \circ F$ where $K \colon J \to C$, then the composition $F \circ G \colon C \to E$ creates colimits of shape $J$.
CategoryTheory.compCreatesColimits
instance
[CreatesColimitsOfSize.{w, w'} F] [CreatesColimitsOfSize.{w, w'} G] : CreatesColimitsOfSize.{w, w'} (F ⋙ G)
Full source
instance compCreatesColimits [CreatesColimitsOfSize.{w, w'} F] [CreatesColimitsOfSize.{w, w'} G] :
CreatesColimitsOfSize.{w, w'} (F ⋙ G) where CreatesColimitsOfShape := inferInstanceInformal description
Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ creates colimits of any size and $G$ creates colimits of any size for the composition $K \circ F$ where $K \colon J \to C$ is any diagram, then the composition $F \circ G \colon C \to E$ creates colimits of any size.