doc-next-gen

Mathlib.CategoryTheory.Adjunction.Limits

Module docstring

{"# Adjunctions and limits

A left adjoint preserves colimits (CategoryTheory.Adjunction.leftAdjoint_preservesColimits), and a right adjoint preserves limits (CategoryTheory.Adjunction.rightAdjoint_preservesLimits).

Equivalences create and reflect (co)limits. (CategoryTheory.Functor.createsLimitsOfIsEquivalence, CategoryTheory.Functor.createsColimitsOfIsEquivalence, CategoryTheory.Functor.reflectsLimits_of_isEquivalence, CategoryTheory.Functor.reflectsColimits_of_isEquivalence.)

In CategoryTheory.Adjunction.coconesIso we show that when F ⊣ G, the functor associating to each Y the cocones over K ⋙ F with cone point Y is naturally isomorphic to the functor associating to each Y the cocones over K with cone point G.obj Y. "}

CategoryTheory.Adjunction.functorialityRightAdjoint definition
: Cocone (K ⋙ F) ⥤ Cocone K
Full source 
/-- The right adjoint of `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityIsLeftAdjoint`.
-/
def functorialityRightAdjoint : CoconeCocone (K ⋙ F) ⥤ Cocone K :=
  Cocones.functorialityCocones.functoriality _ G ⋙
    Cocones.precompose (K.rightUnitor.inv ≫ whiskerLeft K adj.unit ≫ (associator _ _ _).inv)
Right adjoint of cocone functoriality under adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a functor $K \colon J \to C$, the right adjoint of the cocone functoriality construction is defined as follows: it takes a cocone over $K \circ F$ and returns a cocone over $K$ by: 1. First applying the functoriality construction with $G$ 2. Then precomposing with the natural transformation obtained from: - The right unitor isomorphism of $K$ - Whiskered with the adjunction unit - Composed with the associator isomorphism This construction is auxiliary for proving that the cocone functoriality operation is left adjoint to this operation.
CategoryTheory.Adjunction.functorialityUnit definition
: 𝟭 (Cocone K) ⟶ Cocones.functoriality _ F ⋙ functorialityRightAdjoint adj K
Full source 
/-- The unit for the adjunction for `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityIsLeftAdjoint`.
-/
@[simps]
def functorialityUnit :
    𝟭𝟭 (Cocone K) ⟶ Cocones.functoriality _ F ⋙ functorialityRightAdjoint adj K where
  app c := { hom := adj.unit.app c.pt }
Unit for cocone functoriality adjunction
Informal description
The natural transformation that serves as the unit for the adjunction between the functor `Cocones.functoriality K F` (which takes cocones over $K$ to cocones over $K \circ F$) and its right adjoint. Specifically, for a cocone $c$ over $K$, the component of the unit at $c$ is given by the morphism $\eta_{c.\text{pt}}$, where $\eta$ is the unit of the adjunction $F \dashv G$.
CategoryTheory.Adjunction.functorialityCounit definition
: functorialityRightAdjoint adj K ⋙ Cocones.functoriality _ F ⟶ 𝟭 (Cocone (K ⋙ F))
Full source 
/-- The counit for the adjunction for `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityIsLeftAdjoint`.
-/
@[simps]
def functorialityCounit :
    functorialityRightAdjointfunctorialityRightAdjoint adj K ⋙ Cocones.functoriality _ FfunctorialityRightAdjoint adj K ⋙ Cocones.functoriality _ F ⟶ 𝟭 (Cocone (K ⋙ F)) where
  app c := { hom := adj.counit.app c.pt }
Counit for cocone functoriality adjunction
Informal description
The counit natural transformation for the adjunction involving the cocone functoriality construction. Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a functor $K \colon J \to C$, this counit is defined as follows: for any cocone $c$ over $K \circ F$, the component at $c$ is given by the counit of the adjunction evaluated at the cocone point $c.\text{pt}$. This is an auxiliary definition used in establishing that the cocone functoriality operation is left adjoint to its right adjoint construction.
CategoryTheory.Adjunction.functorialityAdjunction definition
: Cocones.functoriality K F ⊣ functorialityRightAdjoint adj K
Full source 
/-- The functor `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)` is a left adjoint. -/
def functorialityAdjunction : Cocones.functorialityCocones.functoriality K F ⊣ functorialityRightAdjoint adj K where
  unit := functorialityUnit adj K
  counit := functorialityCounit adj K
Adjunction between cocone functoriality constructions
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a functor $K \colon J \to C$, the functor `Cocones.functoriality K F` (which sends cocones over $K$ to cocones over $K \circ F$) is left adjoint to the functor `functorialityRightAdjoint adj K` (which sends cocones over $K \circ F$ to cocones over $K$). The unit and counit of this adjunction are given by the unit and counit of the original adjunction $F \dashv G$ applied to the cocone points.
CategoryTheory.Adjunction.leftAdjoint_preservesColimits theorem
: PreservesColimitsOfSize.{v, u} F
Full source 
/-- A left adjoint preserves colimits. -/
@[stacks 0038]
lemma leftAdjoint_preservesColimits : PreservesColimitsOfSize.{v, u} F where
  preservesColimitsOfShape :=
    { preservesColimit :=
        { preserves := fun hc =>
            ⟨IsColimit.isoUniqueCoconeMorphism.inv fun _ =>
              @Equiv.unique _ _ (IsColimit.isoUniqueCoconeMorphism.hom hc _)
                ((adj.functorialityAdjunction _).homEquiv _ _)⟩ } }
Left Adjoint Functors Preserve Colimits
Informal description
If $F \colon C \to D$ is a left adjoint functor between categories $C$ and $D$, then $F$ preserves all colimits (of any size). That is, for any diagram $K \colon J \to C$ and any colimit cocone $(c, \iota)$ over $K$, the image $(Fc, F\iota)$ is a colimit cocone over $F \circ K$ in $D$.
CategoryTheory.Adjunction.leftAdjointPreservesColimits theorem
: PreservesColimitsOfSize.{v, u} F
Full source 
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma leftAdjointPreservesColimits : PreservesColimitsOfSize.{v, u} F :=
  adj.leftAdjoint_preservesColimits
Left Adjoint Functors Preserve Colimits
Informal description
If $F \colon C \to D$ is a left adjoint functor between categories $C$ and $D$, then $F$ preserves all colimits (of any size). That is, for any diagram $K \colon J \to C$ and any colimit cocone $(c, \iota)$ over $K$, the image $(Fc, F\iota)$ is a colimit cocone over $F \circ K$ in $D$.
CategoryTheory.Adjunction.colim_preservesColimits instance
[HasColimitsOfShape J C] : PreservesColimits (colim (J := J) (C := C))
Full source 
noncomputable
instance colim_preservesColimits [HasColimitsOfShape J C] :
    PreservesColimits (colim (J := J) (C := C)) :=
  colimConstAdj.leftAdjoint_preservesColimits
The Colimit Functor Preserves Colimits
Informal description
For any category $C$ that has colimits of shape $J$, the colimit functor $\text{colim} \colon (J \to C) \to C$ preserves all colimits. That is, given a diagram $K \colon I \to (J \to C)$ with a colimit cocone $(F, \iota)$, the image $(\text{colim}\, F, \text{colim}\, \iota)$ is a colimit cocone over $\text{colim} \circ K$ in $C$.
CategoryTheory.Adjunction.isEquivalence_preservesColimits instance
(E : C ⥤ D) [E.IsEquivalence] : PreservesColimitsOfSize.{v, u} E
Full source 
noncomputable instance (priority := 100) isEquivalence_preservesColimits
    (E : C ⥤ D) [E.IsEquivalence] :
    PreservesColimitsOfSize.{v, u} E :=
  leftAdjoint_preservesColimits E.adjunction
Equivalences Preserve Colimits
Informal description
If $E \colon C \to D$ is an equivalence of categories, then $E$ preserves all colimits (of any size). That is, for any diagram $K \colon J \to C$ and any colimit cocone $(c, \iota)$ over $K$, the image $(E c, E \iota)$ is a colimit cocone over $E \circ K$ in $D$.
CategoryTheory.Functor.reflectsColimits_of_isEquivalence instance
(E : D ⥤ C) [E.IsEquivalence] : ReflectsColimitsOfSize.{v, u} E
Full source 
noncomputable instance (priority := 100)
    _root_.CategoryTheory.Functor.reflectsColimits_of_isEquivalence
    (E : D ⥤ C) [E.IsEquivalence] :
    ReflectsColimitsOfSize.{v, u} E where
  reflectsColimitsOfShape :=
    { reflectsColimit :=
        { reflects := fun t =>
          ⟨(isColimitOfPreserves E.inv t).mapCoconeEquiv E.asEquivalence.unitIso.symm⟩ } }
Equivalences Reflect Colimits
Informal description
For any equivalence of categories $E \colon D \to C$, the functor $E$ reflects all colimits (of any size). That is, given a diagram $K \colon J \to D$ and a cocone $(c, \iota)$ over $K$, if the image $(E c, E \iota)$ is a colimit cocone over $E \circ K$ in $C$, then $(c, \iota)$ is a colimit cocone over $K$ in $D$.
CategoryTheory.Adjunction.isEquivalenceReflectsColimits theorem
(E : D ⥤ C) [E.IsEquivalence] : ReflectsColimitsOfSize.{v, u} E
Full source 
@[deprecated "No deprecation message was provided." (since := "2024-11-18")]
lemma isEquivalenceReflectsColimits (E : D ⥤ C) [E.IsEquivalence] :
    ReflectsColimitsOfSize.{v, u} E :=
  Functor.reflectsColimits_of_isEquivalence E
Equivalences Reflect Colimits
Informal description
For any equivalence of categories $E \colon D \to C$, the functor $E$ reflects all colimits (of any size). That is, given a diagram $K \colon J \to D$ and a cocone $(c, \iota)$ over $K$, if the image $(E c, E \iota)$ is a colimit cocone over $E \circ K$ in $C$, then $(c, \iota)$ is a colimit cocone over $K$ in $D$.
CategoryTheory.Functor.createsColimitsOfIsEquivalence instance
(H : D ⥤ C) [H.IsEquivalence] : CreatesColimitsOfSize.{v, u} H
Full source 
noncomputable instance (priority := 100)
    _root_.CategoryTheory.Functor.createsColimitsOfIsEquivalence (H : D ⥤ C)
    [H.IsEquivalence] :
    CreatesColimitsOfSize.{v, u} H where
  CreatesColimitsOfShape :=
    { CreatesColimit :=
        { lifts := fun c _ =>
            { liftedCocone := mapCoconeInv H c
              validLift := mapCoconeMapCoconeInv H c } } }
Equivalences Create Colimits
Informal description
An equivalence of categories $H \colon D \to C$ creates colimits of any size. That is, for any functor $F \colon J \to D$, if the composition $F \circ H$ has a colimit cocone in $C$, then $F$ has a colimit cocone in $D$ which is mapped by $H$ to the original colimit cocone, and $H$ reflects colimits for $F$.
CategoryTheory.Adjunction.hasColimit_comp_equivalence theorem
(E : C ⥤ D) [E.IsEquivalence] [HasColimit K] : HasColimit (K ⋙ E)
Full source 
theorem hasColimit_comp_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimit K] :
    HasColimit (K ⋙ E) :=
  HasColimit.mk
    { cocone := E.mapCocone (colimit.cocone K)
      isColimit := isColimitOfPreserves _ (colimit.isColimit K) }
Composition with Equivalence Preserves Colimits
Informal description
Let $E \colon C \to D$ be an equivalence of categories and $K \colon J \to C$ a functor. If $K$ has a colimit in $C$, then the composition $K \circ E$ has a colimit in $D$.
CategoryTheory.Adjunction.hasColimit_of_comp_equivalence theorem
(E : C ⥤ D) [E.IsEquivalence] [HasColimit (K ⋙ E)] : HasColimit K
Full source 
theorem hasColimit_of_comp_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimit (K ⋙ E)] :
    HasColimit K := by
  rw [hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]
  exact hasColimit_comp_equivalence (K ⋙ E) E.inv
Existence of Colimit via Composition with Equivalence
Informal description
Let $E \colon C \to D$ be an equivalence of categories and $K \colon J \to C$ a functor. If the composition $K \circ E$ has a colimit in $D$, then $K$ has a colimit in $C$.
CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence theorem
(E : C ⥤ D) [E.IsEquivalence] [HasColimitsOfShape J D] : HasColimitsOfShape J C
Full source 
/-- Transport a `HasColimitsOfShape` instance across an equivalence. -/
theorem hasColimitsOfShape_of_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimitsOfShape J D] :
    HasColimitsOfShape J C :=
  ⟨fun F => hasColimit_of_comp_equivalence F E⟩
Equivalence Preserves Existence of Colimits of Given Shape
Informal description
Let $E \colon C \to D$ be an equivalence of categories. If $D$ has colimits of shape $J$, then $C$ also has colimits of shape $J$.
CategoryTheory.Adjunction.has_colimits_of_equivalence theorem
(E : C ⥤ D) [E.IsEquivalence] [HasColimitsOfSize.{v, u} D] : HasColimitsOfSize.{v, u} C
Full source 
/-- Transport a `HasColimitsOfSize` instance across an equivalence. -/
theorem has_colimits_of_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimitsOfSize.{v, u} D] :
    HasColimitsOfSize.{v, u} C :=
  ⟨fun _ _ => hasColimitsOfShape_of_equivalence E⟩
Equivalence Preserves All Colimits of Given Size
Informal description
Let $E \colon C \to D$ be an equivalence of categories. If $D$ has all colimits of size $(v, u)$, then $C$ also has all colimits of size $(v, u)$.
CategoryTheory.Adjunction.functorialityLeftAdjoint definition
: Cone (K ⋙ G) ⥤ Cone K
Full source 
/-- The left adjoint of `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityIsRightAdjoint`.
-/
def functorialityLeftAdjoint : ConeCone (K ⋙ G) ⥤ Cone K :=
  Cones.functorialityCones.functoriality _ F ⋙
    Cones.postcompose ((associator _ _ _).hom ≫ whiskerLeft K adj.counit ≫ K.rightUnitor.hom)
Left adjoint of cone functoriality under composition with $G$
Informal description
The left adjoint of the functor that maps cones over a diagram $K$ to cones over the composition $K \circ G$, where $G$ is a functor. This construction is an auxiliary definition used in proving that the functoriality operation is a right adjoint. More precisely, given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a diagram $K \colon J \to D$, the functor `functorialityLeftAdjoint` maps a cone over $K \circ G$ to a cone over $K$ by: 1. First applying the functoriality operation with $F$ to obtain a cone over $K \circ G \circ F$. 2. Then postcomposing with a natural transformation built from the adjunction counit and the right unitor of $K$.
CategoryTheory.Adjunction.functorialityUnit' definition
: 𝟭 (Cone (K ⋙ G)) ⟶ functorialityLeftAdjoint adj K ⋙ Cones.functoriality _ G
Full source 
/-- The unit for the adjunction for `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityIsRightAdjoint`.
-/
@[simps]
def functorialityUnit' :
    𝟭𝟭 (Cone (K ⋙ G)) ⟶ functorialityLeftAdjoint adj K ⋙ Cones.functoriality _ G where
  app c := { hom := adj.unit.app c.pt }
Unit transformation for cone functoriality adjunction
Informal description
The natural transformation that serves as the unit for the adjunction involving the functoriality of cones under composition with a functor $G$. Specifically, given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a diagram $K \colon J \to D$, the unit transformation maps a cone $c$ over $K \circ G$ to a cone over $K$ by applying the adjunction unit $\eta_{c.\mathrm{pt}}$ at the cone point of $c$.
CategoryTheory.Adjunction.functorialityCounit' definition
: Cones.functoriality _ G ⋙ functorialityLeftAdjoint adj K ⟶ 𝟭 (Cone K)
Full source 
/-- The counit for the adjunction for `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityIsRightAdjoint`.
-/
@[simps]
def functorialityCounit' :
    Cones.functorialityCones.functoriality _ G ⋙ functorialityLeftAdjoint adj KCones.functoriality _ G ⋙ functorialityLeftAdjoint adj K ⟶ 𝟭 (Cone K) where
  app c := { hom := adj.counit.app c.pt }
Counit for cone functoriality adjunction
Informal description
The counit natural transformation for the adjunction involving the functoriality of cones under composition with a functor $G$. Specifically, given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a diagram $K \colon J \to D$, this counit is a natural transformation from the composition of the functoriality operation with $G$ followed by the left adjoint, to the identity functor on the category of cones over $K$. For each cone $c$ over $K$, the component of the counit at $c$ is given by the morphism $\mathrm{adj.counit.app}\, c.\mathrm{pt} \colon (G \circ F)(c.\mathrm{pt}) \to c.\mathrm{pt}$ in $D$, where $\mathrm{adj.counit}$ is the counit of the adjunction $F \dashv G$.
CategoryTheory.Adjunction.functorialityAdjunction' definition
: functorialityLeftAdjoint adj K ⊣ Cones.functoriality K G
Full source 
/-- The functor `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)` is a right adjoint. -/
def functorialityAdjunction' : functorialityLeftAdjointfunctorialityLeftAdjoint adj K ⊣ Cones.functoriality K G where
  unit := functorialityUnit' adj K
  counit := functorialityCounit' adj K
Adjunction for cone functoriality under composition with $G$
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a diagram $K \colon J \to D$, the functor `Cones.functoriality K G` that maps cones over $K$ to cones over $K \circ G$ is a right adjoint. The left adjoint is constructed using the adjunction counit and the right unitor of $K$. The unit and counit of this adjunction are given by natural transformations: - The unit $\eta$ maps a cone $c$ over $K \circ G$ to a cone over $K$ by applying the adjunction unit $\eta_{c.\mathrm{pt}}$ at the cone point of $c$. - The counit $\epsilon$ maps a cone $c$ over $K$ to a cone over $K$ by applying the adjunction counit $\epsilon_{c.\mathrm{pt}}$ at the cone point of $c$.
CategoryTheory.Adjunction.rightAdjoint_preservesLimits theorem
: PreservesLimitsOfSize.{v, u} G
Full source 
/-- A right adjoint preserves limits. -/
@[stacks 0038]
lemma rightAdjoint_preservesLimits : PreservesLimitsOfSize.{v, u} G where
  preservesLimitsOfShape :=
    { preservesLimit :=
        { preserves := fun hc =>
            ⟨IsLimit.isoUniqueConeMorphism.inv fun _ =>
              @Equiv.unique _ _ (IsLimit.isoUniqueConeMorphism.hom hc _)
                ((adj.functorialityAdjunction' _).homEquiv _ _).symm⟩ } }
Right Adjoints Preserve Limits
Informal description
If $F \dashv G$ is an adjunction between functors $F \colon C \to D$ and $G \colon D \to C$, then the right adjoint $G$ preserves all limits (of any size). That is, for any diagram $K \colon J \to D$ and limit cone $t$ over $K$, the image $G(t)$ is a limit cone over $G \circ K$.
CategoryTheory.Adjunction.rightAdjointPreservesLimits theorem
: PreservesLimitsOfSize.{v, u} G
Full source 
@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
lemma rightAdjointPreservesLimits : PreservesLimitsOfSize.{v, u} G :=
  adj.rightAdjoint_preservesLimits
Right Adjoints Preserve Limits
Informal description
If $F \dashv G$ is an adjunction between functors $F \colon C \to D$ and $G \colon D \to C$, then the right adjoint $G$ preserves all limits (of any size). That is, for any diagram $K \colon J \to D$ and limit cone $t$ over $K$, the image $G(t)$ is a limit cone over $G \circ K$.
CategoryTheory.Adjunction.lim_preservesLimits instance
[HasLimitsOfShape J C] : PreservesLimits (lim (J := J) (C := C))
Full source 
instance lim_preservesLimits [HasLimitsOfShape J C] :
    PreservesLimits (lim (J := J) (C := C)) :=
  constLimAdj.rightAdjoint_preservesLimits
The Limit Functor Preserves Limits
Informal description
For any category $\mathcal{C}$ that has limits of shape $J$, the limit functor $\text{lim} \colon (J \to \mathcal{C}) \to \mathcal{C}$ preserves all limits. That is, $\text{lim}$ maps limit cones in the functor category $J \to \mathcal{C}$ to limit cones in $\mathcal{C}$.
CategoryTheory.Adjunction.isEquivalencePreservesLimits instance
(E : D ⥤ C) [E.IsEquivalence] : PreservesLimitsOfSize.{v, u} E
Full source 
instance (priority := 100) isEquivalencePreservesLimits
    (E : D ⥤ C) [E.IsEquivalence] :
    PreservesLimitsOfSize.{v, u} E :=
  rightAdjoint_preservesLimits E.asEquivalence.symm.toAdjunction
Equivalences Preserve Limits
Informal description
For any equivalence of categories $E \colon D \to C$, the functor $E$ preserves all limits (of any size). That is, for any diagram $K \colon J \to D$ and limit cone $t$ over $K$, the image $E(t)$ is a limit cone over $E \circ K$.
CategoryTheory.Functor.reflectsLimits_of_isEquivalence instance
(E : D ⥤ C) [E.IsEquivalence] : ReflectsLimitsOfSize.{v, u} E
Full source 
noncomputable instance (priority := 100)
    _root_.CategoryTheory.Functor.reflectsLimits_of_isEquivalence
    (E : D ⥤ C) [E.IsEquivalence] :
    ReflectsLimitsOfSize.{v, u} E where
  reflectsLimitsOfShape :=
    { reflectsLimit :=
        { reflects := fun t =>
            ⟨(isLimitOfPreserves E.inv t).mapConeEquiv E.asEquivalence.unitIso.symm⟩ } }
Equivalences Reflect Limits
Informal description
For any equivalence of categories $E \colon D \to C$, the functor $E$ reflects all limits (of any size). That is, given a diagram $K \colon J \to D$ and a cone $t$ over $K$, if the image $E(t)$ is a limit cone over $E \circ K$ in $C$, then $t$ must be a limit cone over $K$ in $D$.
CategoryTheory.Adjunction.isEquivalenceReflectsLimits theorem
(E : D ⥤ C) [E.IsEquivalence] : ReflectsLimitsOfSize.{v, u} E
Full source 
@[deprecated "No deprecation message was provided." (since := "2024-11-18")]
lemma isEquivalenceReflectsLimits (E : D ⥤ C) [E.IsEquivalence] :
    ReflectsLimitsOfSize.{v, u} E :=
  Functor.reflectsLimits_of_isEquivalence E
Equivalences Reflect Limits of Any Size
Informal description
For any equivalence of categories $E \colon D \to C$, the functor $E$ reflects all limits (of any size). That is, given a diagram $K \colon J \to D$ and a cone $t$ over $K$, if the image $E(t)$ is a limit cone over $E \circ K$ in $C$, then $t$ must be a limit cone over $K$ in $D$.
CategoryTheory.Functor.createsLimitsOfIsEquivalence instance
(H : D ⥤ C) [H.IsEquivalence] : CreatesLimitsOfSize.{v, u} H
Full source 
noncomputable instance (priority := 100)
    _root_.CategoryTheory.Functor.createsLimitsOfIsEquivalence (H : D ⥤ C) [H.IsEquivalence] :
    CreatesLimitsOfSize.{v, u} H where
  CreatesLimitsOfShape :=
    { CreatesLimit :=
        { lifts := fun c _ =>
            { liftedCone := mapConeInv H c
              validLift := mapConeMapConeInv H c } } }
Equivalences Create Limits of Any Size
Informal description
For any equivalence of categories $H \colon D \to C$, the functor $H$ creates limits of any size. This means that given any limit cone in $C$ for the composition $K \circ H$ (where $K$ is a diagram in $D$), there exists a lift to a limit cone in $D$, and $H$ reflects limits for $K$.
CategoryTheory.Adjunction.hasLimit_comp_equivalence theorem
(E : D ⥤ C) [E.IsEquivalence] [HasLimit K] : HasLimit (K ⋙ E)
Full source 
theorem hasLimit_comp_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimit K] : HasLimit (K ⋙ E) :=
  HasLimit.mk
    { cone := E.mapCone (limit.cone K)
      isLimit := isLimitOfPreserves _ (limit.isLimit K) }
Existence of Limits under Composition with Equivalence
Informal description
Given an equivalence of categories $E \colon D \to C$ and a functor $K \colon J \to D$ that has a limit in $D$, the composition $K \circ E$ has a limit in $C$.
CategoryTheory.Adjunction.hasLimit_of_comp_equivalence theorem
(E : D ⥤ C) [E.IsEquivalence] [HasLimit (K ⋙ E)] : HasLimit K
Full source 
theorem hasLimit_of_comp_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimit (K ⋙ E)] :
    HasLimit K := by
  rw [← hasLimit_iff_of_iso
    (isoWhiskerLeftisoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]
  exact hasLimit_comp_equivalence (K ⋙ E) E.inv
Existence of Limits under Precomposition with Equivalence
Informal description
Given an equivalence of categories $E \colon D \to C$ and a functor $K \colon J \to D$, if the composition $K \circ E$ has a limit in $C$, then $K$ has a limit in $D$.
CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence theorem
(E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfShape J C] : HasLimitsOfShape J D
Full source 
/-- Transport a `HasLimitsOfShape` instance across an equivalence. -/
theorem hasLimitsOfShape_of_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfShape J C] :
    HasLimitsOfShape J D :=
  ⟨fun F => hasLimit_of_comp_equivalence F E⟩
Preservation of Limits of Shape under Equivalence of Categories
Informal description
Given an equivalence of categories $E \colon D \to C$ and that $C$ has limits of shape $J$, then $D$ also has limits of shape $J$.
CategoryTheory.Adjunction.has_limits_of_equivalence theorem
(E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfSize.{v, u} C] : HasLimitsOfSize.{v, u} D
Full source 
/-- Transport a `HasLimitsOfSize` instance across an equivalence. -/
theorem has_limits_of_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfSize.{v, u} C] :
    HasLimitsOfSize.{v, u} D :=
  ⟨fun _ _ => hasLimitsOfShape_of_equivalence E⟩
Preservation of All Limits under Equivalence of Categories
Informal description
Given an equivalence of categories $E \colon D \to C$ and that $C$ has all limits of size $(v, u)$, then $D$ also has all limits of size $(v, u)$.
CategoryTheory.Adjunction.coconesIsoComponentHom definition
{J : Type u} [Category.{v} J] {K : J ⥤ C} (Y : D) (t : ((cocones J D).obj (op (K ⋙ F))).obj Y) : (G ⋙ (cocones J C).obj (op K)).obj Y
Full source 
/-- auxiliary construction for `coconesIso` -/
@[simp]
def coconesIsoComponentHom {J : Type u} [Category.{v} J] {K : J ⥤ C} (Y : D)
    (t : ((cocones J D).obj (op (K ⋙ F))).obj Y) : (G ⋙ (cocones J C).obj (op K)).obj Y where
  app j := (adj.homEquiv (K.obj j) Y) (t.app j)
  naturality j j' f := by
    rw [← adj.homEquiv_naturality_left, ← Functor.comp_map, t.naturality]
    simp
Component of the cocone isomorphism for an adjunction
Informal description
For a fixed adjunction $F \dashv G$ between categories $C$ and $D$, and a functor $K \colon J \to C$, the component of the natural isomorphism between cocone functors at an object $Y \in D$ takes a cocone $t$ over $K \circ F$ with vertex $Y$ to a cocone over $K$ with vertex $G(Y)$. The components of this cocone are given by applying the adjunction hom-equivalence at each object $j \in J$ to the corresponding component of $t$.
CategoryTheory.Adjunction.coconesIsoComponentInv definition
{J : Type u} [Category.{v} J] {K : J ⥤ C} (Y : D) (t : (G ⋙ (cocones J C).obj (op K)).obj Y) : ((cocones J D).obj (op (K ⋙ F))).obj Y
Full source 
/-- auxiliary construction for `coconesIso` -/
@[simp]
def coconesIsoComponentInv {J : Type u} [Category.{v} J] {K : J ⥤ C} (Y : D)
    (t : (G ⋙ (cocones J C).obj (op K)).obj Y) : ((cocones J D).obj (op (K ⋙ F))).obj Y where
  app j := (adj.homEquiv (K.obj j) Y).symm (t.app j)
  naturality j j' f := by
    erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm, t.naturality]
    dsimp; simp
Inverse component of cocone isomorphism under adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, a small category $J$, and a diagram $K \colon J \to C$, the component of the inverse natural isomorphism at an object $Y \in D$ maps a cocone over $K$ with apex $G(Y)$ to a cocone over $K \circ F$ with apex $Y$. Specifically, for each object $j \in J$, the component at $j$ is given by applying the inverse of the adjunction's hom-equivalence to the corresponding component of the input cocone.
CategoryTheory.Adjunction.conesIsoComponentHom definition
{J : Type u} [Category.{v} J] {K : J ⥤ D} (X : Cᵒᵖ) (t : (Functor.op F ⋙ (cones J D).obj K).obj X) : ((cones J C).obj (K ⋙ G)).obj X
Full source 
/-- auxiliary construction for `conesIso` -/
@[simp]
def conesIsoComponentHom {J : Type u} [Category.{v} J] {K : J ⥤ D} (X : Cᵒᵖ)
    (t : (Functor.opFunctor.op F ⋙ (cones J D).obj K).obj X) : ((cones J C).obj (K ⋙ G)).obj X where
  app j := (adj.homEquiv (unop X) (K.obj j)) (t.app j)
  naturality j j' f := by
    erw [← adj.homEquiv_naturality_right, ← t.naturality, Category.id_comp, Category.id_comp]
    rfl
Component of Cones Isomorphism in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between categories $C$ and $D$, a small category $J$, and a functor $K \colon J \to D$, the component of the cones isomorphism at an object $X \in C^{\mathrm{op}}$ maps a cone $t$ over $K \circ F^{\mathrm{op}}$ with apex $X$ to a cone over $K \circ G$ with apex $X$. Specifically, for each object $j \in J$, the component at $j$ is given by the adjunction hom-equivalence applied to the corresponding component of $t$.
CategoryTheory.Adjunction.conesIsoComponentInv definition
{J : Type u} [Category.{v} J] {K : J ⥤ D} (X : Cᵒᵖ) (t : ((cones J C).obj (K ⋙ G)).obj X) : (Functor.op F ⋙ (cones J D).obj K).obj X
Full source 
/-- auxiliary construction for `conesIso` -/
@[simp]
def conesIsoComponentInv {J : Type u} [Category.{v} J] {K : J ⥤ D} (X : Cᵒᵖ)
    (t : ((cones J C).obj (K ⋙ G)).obj X) : (Functor.opFunctor.op F ⋙ (cones J D).obj K).obj X where
  app j := (adj.homEquiv (unop X) (K.obj j)).symm (t.app j)
  naturality j j' f := by
    erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]
Inverse component of cones isomorphism under adjunction
Informal description
Given an adjunction $F \dashv G$ between categories $C$ and $D$, a small category $J$, and a functor $K \colon J \to D$, the component of the inverse natural isomorphism for cones at an object $X \in C^{\mathrm{op}}$ takes a cone $t$ over the composed functor $K \circ G$ with vertex $X$ and returns a cone over $K$ with vertex $F(X)$. More precisely, for each object $j \in J$, the component at $j$ is obtained by applying the inverse of the adjunction's hom-equivalence to the corresponding component of $t$.
CategoryTheory.Adjunction.coconesIso definition
{J : Type u} [Category.{v} J] {K : J ⥤ C} : (cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ (cocones J C).obj (op K)
Full source 
/-- When `F ⊣ G`,
the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
is naturally isomorphic to
the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
-/
def coconesIso {J : Type u} [Category.{v} J] {K : J ⥤ C} :
    (cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ (cocones J C).obj (op K) :=
  NatIso.ofComponents fun Y =>
    { hom := coconesIsoComponentHom adj Y
      inv := coconesIsoComponentInv adj Y }
Natural isomorphism of cocone functors under adjunction
Informal description
Given an adjunction \( F \dashv G \) between categories \( C \) and \( D \), and a functor \( K \colon J \to C \), there is a natural isomorphism between the functor that sends each object \( Y \in D \) to the cocones over \( K \circ F \) with vertex \( Y \), and the functor that sends each \( Y \in D \) to the cocones over \( K \) with vertex \( G(Y) \).
CategoryTheory.Adjunction.conesIso definition
{J : Type u} [Category.{v} J] {K : J ⥤ D} : F.op ⋙ (cones J D).obj K ≅ (cones J C).obj (K ⋙ G)
Full source 
/-- When `F ⊣ G`,
the functor associating to each `X` the cones over `K` with cone point `F.op.obj X`
is naturally isomorphic to
the functor associating to each `X` the cones over `K ⋙ G` with cone point `X`.
-/
def conesIso {J : Type u} [Category.{v} J] {K : J ⥤ D} :
    F.op ⋙ (cones J D).obj KF.op ⋙ (cones J D).obj K ≅ (cones J C).obj (K ⋙ G) :=
  NatIso.ofComponents fun X =>
    { hom := conesIsoComponentHom adj X
      inv := conesIsoComponentInv adj X }
Natural isomorphism of cones under adjunction
Informal description
Given an adjunction $F \dashv G$ between categories $C$ and $D$, and a functor $K \colon J \to D$ from a small category $J$, there is a natural isomorphism between: 1. The functor that sends an object $X \in C^{\mathrm{op}}$ to cones over $K$ with vertex $F(X)$, and 2. The functor that sends $X$ to cones over $K \circ G$ with vertex $X$. This isomorphism demonstrates how the adjunction $F \dashv G$ relates cones in the two categories.
CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint instance
[IsLeftAdjoint F] : PreservesColimitsOfSize.{v, u} F
Full source 
noncomputable instance [IsLeftAdjoint F] : PreservesColimitsOfSize.{v, u} F where
Left Adjoint Functors Preserve All Colimits
Informal description
For any functor $F$ that is a left adjoint, $F$ preserves all colimits of any size.
CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint instance
[IsRightAdjoint F] : PreservesLimitsOfSize.{v, u} F
Full source 
noncomputable instance [IsRightAdjoint F] : PreservesLimitsOfSize.{v, u} F where
Right Adjoint Functors Preserve All Limits
Informal description
For any functor $F$ that is a right adjoint, $F$ preserves all limits of any size.