Mathlib.CategoryTheory.Limits.Preserves.Basic

CategoryTheory.Limits.PreservesLimit structure

(K : J ⥤ C) (F : C ⥤ D)

Full source

/-- A functor `F` preserves limits of `K` (written as `PreservesLimit K F`)
if `F` maps any limit cone over `K` to a limit cone.
-/
class PreservesLimit (K : J ⥤ C) (F : C ⥤ D) : Prop where
  preserves {c : Cone K} (hc : IsLimit c) : Nonempty (IsLimit (F.mapCone c))

Preservation of limits by a functor

Informal description

A functor $ F : C \to D $ preserves limits of a diagram $ K : J \to C $ if $ F $ maps every limit cone over $ K $ to a limit cone in $ D $. This means that $ F $ sends any existing limit of $ K $ in $ C $ to a limit of $ F \circ K $ in $ D $.

CategoryTheory.Limits.PreservesColimit structure

(K : J ⥤ C) (F : C ⥤ D)

Full source

/-- A functor `F` preserves colimits of `K` (written as `PreservesColimit K F`)
if `F` maps any colimit cocone over `K` to a colimit cocone.
-/
class PreservesColimit (K : J ⥤ C) (F : C ⥤ D) : Prop where
  preserves {c : Cocone K} (hc : IsColimit c) : Nonempty (IsColimit (F.mapCocone c))

Preservation of Colimits by a Functor

Informal description

A functor $ F : C \to D $ preserves colimits of a diagram $ K : J \to C $ if $ F $ maps every colimit cocone over $ K $ to a colimit cocone in $ D $. This means that $ F $ sends colimiting cocones in $ C $ to colimiting cocones in $ D $.

CategoryTheory.Limits.PreservesLimitsOfShape structure

(J : Type w) [Category.{w'} J] (F : C ⥤ D)

Full source

/-- We say that `F` preserves limits of shape `J` if `F` preserves limits for every diagram
    `K : J ⥤ C`, i.e., `F` maps limit cones over `K` to limit cones. -/
class PreservesLimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop where
  preservesLimit : ∀ {K : J ⥤ C}, PreservesLimit K F := by infer_instance

Preservation of limits of a given shape by a functor

Informal description

The structure `PreservesLimitsOfShape J F` asserts that the functor $F \colon C \to D$ preserves all limit cones over any diagram $K \colon J \to C$, where $J$ is a small category. Specifically, for any such diagram $K$ that has a limit cone in $C$, the image of this cone under $F$ is a limit cone in $D$.

CategoryTheory.Limits.PreservesColimitsOfShape structure

(J : Type w) [Category.{w'} J] (F : C ⥤ D)

Full source

/-- We say that `F` preserves colimits of shape `J` if `F` preserves colimits for every diagram
    `K : J ⥤ C`, i.e., `F` maps colimit cocones over `K` to colimit cocones. -/
class PreservesColimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop where
  preservesColimit : ∀ {K : J ⥤ C}, PreservesColimit K F := by infer_instance

Preservation of colimits of a given shape by a functor

Informal description

The structure `PreservesColimitsOfShape J F` asserts that the functor $F \colon C \to D$ preserves all colimit cocones over any diagram $K \colon J \to C$. Specifically, for any diagram $K$ of shape $J$ in $C$ that has a colimit cocone, the image of this cocone under $F$ is a colimit cocone in $D$.

CategoryTheory.Limits.PreservesLimitsOfSize structure

(F : C ⥤ D)

Full source

/-- `PreservesLimitsOfSize.{v u} F` means that `F` sends all limit cones over any
diagram `J ⥤ C` to limit cones, where `J : Type u` with `[Category.{v} J]`. -/
@[nolint checkUnivs, pp_with_univ]
class PreservesLimitsOfSize (F : C ⥤ D) : Prop where
  preservesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], PreservesLimitsOfShape J F := by
    infer_instance

Preservation of limits of a given size by a functor

Informal description

The structure `PreservesLimitsOfSize F` asserts that the functor $F \colon C \to D$ preserves all limit cones over any diagram $J \to C$, where $J$ is a category of a certain size. Specifically, for any diagram $K \colon J \to C$ that has a limit cone in $C$, the image of this cone under $F$ is a limit cone in $D$.

CategoryTheory.Limits.PreservesLimits abbrev

(F : C ⥤ D)

Full source

/-- We say that `F` preserves (small) limits if it sends small
limit cones over any diagram to limit cones. -/
abbrev PreservesLimits (F : C ⥤ D) :=
  PreservesLimitsOfSize.{v₂, v₂} F

Preservation of Small Limits by a Functor

Informal description

A functor $F \colon C \to D$ preserves (small) limits if for every small diagram $K \colon J \to C$ that has a limit cone in $C$, the image of this cone under $F$ is a limit cone in $D$.

CategoryTheory.Limits.PreservesColimitsOfSize structure

(F : C ⥤ D)

Full source

/-- `PreservesColimitsOfSize.{v u} F` means that `F` sends all colimit cocones over any
diagram `J ⥤ C` to colimit cocones, where `J : Type u` with `[Category.{v} J]`. -/
@[nolint checkUnivs, pp_with_univ]
class PreservesColimitsOfSize (F : C ⥤ D) : Prop where
  preservesColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], PreservesColimitsOfShape J F := by
    infer_instance

Preservation of colimits of a given size by a functor

Informal description

The structure `PreservesColimitsOfSize F` asserts that the functor $F \colon C \to D$ preserves all colimit cocones over any diagram $J \to C$, where $J$ is a category of a certain size. Specifically, for any diagram $K \colon J \to C$ that has a colimit cocone in $C$, the image of this cocone under $F$ is a colimit cocone in $D$.

CategoryTheory.Limits.PreservesColimits abbrev

(F : C ⥤ D)

Full source

/-- We say that `F` preserves (small) limits if it sends small
limit cones over any diagram to limit cones. -/
abbrev PreservesColimits (F : C ⥤ D) :=
  PreservesColimitsOfSize.{v₂, v₂} F

Preservation of Small Colimits by a Functor

Informal description

A functor $F \colon C \to D$ preserves (small) colimits if for every small diagram $K \colon J \to C$ that has a colimit cocone in $C$, the image of this cocone under $F$ is a colimit cocone in $D$.

CategoryTheory.Limits.isLimitOfPreserves definition

(F : C ⥤ D) {c : Cone K} (t : IsLimit c) [PreservesLimit K F] : IsLimit (F.mapCone c)

Full source

/-- A convenience function for `PreservesLimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
-/
def isLimitOfPreserves (F : C ⥤ D) {c : Cone K} (t : IsLimit c) [PreservesLimit K F] :
    IsLimit (F.mapCone c) :=
  (PreservesLimit.preserves t).some

Preservation of limit cones under a functor

Informal description

Given a functor $ F \colon C \to D $ that preserves limits of a diagram $ K \colon J \to C $, and a limit cone $ c $ over $ K $ in $ C $, the image of $ c $ under $ F $ is a limit cone over $ F \circ K $ in $ D $. In other words, if $ c $ is a limit cone in $ C $, then $ F $ maps it to a limit cone in $ D $.

CategoryTheory.Limits.isColimitOfPreserves definition

(F : C ⥤ D) {c : Cocone K} (t : IsColimit c) [PreservesColimit K F] : IsColimit (F.mapCocone c)

Full source

/--
A convenience function for `PreservesColimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
-/
def isColimitOfPreserves (F : C ⥤ D) {c : Cocone K} (t : IsColimit c) [PreservesColimit K F] :
    IsColimit (F.mapCocone c) :=
  (PreservesColimit.preserves t).some

Preservation of colimit cocones under a functor

Informal description

Given a functor $ F : C \to D $ that preserves colimits of a diagram $ K : J \to C $, and a colimit cocone $ c $ over $ K $ in $ C $, the image of $ c $ under $ F $ is a colimit cocone in $ D $.

CategoryTheory.Limits.preservesLimit_subsingleton instance

(K : J ⥤ C) (F : C ⥤ D) : Subsingleton (PreservesLimit K F)

Full source

instance preservesLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) :
    Subsingleton (PreservesLimit K F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Preservation Proofs

Informal description

For any diagram $K \colon J \to C$ and functor $F \colon C \to D$, the type of proofs that $F$ preserves limits of $K$ is a subsingleton (i.e., any two such proofs are equal).

CategoryTheory.Limits.preservesColimit_subsingleton instance

(K : J ⥤ C) (F : C ⥤ D) : Subsingleton (PreservesColimit K F)

Full source

instance preservesColimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) :
    Subsingleton (PreservesColimit K F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Colimit Preservation Proofs

Informal description

For any diagram $K \colon J \to C$ and functor $F \colon C \to D$, the type of proofs that $F$ preserves colimits of $K$ is a subsingleton (i.e., any two such proofs are equal).

CategoryTheory.Limits.preservesLimitsOfShape_subsingleton instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) : Subsingleton (PreservesLimitsOfShape J F)

Full source

instance preservesLimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
    Subsingleton (PreservesLimitsOfShape J F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Preservation Proofs for a Functor

Informal description

For any small category $J$ and functor $F \colon C \to D$, the type of proofs that $F$ preserves all limits of shape $J$ is a subsingleton (i.e., has at most one element up to propositional equality).

CategoryTheory.Limits.preservesColimitsOfShape_subsingleton instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) : Subsingleton (PreservesColimitsOfShape J F)

Full source

instance preservesColimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
    Subsingleton (PreservesColimitsOfShape J F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Colimit Preservation Proofs for a Given Shape

Informal description

For any category $J$ and functor $F \colon C \to D$, the type of proofs that $F$ preserves all colimits of shape $J$ is a subsingleton (i.e., has at most one element up to propositional equality).

CategoryTheory.Limits.preservesLimitsOfSize_subsingleton instance

(F : C ⥤ D) : Subsingleton (PreservesLimitsOfSize.{w', w} F)

Full source

instance preservesLimitsOfSize_subsingleton (F : C ⥤ D) :
    Subsingleton (PreservesLimitsOfSize.{w', w} F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Preservation Structure for Functors

Informal description

For any functor $F \colon C \to D$ between categories, the type of instances asserting that $F$ preserves all limits of a given size is a subsingleton. This means there is at most one way for $F$ to preserve all such limits.

CategoryTheory.Limits.preservesColimitsOfSize_subsingleton instance

(F : C ⥤ D) : Subsingleton (PreservesColimitsOfSize.{w', w} F)

Full source

instance preservesColimitsOfSize_subsingleton (F : C ⥤ D) :
    Subsingleton (PreservesColimitsOfSize.{w', w} F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Proofs for Colimit Preservation

Informal description

For any functor $F \colon C \to D$ between categories, the type of proofs that $F$ preserves all colimits of a given size is a subsingleton (i.e., there is at most one such proof).

CategoryTheory.Limits.id_preservesLimitsOfSize instance

: PreservesLimitsOfSize.{w', w} (𝟭 C)

Full source

instance id_preservesLimitsOfSize : PreservesLimitsOfSize.{w', w} (𝟭 C) where
  preservesLimitsOfShape {J} 𝒥 :=
    {
      preservesLimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.lift ⟨s.pt, fun j => s.π.app j, fun _ _ f => s.π.naturality f⟩, by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j, by
            cases K; rcases c with ⟨_, _, _⟩; intro s m w; rcases s with ⟨_, _, _⟩;
              exact h.uniq _ m w⟩⟩ }

Identity Functor Preserves All Limits

Informal description

The identity functor $\mathsf{1}_C \colon C \to C$ preserves all limits of any size in the category $C$.

CategoryTheory.Limits.idPreservesLimits theorem

: PreservesLimitsOfSize.{w', w} (𝟭 C)

Full source

@[deprecated "use id_preservesLimitsOfSize" (since := "2024-11-19")]
lemma idPreservesLimits : PreservesLimitsOfSize.{w', w} (𝟭 C) :=
  id_preservesLimitsOfSize

Identity Functor Preserves All Limits

Informal description

The identity functor $\mathsf{1}_C \colon C \to C$ preserves all limits of any size in the category $C$. That is, for any diagram $K \colon J \to C$ that has a limit cone in $C$, the image of this cone under the identity functor is also a limit cone in $C$.

CategoryTheory.Limits.id_preservesColimitsOfSize instance

: PreservesColimitsOfSize.{w', w} (𝟭 C)

Full source

instance id_preservesColimitsOfSize : PreservesColimitsOfSize.{w', w} (𝟭 C) where
  preservesColimitsOfShape {J} 𝒥 :=
    {
      preservesColimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.desc ⟨s.pt, fun j => s.ι.app j, fun _ _ f => s.ι.naturality f⟩, by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j, by
            cases K; rcases c with ⟨_, _, _⟩; intro s m w; rcases s with ⟨_, _, _⟩;
              exact h.uniq _ m w⟩⟩ }

Identity Functor Preserves All Colimits

Informal description

The identity functor $\text{id} \colon C \to C$ preserves all colimits of any size in the category $C$. That is, for any diagram $K \colon J \to C$ that has a colimit cocone in $C$, the image of this cocone under the identity functor is also a colimit cocone in $C$.

CategoryTheory.Limits.idPreservesColimits theorem

: PreservesColimitsOfSize.{w', w} (𝟭 C)

Full source

@[deprecated "use id_preservesColimitsOfSize" (since := "2024-11-19")]
lemma idPreservesColimits : PreservesColimitsOfSize.{w', w} (𝟭 C) :=
  id_preservesColimitsOfSize

Identity Functor Preserves All Colimits

Informal description

The identity functor $\text{id} \colon C \to C$ preserves all colimits of any size in the category $C$. That is, for any diagram $K \colon J \to C$ that has a colimit cocone in $C$, the image of this cocone under the identity functor is also a colimit cocone in $C$.

CategoryTheory.Limits.instHasLimitCompOfPreservesLimit instance

[HasLimit K] {F : C ⥤ D} [PreservesLimit K F] : HasLimit (K ⋙ F)

Full source

instance [HasLimit K] {F : C ⥤ D} [PreservesLimit K F] : HasLimit (K ⋙ F) where
  exists_limit := ⟨_, isLimitOfPreserves F (limit.isLimit K)⟩

Preservation of Limits Under Functor Composition

Informal description

Given a functor $F \colon C \to D$ that preserves limits of a diagram $K \colon J \to C$, and assuming $K$ has a limit in $C$, then the composition $K \circ F \colon J \to D$ also has a limit in $D$.

CategoryTheory.Limits.instHasColimitCompOfPreservesColimit instance

[HasColimit K] {F : C ⥤ D} [PreservesColimit K F] : HasColimit (K ⋙ F)

Full source

instance [HasColimit K] {F : C ⥤ D} [PreservesColimit K F] : HasColimit (K ⋙ F) where
  exists_colimit := ⟨_, isColimitOfPreserves F (colimit.isColimit K)⟩

Preservation of Colimits Under Functor Composition

Informal description

Given a functor $F \colon C \to D$ that preserves colimits of a diagram $K \colon J \to C$, and assuming $K$ has a colimit in $C$, then the composition $K \circ F \colon J \to D$ also has a colimit in $D$.

CategoryTheory.Limits.comp_preservesLimit instance

[PreservesLimit K F] [PreservesLimit (K ⋙ F) G] : PreservesLimit K (F ⋙ G)

Full source

instance comp_preservesLimit [PreservesLimit K F] [PreservesLimit (K ⋙ F) G] :
    PreservesLimit K (F ⋙ G) where
  preserves hc := ⟨isLimitOfPreserves G (isLimitOfPreserves F hc)⟩

Composition of Limit-Preserving Functors Preserves Limits

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves limits of a diagram $K \colon J \to C$ and $G$ preserves limits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ preserves limits of $K$.

CategoryTheory.Limits.comp_preservesLimitsOfShape instance

[PreservesLimitsOfShape J F] [PreservesLimitsOfShape J G] : PreservesLimitsOfShape J (F ⋙ G)

Full source

instance comp_preservesLimitsOfShape [PreservesLimitsOfShape J F] [PreservesLimitsOfShape J G] :
    PreservesLimitsOfShape J (F ⋙ G) where

Composition of Functors Preserving Limits of a Given Shape

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves all limits of shape $J$ and $G$ preserves all limits of shape $J$, then the composition $F \circ G \colon C \to E$ preserves all limits of shape $J$.

CategoryTheory.Limits.comp_preservesLimits instance

[PreservesLimitsOfSize.{w', w} F] [PreservesLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} (F ⋙ G)

Full source

instance comp_preservesLimits [PreservesLimitsOfSize.{w', w} F] [PreservesLimitsOfSize.{w', w} G] :
    PreservesLimitsOfSize.{w', w} (F ⋙ G) where

Composition of Functors Preserves Limits of a Given Size

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves all limits of a given size and $G$ preserves all limits of the same size, then the composition $F \circ G \colon C \to E$ preserves all limits of that size.

CategoryTheory.Limits.comp_preservesColimit instance

[PreservesColimit K F] [PreservesColimit (K ⋙ F) G] : PreservesColimit K (F ⋙ G)

Full source

instance comp_preservesColimit [PreservesColimit K F] [PreservesColimit (K ⋙ F) G] :
    PreservesColimit K (F ⋙ G) where
  preserves hc := ⟨isColimitOfPreserves G (isColimitOfPreserves F hc)⟩

Preservation of Colimits under Functor Composition

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves colimits of a diagram $K \colon J \to C$ and $G$ preserves colimits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ preserves colimits of $K$.

CategoryTheory.Limits.comp_preservesColimitsOfShape instance

[PreservesColimitsOfShape J F] [PreservesColimitsOfShape J G] : PreservesColimitsOfShape J (F ⋙ G)

Full source

instance comp_preservesColimitsOfShape [PreservesColimitsOfShape J F]
    [PreservesColimitsOfShape J G] : PreservesColimitsOfShape J (F ⋙ G) where

Preservation of Colimits of a Given Shape under Functor Composition

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves all colimits of shape $J$ and $G$ preserves all colimits of shape $J$, then the composition $F \circ G \colon C \to E$ also preserves all colimits of shape $J$.

CategoryTheory.Limits.comp_preservesColimits instance

[PreservesColimitsOfSize.{w', w} F] [PreservesColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} (F ⋙ G)

Full source

instance comp_preservesColimits [PreservesColimitsOfSize.{w', w} F]
    [PreservesColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} (F ⋙ G) where

Composition of Colimit-Preserving Functors Preserves Colimits

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves all colimits and $G$ preserves all colimits, then the composition $F \circ G \colon C \to E$ also preserves all colimits.

CategoryTheory.Limits.compPreservesLimit theorem

[PreservesLimit K F] [PreservesLimit (K ⋙ F) G] : PreservesLimit K (F ⋙ G)

Full source

@[deprecated "use comp_preservesLimit" (since := "2024-11-19")]
lemma compPreservesLimit [PreservesLimit K F] [PreservesLimit (K ⋙ F) G] :
    PreservesLimit K (F ⋙ G) := inferInstance

Composition of Limit-Preserving Functors Preserves Limits

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves limits of a diagram $K \colon J \to C$ and $G$ preserves limits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ preserves limits of $K$.

CategoryTheory.Limits.compPreservesLimitsOfShape theorem

[PreservesLimitsOfShape J F] [PreservesLimitsOfShape J G] : PreservesLimitsOfShape J (F ⋙ G)

Full source

@[deprecated "use comp_preservesLimitsOfShape" (since := "2024-11-19")]
lemma compPreservesLimitsOfShape [PreservesLimitsOfShape J F] [PreservesLimitsOfShape J G] :
    PreservesLimitsOfShape J (F ⋙ G) :=
  comp_preservesLimitsOfShape _ _

Composition of Functors Preserves Limits of a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If $F$ preserves all limits of shape $J$ and $G$ preserves all limits of shape $J$, then the composition $F \circ G \colon C \to E$ preserves all limits of shape $J$.

CategoryTheory.Limits.compPreservesLimits theorem

[PreservesLimitsOfSize.{w', w} F] [PreservesLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} (F ⋙ G)

Full source

@[deprecated "use comp_preservesLimits" (since := "2024-11-19")]
lemma compPreservesLimits [PreservesLimitsOfSize.{w', w} F] [PreservesLimitsOfSize.{w', w} G] :
    PreservesLimitsOfSize.{w', w} (F ⋙ G) :=
  comp_preservesLimits _ _

Composition of Limit-Preserving Functors Preserves Limits of a Given Size

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if $F$ preserves all limits of a given size and $G$ preserves all limits of the same size, then their composition $F \circ G \colon C \to E$ also preserves all limits of that size.

CategoryTheory.Limits.compPreservesColimit theorem

[PreservesColimit K F] [PreservesColimit (K ⋙ F) G] : PreservesColimit K (F ⋙ G)

Full source

@[deprecated "use comp_preservesColimit" (since := "2024-11-19")]
lemma compPreservesColimit [PreservesColimit K F] [PreservesColimit (K ⋙ F) G] :
    PreservesColimit K (F ⋙ G) := inferInstance

Preservation of Colimits under Functor Composition

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ preserves colimits of a diagram $K \colon J \to C$ and $G$ preserves colimits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ preserves colimits of $K$.

CategoryTheory.Limits.compPreservesColimitsOfShape theorem

[PreservesColimitsOfShape J F] [PreservesColimitsOfShape J G] : PreservesColimitsOfShape J (F ⋙ G)

Full source

@[deprecated "use comp_preservesColimitsOfShape" (since := "2024-11-19")]
lemma compPreservesColimitsOfShape [PreservesColimitsOfShape J F] [PreservesColimitsOfShape J G] :
    PreservesColimitsOfShape J (F ⋙ G) :=
  comp_preservesColimitsOfShape _ _

Composition of Functors Preserves Colimits of a Given Shape

Informal description

Given functors $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$ between categories, if $F$ preserves all colimits of shape $J$ and $G$ preserves all colimits of shape $J$, then the composition $F \circ G \colon \mathcal{C} \to \mathcal{E}$ also preserves all colimits of shape $J$.

CategoryTheory.Limits.compPreservesColimits theorem

[PreservesColimitsOfSize.{w', w} F] [PreservesColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} (F ⋙ G)

Full source

@[deprecated "use comp_preservesColimits" (since := "2024-11-19")]
lemma compPreservesColimits [PreservesColimitsOfSize.{w', w} F]
    [PreservesColimitsOfSize.{w', w} G] :
    PreservesColimitsOfSize.{w', w} (F ⋙ G) :=
  comp_preservesColimits _ _

Composition of Colimit-Preserving Functors Preserves Colimits

Informal description

Given functors $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$ between categories, if $F$ preserves all colimits of a given size and $G$ preserves all colimits of the same size, then their composition $F \circ G \colon \mathcal{C} \to \mathcal{E}$ also preserves all colimits of that size.

CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone theorem

{F : C ⥤ D} {t : Cone K} (h : IsLimit t) (hF : IsLimit (F.mapCone t)) : PreservesLimit K F

Full source

/-- If F preserves one limit cone for the diagram K,
  then it preserves any limit cone for K. -/
lemma preservesLimit_of_preserves_limit_cone {F : C ⥤ D} {t : Cone K} (h : IsLimit t)
    (hF : IsLimit (F.mapCone t)) : PreservesLimit K F where
  preserves h' := ⟨IsLimit.ofIsoLimit hF (Functor.mapIso _ (IsLimit.uniqueUpToIso h h'))⟩

Preservation of Limits via a Single Limit Cone

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and let $K \colon J \to \mathcal{C}$ be a diagram. If there exists a limit cone $t$ over $K$ such that $F$ maps $t$ to a limit cone over $F \circ K$ in $\mathcal{D}$, then $F$ preserves all limit cones over $K$. That is, $F$ sends every limit cone over $K$ to a limit cone in $\mathcal{D}$.

CategoryTheory.Limits.preservesLimitOfPreservesLimitCone theorem

{F : C ⥤ D} {t : Cone K} (h : IsLimit t) (hF : IsLimit (F.mapCone t)) : PreservesLimit K F

Full source

@[deprecated "use preservesLimit_of_preserves_limit_cone" (since := "2024-11-19")]
lemma preservesLimitOfPreservesLimitCone {F : C ⥤ D} {t : Cone K} (h : IsLimit t)
    (hF : IsLimit (F.mapCone t)) : PreservesLimit K F :=
preservesLimit_of_preserves_limit_cone h hF

Preservation of Limits via a Single Limit Cone

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and let $K \colon J \to \mathcal{C}$ be a diagram. If $t$ is a limit cone over $K$ and $F$ maps $t$ to a limit cone over $F \circ K$ in $\mathcal{D}$, then $F$ preserves all limits of $K$. That is, $F$ sends every limit cone over $K$ to a limit cone in $\mathcal{D}$.

CategoryTheory.Limits.preservesLimit_of_iso_diagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesLimit K₁ F] : PreservesLimit K₂ F

Full source

/-- Transfer preservation of limits along a natural isomorphism in the diagram. -/
lemma preservesLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesLimit K₁ F] : PreservesLimit K₂ F where
  preserves {c} t := ⟨by
    apply IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _ _
    have := (IsLimit.postcomposeInvEquiv h c).symm t
    apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
    exact Cones.ext (Iso.refl _)⟩

Preservation of Limits under Natural Isomorphism of Diagrams

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Suppose $K_1, K_2 \colon J \to \mathcal{C}$ are diagrams in $\mathcal{C}$ that are naturally isomorphic via $h \colon K_1 \cong K_2$. If $F$ preserves limits of $K_1$, then $F$ also preserves limits of $K_2$. In other words, if $F$ maps every limit cone over $K_1$ to a limit cone in $\mathcal{D}$, then $F$ also maps every limit cone over $K_2$ to a limit cone in $\mathcal{D}$.

CategoryTheory.Limits.preservesLimitOfIsoDiagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesLimit K₁ F] : PreservesLimit K₂ F

Full source

@[deprecated "use preservesLimit_of_iso_diagram" (since := "2024-11-19")]
lemma preservesLimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesLimit K₁ F] : PreservesLimit K₂ F :=
  preservesLimit_of_iso_diagram F h

Preservation of Limits under Natural Isomorphism of Diagrams

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Suppose $K_1, K_2 \colon J \to \mathcal{C}$ are naturally isomorphic diagrams via $h \colon K_1 \cong K_2$. If $F$ preserves limits of $K_1$, then $F$ also preserves limits of $K_2$. In other words, if $F$ maps every limit cone over $K_1$ to a limit cone in $\mathcal{D}$, then $F$ also maps every limit cone over $K_2$ to a limit cone in $\mathcal{D}$.

CategoryTheory.Limits.preservesLimit_of_natIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesLimit K F] : PreservesLimit K G

Full source

/-- Transfer preservation of a limit along a natural isomorphism in the functor. -/
lemma preservesLimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesLimit K F] :
    PreservesLimit K G where
  preserves t := ⟨IsLimit.mapConeEquiv h (isLimitOfPreserves F t)⟩

Preservation of Limits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon J \to \mathcal{C}$ be a diagram. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ that are naturally isomorphic via $h \colon F \cong G$, if $F$ preserves limits of $K$, then $G$ also preserves limits of $K$. In other words, if $F$ maps every limit cone over $K$ to a limit cone in $\mathcal{D}$, then $G$ does the same.

CategoryTheory.Limits.preservesLimitOfNatIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesLimit K F] : PreservesLimit K G

Full source

@[deprecated "use preservesLimit_of_natIso" (since := "2024-11-19")]
lemma preservesLimitOfNatIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesLimit K F] :
    PreservesLimit K G :=
  preservesLimit_of_natIso K h

Preservation of Limits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon J \to \mathcal{C}$ be a diagram. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ that are naturally isomorphic via $h \colon F \cong G$, if $F$ preserves limits of $K$, then $G$ also preserves limits of $K$. In other words, if $F$ maps every limit cone over $K$ to a limit cone in $\mathcal{D}$, then $G$ does the same.

CategoryTheory.Limits.preservesLimitsOfShape_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J G

Full source

/-- Transfer preservation of limits of shape along a natural isomorphism in the functor. -/
lemma preservesLimitsOfShape_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfShape J F] :
    PreservesLimitsOfShape J G where
  preservesLimit {K} := preservesLimit_of_natIso K h

Preservation of Limits of Shape under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ that are naturally isomorphic via $h \colon F \cong G$, if $F$ preserves all limits of shape $J$, then $G$ also preserves all limits of shape $J$. In other words, if $F$ maps every limit cone over any diagram $K \colon J \to \mathcal{C}$ to a limit cone in $\mathcal{D}$, then $G$ does the same.

CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J G

Full source

@[deprecated "use preservesLimitsOfShape_of_natIso" (since := "2024-11-19")]
lemma preservesLimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfShape J F] :
    PreservesLimitsOfShape J G :=
  preservesLimitsOfShape_of_natIso h

Preservation of Limits of Shape under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ that are naturally isomorphic via $h \colon F \cong G$, if $F$ preserves all limits of shape $J$, then $G$ also preserves all limits of shape $J$. In other words, if $F$ maps every limit cone over any diagram $K \colon J \to \mathcal{C}$ to a limit cone in $\mathcal{D}$, then $G$ does the same.

CategoryTheory.Limits.preservesLimits_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfSize.{w, w'} F] : PreservesLimitsOfSize.{w, w'} G

Full source

/-- Transfer preservation of limits along a natural isomorphism in the functor. -/
lemma preservesLimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfSize.{w, w'} F] :
    PreservesLimitsOfSize.{w, w'} G where
  preservesLimitsOfShape := preservesLimitsOfShape_of_natIso h

Preservation of Limits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors that are naturally isomorphic via $h \colon F \cong G$. If $F$ preserves all limits of a given size, then $G$ also preserves all limits of the same size. In other words, if $F$ maps every limit cone over any diagram $K \colon J \to \mathcal{C}$ (where $J$ is a category of the specified size) to a limit cone in $\mathcal{D}$, then $G$ does the same.

CategoryTheory.Limits.preservesLimitsOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfSize.{w, w'} F] : PreservesLimitsOfSize.{w, w'} G

Full source

@[deprecated "use preservesLimits_of_natIso" (since := "2024-11-19")]
lemma preservesLimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfSize.{w, w'} F] :
    PreservesLimitsOfSize.{w, w'} G :=
  preservesLimits_of_natIso h

Preservation of Limits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors that are naturally isomorphic via $h \colon F \cong G$. If $F$ preserves all limits of a given size, then $G$ also preserves all limits of the same size.

CategoryTheory.Limits.preservesLimitsOfShape_of_equiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F

Full source

/-- Transfer preservation of limits along an equivalence in the shape. -/
lemma preservesLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F where
  preservesLimit {K} :=
    { preserves := fun {c} t => ⟨by
        let equ := e.invFunIdAssoc (K ⋙ F)
        have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
        apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
        refine Cones.ext (Iso.refl _) fun j => ?_
        dsimp
        simp [equ, ← Functor.map_comp]⟩ }

Preservation of Limits Under Equivalence of Diagram Shapes

Informal description

Let $J$ and $J'$ be small categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that preserves limits of shape $J$. Then $F$ also preserves limits of shape $J'$.

CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F

Full source

@[deprecated "use preservesLimitsOfShape_of_equiv" (since := "2024-11-19")]
lemma preservesLimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F :=
  preservesLimitsOfShape_of_equiv e F

Preservation of Limits Under Equivalence of Diagram Shapes

Informal description

Let $J$ and $J'$ be small categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that preserves limits of shape $J$. Then $F$ also preserves limits of shape $J'$.

CategoryTheory.Limits.preservesLimitsOfSize_of_univLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F

Full source

/-- A functor preserving larger limits also preserves smaller limits. -/
lemma preservesLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F where
  preservesLimitsOfShape {J} := preservesLimitsOfShape_of_equiv
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

Preservation of Smaller Limits Under Universe Level Constraints

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and suppose that: 1. Universe level $w$ is less than or equal to $w'$ (denoted $\text{UnivLE}\{w, w'\}$), 2. Universe level $w_2$ is less than or equal to $w_2'$ (denoted $\text{UnivLE}\{w_2, w_2'\}$), and 3. $F$ preserves limits of size $(w', w_2')$. Then $F$ also preserves limits of size $(w, w_2)$.

CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F

Full source

@[deprecated "use preservesLimitsOfSize_of_univLE" (since := "2024-11-19")]
lemma preservesLimitsOfSizeOfUnivLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F :=
  preservesLimitsOfSize_of_univLE.{w', w₂'} F

Preservation of Smaller Limits Under Universe Level Constraints

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. Suppose that: 1. Universe level $w$ is less than or equal to $w'$, 2. Universe level $w_2$ is less than or equal to $w_2'$, and 3. $F$ preserves limits of size $(w', w_2')$. Then $F$ also preserves limits of size $(w, w_2)$.

CategoryTheory.Limits.preservesLimitsOfSize_shrink theorem

(F : C ⥤ D) [PreservesLimitsOfSize.{max w w₂, max w' w₂'} F] : PreservesLimitsOfSize.{w, w'} F

Full source

/-- `PreservesLimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesLimitsOfSize.{w w'} F`
from some other `PreservesLimitsOfSize F`.
-/
lemma preservesLimitsOfSize_shrink (F : C ⥤ D) [PreservesLimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesLimitsOfSize.{w, w'} F := preservesLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Preservation of Smaller Limits from Preservation of Larger Limits

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves limits of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also preserves limits of size $(w, w')$.

CategoryTheory.Limits.PreservesLimitsOfSizeShrink theorem

(F : C ⥤ D) [PreservesLimitsOfSize.{max w w₂, max w' w₂'} F] : PreservesLimitsOfSize.{w, w'} F

Full source

@[deprecated "use preservesLimitsOfSize_shrink" (since := "2024-11-19")]
lemma PreservesLimitsOfSizeShrink (F : C ⥤ D) [PreservesLimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesLimitsOfSize.{w, w'} F :=
  preservesLimitsOfSize_shrink F

Preservation of Smaller Limits from Preservation of Larger Limits

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves limits of diagrams of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also preserves limits of diagrams of size $(w, w')$.

CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits theorem

(F : C ⥤ D) [PreservesLimitsOfSize.{v₃, u₃} F] : PreservesLimitsOfSize.{0, 0} F

Full source

/-- Preserving limits at any universe level implies preserving limits in universe `0`. -/
lemma preservesSmallestLimits_of_preservesLimits (F : C ⥤ D) [PreservesLimitsOfSize.{v₃, u₃} F] :
    PreservesLimitsOfSize.{0, 0} F :=
  preservesLimitsOfSize_shrink F

Preservation of Small Limits from Preservation of All Limits

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves limits of all sizes (i.e., for any universe levels $v_3$ and $u_3$), then $F$ also preserves limits of diagrams indexed by small categories (i.e., categories in universe level $0$).

CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits theorem

(F : C ⥤ D) [PreservesLimitsOfSize.{v₃, u₃} F] : PreservesLimitsOfSize.{0, 0} F

Full source

@[deprecated "use preservesSmallestLimits_of_preservesLimits" (since := "2024-11-19")]
lemma preservesSmallestLimitsOfPreservesLimits (F : C ⥤ D) [PreservesLimitsOfSize.{v₃, u₃} F] :
    PreservesLimitsOfSize.{0, 0} F :=
  preservesSmallestLimits_of_preservesLimits F

Preservation of Small Limits from Preservation of All Limits

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves limits of all sizes (i.e., for any universe levels $v_3$ and $u_3$), then $F$ also preserves limits of diagrams indexed by small categories (i.e., categories in universe level $0$).

CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone theorem

{F : C ⥤ D} {t : Cocone K} (h : IsColimit t) (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F

Full source

/-- If F preserves one colimit cocone for the diagram K,
  then it preserves any colimit cocone for K. -/
lemma preservesColimit_of_preserves_colimit_cocone {F : C ⥤ D} {t : Cocone K} (h : IsColimit t)
    (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F :=
  ⟨fun h' => ⟨IsColimit.ofIsoColimit hF (Functor.mapIso _ (IsColimit.uniqueUpToIso h h'))⟩⟩

Functor Preserves Colimit if it Preserves a Colimit Cocone

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor, and let $K \colon \mathcal{J} \to \mathcal{C}$ be a diagram. If $t$ is a colimit cocone for $K$ in $\mathcal{C}$ and $F$ maps $t$ to a colimit cocone in $\mathcal{D}$, then $F$ preserves colimits of the diagram $K$.

CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone theorem

{F : C ⥤ D} {t : Cocone K} (h : IsColimit t) (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F

Full source

@[deprecated "use preservesColimit_of_preserves_colimit_cocone" (since := "2024-11-19")]
lemma preservesColimitOfPreservesColimitCocone {F : C ⥤ D} {t : Cocone K} (h : IsColimit t)
    (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F :=
preservesColimit_of_preserves_colimit_cocone h hF

Functor Preserves Colimit if it Preserves a Colimit Cocone

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor and $K \colon \mathcal{J} \to \mathcal{C}$ a diagram. If $t$ is a colimit cocone for $K$ in $\mathcal{C}$ and $F$ maps $t$ to a colimit cocone in $\mathcal{D}$, then $F$ preserves colimits of the diagram $K$.

CategoryTheory.Limits.preservesColimit_of_iso_diagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesColimit K₁ F] : PreservesColimit K₂ F

Full source

/-- Transfer preservation of colimits along a natural isomorphism in the shape. -/
lemma preservesColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesColimit K₁ F] :
    PreservesColimit K₂ F where
  preserves {c} t := ⟨by
    apply IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _ _
    have := (IsColimit.precomposeHomEquiv h c).symm t
    apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
    exact Cocones.ext (Iso.refl _)⟩

Preservation of Colimits under Natural Isomorphism of Diagrams

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two diagrams $K_1, K_2 \colon \mathcal{J} \to \mathcal{C}$ that are naturally isomorphic via $h \colon K_1 \cong K_2$, if $F$ preserves colimits of $K_1$, then $F$ also preserves colimits of $K_2$.

CategoryTheory.Limits.preservesColimitOfIsoDiagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesColimit K₁ F] : PreservesColimit K₂ F

Full source

@[deprecated "use preservesColimit_of_iso_diagram" (since := "2024-11-19")]
lemma preservesColimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesColimit K₁ F] :
    PreservesColimit K₂ F :=
  preservesColimit_of_iso_diagram F h

Preservation of Colimits under Diagram Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two naturally isomorphic diagrams $K_1, K_2 \colon \mathcal{J} \to \mathcal{C}$ via an isomorphism $h \colon K_1 \cong K_2$, if $F$ preserves colimits of $K_1$, then $F$ also preserves colimits of $K_2$.

CategoryTheory.Limits.preservesColimit_of_natIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] : PreservesColimit K G

Full source

/-- Transfer preservation of a colimit along a natural isomorphism in the functor. -/
lemma preservesColimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] :
    PreservesColimit K G where
  preserves t := ⟨IsColimit.mapCoconeEquiv h (isColimitOfPreserves F t)⟩

Preservation of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon \mathcal{J} \to \mathcal{C}$ be a diagram. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ via an isomorphism $h \colon F \cong G$, if $F$ preserves colimits of $K$, then $G$ also preserves colimits of $K$.

CategoryTheory.Limits.preservesColimitOfNatIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] : PreservesColimit K G

Full source

@[deprecated preservesColimit_of_natIso (since := "2024-11-19")]
lemma preservesColimitOfNatIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] :
    PreservesColimit K G :=
  preservesColimit_of_natIso K h

Preservation of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon \mathcal{J} \to \mathcal{C}$ be a diagram. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ via an isomorphism $h \colon F \cong G$, if $F$ preserves colimits of $K$, then $G$ also preserves colimits of $K$.

CategoryTheory.Limits.preservesColimitsOfShape_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] : PreservesColimitsOfShape J G

Full source

/-- Transfer preservation of colimits of shape along a natural isomorphism in the functor. -/
lemma preservesColimitsOfShape_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] :
    PreservesColimitsOfShape J G where
  preservesColimit {K} := preservesColimit_of_natIso K h

Preservation of Colimits of Shape under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ via an isomorphism $h \colon F \cong G$, if $F$ preserves all colimits of shape $J$, then $G$ also preserves all colimits of shape $J$.

CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] : PreservesColimitsOfShape J G

Full source

@[deprecated "use preservesColimitsOfShape_of_natIso" (since := "2024-11-19")]
lemma preservesColimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] :
    PreservesColimitsOfShape J G :=
  preservesColimitsOfShape_of_natIso h

Preservation of Colimits of Shape under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ via an isomorphism $h \colon F \cong G$, if $F$ preserves all colimits of shape $J$, then $G$ also preserves all colimits of shape $J$.

CategoryTheory.Limits.preservesColimits_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfSize.{w, w'} F] : PreservesColimitsOfSize.{w, w'} G

Full source

/-- Transfer preservation of colimits along a natural isomorphism in the functor. -/
lemma preservesColimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfSize.{w, w'} F] :
    PreservesColimitsOfSize.{w, w'} G where
  preservesColimitsOfShape {_J} _𝒥₁ := preservesColimitsOfShape_of_natIso h

Preservation of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be naturally isomorphic functors via an isomorphism $h \colon F \cong G$. If $F$ preserves all colimits (of a given size), then $G$ also preserves all colimits (of the same size).

CategoryTheory.Limits.preservesColimitsOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfSize.{w, w'} F] : PreservesColimitsOfSize.{w, w'} G

Full source

@[deprecated "use preservesColimits_of_natIso" (since := "2024-11-19")]
lemma preservesColimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfSize.{w, w'} F] :
    PreservesColimitsOfSize.{w, w'} G :=
  preservesColimits_of_natIso h

Preservation of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be naturally isomorphic functors via an isomorphism $h \colon F \cong G$. If $F$ preserves all colimits (of a given size), then $G$ also preserves all colimits (of the same size).

CategoryTheory.Limits.preservesColimitsOfShape_of_equiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [PreservesColimitsOfShape J F] :
  PreservesColimitsOfShape J' F

Full source

/-- Transfer preservation of colimits along an equivalence in the shape. -/
lemma preservesColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesColimitsOfShape J F] : PreservesColimitsOfShape J' F where
  preservesColimit {K} :=
    { preserves := fun {c} t => ⟨by
        let equ := e.invFunIdAssoc (K ⋙ F)
        have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
        apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
        refine Cocones.ext (Iso.refl _) fun j => ?_
        dsimp
        simp [equ, ← Functor.map_comp]⟩ }

Preservation of colimits under equivalence of diagram shapes

Informal description

Let $J$ and $J'$ be small categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that preserves all colimits of shape $J$. Then $F$ also preserves all colimits of shape $J'$.

CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [PreservesColimitsOfShape J F] :
  PreservesColimitsOfShape J' F

Full source

@[deprecated "use preservesColimitsOfShape_of_equiv" (since := "2024-11-19")]
lemma preservesColimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesColimitsOfShape J F] : PreservesColimitsOfShape J' F :=
  preservesColimitsOfShape_of_equiv e F

Preservation of Colimits under Equivalence of Diagram Shapes

Informal description

Let $J$ and $J'$ be small categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that preserves all colimits of shape $J$. Then $F$ also preserves all colimits of shape $J'$.

CategoryTheory.Limits.preservesColimitsOfSize_of_univLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesColimitsOfSize.{w', w₂'} F] :
  PreservesColimitsOfSize.{w, w₂} F

Full source

/-- A functor preserving larger colimits also preserves smaller colimits. -/
lemma preservesColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [PreservesColimitsOfSize.{w', w₂'} F] : PreservesColimitsOfSize.{w, w₂} F where
  preservesColimitsOfShape {J} := preservesColimitsOfShape_of_equiv
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

Preservation of Colimits under Universe Level Constraints

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and suppose that: 1. The universe level $w$ is less than or equal to $w'$ (denoted by $\text{UnivLE}\{w, w'\}$), 2. The universe level $w_2$ is less than or equal to $w_2'$ (denoted by $\text{UnivLE}\{w_2, w_2'\}$), 3. $F$ preserves all colimits of size $(w', w_2')$. Then $F$ also preserves all colimits of size $(w, w_2)$.

CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesColimitsOfSize.{w', w₂'} F] :
  PreservesColimitsOfSize.{w, w₂} F

Full source

@[deprecated "use preservesColimitsOfSize_of_univLE" (since := "2024-11-19")]
lemma preservesColimitsOfSizeOfUnivLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [PreservesColimitsOfSize.{w', w₂'} F] : PreservesColimitsOfSize.{w, w₂} F :=
  preservesColimitsOfSize_of_univLE.{w', w₂'} F

Preservation of Colimits under Universe Level Constraints

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and suppose that: 1. The universe level $w$ is less than or equal to $w'$ (denoted by $w \leq w'$), 2. The universe level $w_2$ is less than or equal to $w_2'$ (denoted by $w_2 \leq w_2'$), 3. $F$ preserves all colimits of size $(w', w_2')$. Then $F$ also preserves all colimits of size $(w, w_2)$.

CategoryTheory.Limits.preservesColimitsOfSize_shrink theorem

(F : C ⥤ D) [PreservesColimitsOfSize.{max w w₂, max w' w₂'} F] : PreservesColimitsOfSize.{w, w'} F

Full source

/--
`PreservesColimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesColimitsOfSize.{w w'} F`
from some other `PreservesColimitsOfSize F`.
-/
lemma preservesColimitsOfSize_shrink (F : C ⥤ D)
    [PreservesColimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesColimitsOfSize.{w, w'} F := preservesColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Preservation of Colimits under Size Shrinkage

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves all colimits of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also preserves all colimits of size $(w, w')$.

CategoryTheory.Limits.PreservesColimitsOfSizeShrink theorem

(F : C ⥤ D) [PreservesColimitsOfSize.{max w w₂, max w' w₂'} F] : PreservesColimitsOfSize.{w, w'} F

Full source

@[deprecated "use preservesColimitsOfSize_shrink" (since := "2024-11-19")]
lemma PreservesColimitsOfSizeShrink (F : C ⥤ D)
    [PreservesColimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesColimitsOfSize.{w, w'} F :=
  preservesColimitsOfSize_shrink F

Preservation of Colimits under Size Reduction

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If $F$ preserves all colimits of diagrams of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also preserves all colimits of diagrams of size $(w, w')$.

CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits theorem

(F : C ⥤ D) [PreservesColimitsOfSize.{v₃, u₃} F] : PreservesColimitsOfSize.{0, 0} F

Full source

/-- Preserving colimits at any universe implies preserving colimits at universe `0`. -/
lemma preservesSmallestColimits_of_preservesColimits (F : C ⥤ D)
    [PreservesColimitsOfSize.{v₃, u₃} F] :
    PreservesColimitsOfSize.{0, 0} F :=
  preservesColimitsOfSize_shrink F

Preservation of Smallest Colimits from Preservation of Colimits

Informal description

If a functor $F \colon \mathcal{C} \to \mathcal{D}$ preserves all colimits of a certain size (specified by universe levels $v₃$ and $u₃$), then it also preserves all colimits of the smallest size (universe level $0$).

CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits theorem

(F : C ⥤ D) [PreservesColimitsOfSize.{v₃, u₃} F] : PreservesColimitsOfSize.{0, 0} F

Full source

@[deprecated "use preservesSmallestColimits_of_preservesColimits" (since := "2024-11-19")]
lemma preservesSmallestColimitsOfPreservesColimits (F : C ⥤ D)
    [PreservesColimitsOfSize.{v₃, u₃} F] :
    PreservesColimitsOfSize.{0, 0} F :=
  preservesSmallestColimits_of_preservesColimits F

Preservation of Smallest Colimits from Preservation of Colimits

Informal description

If a functor $F \colon \mathcal{C} \to \mathcal{D}$ preserves all colimits of a certain size (specified by universe levels $v₃$ and $u₃$), then it also preserves all colimits of the smallest size (universe level $0$).

CategoryTheory.Limits.ReflectsLimit structure

(K : J ⥤ C) (F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects limits for `K : J ⥤ C` if
whenever the image of a cone over `K` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
-/
class ReflectsLimit (K : J ⥤ C) (F : C ⥤ D) : Prop where
  reflects {c : Cone K} (hc : IsLimit (F.mapCone c)) : Nonempty (IsLimit c)

Reflection of limits by a functor

Informal description

A functor $F \colon C \to D$ reflects limits for a diagram $K \colon J \to C$ if whenever the image of a cone over $K$ under $F$ is a limit cone in $D$, the original cone was already a limit cone in $C$. Note that this definition does not require $D$ to have any limits a priori.

CategoryTheory.Limits.ReflectsColimit structure

(K : J ⥤ C) (F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects colimits for `K : J ⥤ C` if
whenever the image of a cocone over `K` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
-/
class ReflectsColimit (K : J ⥤ C) (F : C ⥤ D) : Prop where
  reflects {c : Cocone K} (hc : IsColimit (F.mapCocone c)) : Nonempty (IsColimit c)

Reflection of colimits by a functor

Informal description

A functor $F \colon C \to D$ reflects colimits for a diagram $K \colon J \to C$ if whenever the image of a cocone over $K$ under $F$ is a colimit cocone in $D$, the original cocone was already a colimit cocone in $C$. Note that this definition does not require $D$ to have any colimits a priori.

CategoryTheory.Limits.ReflectsLimitsOfShape structure

(J : Type w) [Category.{w'} J] (F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects limits of shape `J` if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
-/
class ReflectsLimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop where
  reflectsLimit : ∀ {K : J ⥤ C}, ReflectsLimit K F := by infer_instance

Reflection of limits of a given shape by a functor

Informal description

A functor $F \colon C \to D$ reflects limits of shape $J$ if for any diagram $K \colon J \to C$, whenever the image under $F$ of a cone over $K$ is a limit cone in $D$, the original cone was already a limit cone in $C$. This definition does not assume that $D$ has any limits of shape $J$.

CategoryTheory.Limits.ReflectsColimitsOfShape structure

(J : Type w) [Category.{w'} J] (F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects colimits of shape `J` if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
-/
class ReflectsColimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop where
  reflectsColimit : ∀ {K : J ⥤ C}, ReflectsColimit K F := by infer_instance

Reflection of colimits of a given shape

Informal description

A functor $F \colon C \to D$ reflects colimits of shape $J$ if whenever the image of a cocone over a diagram $K \colon J \to C$ under $F$ is a colimit cocone in $D$, the original cocone was already a colimit cocone in $C$. Note that this definition does not require $D$ to have any colimits a priori.

CategoryTheory.Limits.ReflectsLimitsOfSize structure

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects limits if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
-/
@[nolint checkUnivs, pp_with_univ]
class ReflectsLimitsOfSize (F : C ⥤ D) : Prop where
  reflectsLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], ReflectsLimitsOfShape J F := by
    infer_instance

Functor that reflects limits

Informal description

A functor $F : C \to D$ reflects limits if whenever the image of a cone over some diagram $K : J \to C$ under $F$ is a limit cone in $D$, the original cone was already a limit cone in $C$. Note that this definition does not require $D$ to have any limits a priori.

CategoryTheory.Limits.ReflectsLimits abbrev

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects (small) limits if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
-/
abbrev ReflectsLimits (F : C ⥤ D) :=
  ReflectsLimitsOfSize.{v₂, v₂} F

Reflection of Limits by a Functor

Informal description

A functor $F \colon C \to D$ reflects (small) limits if whenever the image of a cone over a diagram $K \colon J \to C$ under $F$ is a limit cone in $D$, the original cone was already a limit cone in $C$. Note that this definition does not require $D$ to have any limits a priori.

CategoryTheory.Limits.ReflectsColimitsOfSize structure

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects colimits if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
-/
@[nolint checkUnivs, pp_with_univ]
class ReflectsColimitsOfSize (F : C ⥤ D) : Prop where
  reflectsColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], ReflectsColimitsOfShape J F := by
    infer_instance

Reflection of colimits by a functor

Informal description

A functor $F \colon C \to D$ reflects colimits if whenever the image of a cocone under $F$ is a colimit cocone in $D$, the original cocone was already a colimit cocone in $C$. Note that this definition does not require $D$ to have any colimits a priori.

CategoryTheory.Limits.ReflectsColimits abbrev

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` reflects (small) colimits if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
-/
abbrev ReflectsColimits (F : C ⥤ D) :=
  ReflectsColimitsOfSize.{v₂, v₂} F

Reflection of Colimits by a Functor

Informal description

A functor $F \colon C \to D$ reflects (small) colimits if whenever the image of a cocone under $F$ is a colimit cocone in $D$, the original cocone was already a colimit cocone in $C$. Note that this definition does not require $D$ to have any colimits a priori.

CategoryTheory.Limits.isLimitOfReflects definition

(F : C ⥤ D) {c : Cone K} (t : IsLimit (F.mapCone c)) [ReflectsLimit K F] : IsLimit c

Full source

/-- A convenience function for `ReflectsLimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
-/
def isLimitOfReflects (F : C ⥤ D) {c : Cone K} (t : IsLimit (F.mapCone c))
    [ReflectsLimit K F] : IsLimit c :=
  (ReflectsLimit.reflects t).some

Limit cone reflection via a functor

Informal description

Given a functor $ F \colon C \to D $ that reflects limits for a diagram $ K \colon J \to C $, if the image $ F(c) $ of a cone $ c $ over $ K $ is a limit cone in $ D $, then $ c $ is a limit cone in $ C $.

CategoryTheory.Limits.isColimitOfReflects definition

(F : C ⥤ D) {c : Cocone K} (t : IsColimit (F.mapCocone c)) [ReflectsColimit K F] : IsColimit c

Full source

/--
A convenience function for `ReflectsColimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
-/
def isColimitOfReflects (F : C ⥤ D) {c : Cocone K} (t : IsColimit (F.mapCocone c))
    [ReflectsColimit K F] : IsColimit c :=
  (ReflectsColimit.reflects t).some

Reflection of colimit cocones by a functor

Informal description

Given a functor $ F \colon C \to D $, a cocone $ c $ over a diagram $ K \colon J \to C $, and a proof that the image $ F(c) $ is a colimit cocone in $ D $, if $ F $ reflects colimits of $ K $, then $ c $ is a colimit cocone in $ C $.

CategoryTheory.Limits.reflectsLimit_subsingleton instance

(K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsLimit K F)

Full source

instance reflectsLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsLimit K F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Reflection Property for a Functor

Informal description

For any functor $F \colon C \to D$ and diagram $K \colon J \to C$, the property that $F$ reflects limits of $K$ is unique when it exists. That is, there is at most one proof that $F$ reflects limits of $K$.

CategoryTheory.Limits.reflectsColimit_subsingleton instance

(K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsColimit K F)

Full source

instance
  reflectsColimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsColimit K F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Colimit Reflection Property for a Functor and Diagram

Informal description

For any functor $F \colon C \to D$ and diagram $K \colon J \to C$, the property that $F$ reflects colimits of $K$ is a subsingleton (i.e., there is at most one proof of this property).

CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) : Subsingleton (ReflectsLimitsOfShape J F)

Full source

instance reflectsLimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
    Subsingleton (ReflectsLimitsOfShape J F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Reflection Property for a Functor

Informal description

For any category $J$ and functor $F \colon C \to D$, the property that $F$ reflects limits of shape $J$ is a subsingleton. That is, there is at most one proof that $F$ reflects limits of shape $J$.

CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) : Subsingleton (ReflectsColimitsOfShape J F)

Full source

instance reflectsColimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
    Subsingleton (ReflectsColimitsOfShape J F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Colimit Reflection Property for a Given Shape

Informal description

For any category $J$ and functor $F \colon C \to D$, the property that $F$ reflects colimits of shape $J$ is a subsingleton (i.e., there is at most one proof of this property).

CategoryTheory.Limits.reflects_limits_subsingleton instance

(F : C ⥤ D) : Subsingleton (ReflectsLimitsOfSize.{w', w} F)

Full source

instance
  reflects_limits_subsingleton (F : C ⥤ D) : Subsingleton (ReflectsLimitsOfSize.{w', w} F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Limit Reflection Property for Functors

Informal description

For any functor $F \colon C \to D$, the property of reflecting limits (of any size) is a subsingleton. This means there is at most one way for $F$ to satisfy the condition that whenever $F$ maps a cone in $C$ to a limit cone in $D$, the original cone was already a limit cone in $C$.

CategoryTheory.Limits.reflects_colimits_subsingleton instance

(F : C ⥤ D) : Subsingleton (ReflectsColimitsOfSize.{w', w} F)

Full source

instance reflects_colimits_subsingleton (F : C ⥤ D) :
    Subsingleton (ReflectsColimitsOfSize.{w', w} F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

Uniqueness of Colimit Reflection Property for Functors

Informal description

For any functor $F \colon C \to D$, the property that $F$ reflects all colimits (of any size) is a subsingleton. This means there is at most one way for $F$ to satisfy the condition that it reflects colimits.

CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape instance

(K : J ⥤ C) (F : C ⥤ D) [ReflectsLimitsOfShape J F] : ReflectsLimit K F

Full source

instance (priority := 100) reflectsLimit_of_reflectsLimitsOfShape (K : J ⥤ C) (F : C ⥤ D)
    [ReflectsLimitsOfShape J F] : ReflectsLimit K F :=
  ReflectsLimitsOfShape.reflectsLimit

Reflection of Limits for a Given Shape Implies Reflection of Individual Limits

Informal description

For any functor $F \colon C \to D$ that reflects limits of shape $J$, and for any diagram $K \colon J \to C$, $F$ reflects the limit of $K$. This means that if $F$ maps a cone over $K$ to a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape instance

(K : J ⥤ C) (F : C ⥤ D) [ReflectsColimitsOfShape J F] : ReflectsColimit K F

Full source

instance (priority := 100) reflectsColimit_of_reflectsColimitsOfShape (K : J ⥤ C) (F : C ⥤ D)
    [ReflectsColimitsOfShape J F] : ReflectsColimit K F :=
  ReflectsColimitsOfShape.reflectsColimit

Reflection of Colimits for a Given Shape Implies Reflection of Individual Colimits

Informal description

For any functor $F \colon C \to D$ that reflects colimits of shape $J$, and for any diagram $K \colon J \to C$, $F$ reflects the colimit of $K$. This means that if $F$ maps a cocone over $K$ to a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) [ReflectsLimitsOfSize.{w', w} F] : ReflectsLimitsOfShape J F

Full source

instance (priority := 100) reflectsLimitsOfShape_of_reflectsLimits (J : Type w) [Category.{w'} J]
    (F : C ⥤ D) [ReflectsLimitsOfSize.{w', w} F] : ReflectsLimitsOfShape J F :=
  ReflectsLimitsOfSize.reflectsLimitsOfShape

Reflection of Limits of a Given Shape by a Limit-Reflecting Functor

Informal description

For any functor $F \colon C \to D$ that reflects limits of any size, and for any small category $J$, $F$ reflects limits of shape $J$. This means that if $F$ maps a cone over a diagram $K \colon J \to C$ to a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits instance

(J : Type w) [Category.{w'} J] (F : C ⥤ D) [ReflectsColimitsOfSize.{w', w} F] : ReflectsColimitsOfShape J F

Full source

instance (priority := 100) reflectsColimitsOfShape_of_reflectsColimits
    (J : Type w) [Category.{w'} J]
    (F : C ⥤ D) [ReflectsColimitsOfSize.{w', w} F] : ReflectsColimitsOfShape J F :=
  ReflectsColimitsOfSize.reflectsColimitsOfShape

Reflection of Colimits of a Given Shape by a Colimit-Reflecting Functor

Informal description

For any functor $F \colon C \to D$ that reflects colimits of any size, and for any small category $J$, $F$ reflects colimits of shape $J$. This means that if $F$ maps a cocone over a diagram $K \colon J \to C$ to a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.id_reflectsLimits instance

: ReflectsLimitsOfSize.{w, w'} (𝟭 C)

Full source

instance id_reflectsLimits : ReflectsLimitsOfSize.{w, w'} (𝟭 C) where
  reflectsLimitsOfShape {J} 𝒥 :=
    { reflectsLimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.lift ⟨s.pt, fun j => s.π.app j, fun _ _ f => s.π.naturality f⟩, by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j, by
            cases K; rcases c with ⟨_, _, _⟩; intro s m w; rcases s with ⟨_, _, _⟩;
              exact h.uniq _ m w⟩⟩ }

Identity Functor Reflects Limits

Informal description

The identity functor on any category $C$ reflects all limits. That is, if a cone over a diagram in $C$ is sent by the identity functor to a limit cone, then the original cone was already a limit cone.

CategoryTheory.Limits.idReflectsLimits theorem

: ReflectsLimitsOfSize.{w, w'} (𝟭 C)

Full source

@[deprecated "use id_reflectsLimits" (since := "2024-11-19")]
lemma idReflectsLimits : ReflectsLimitsOfSize.{w, w'} (𝟭 C) := id_reflectsLimits

Identity Functor Reflects All Limits

Informal description

The identity functor $𝟭 C$ on a category $C$ reflects all limits. That is, if a cone over a diagram in $C$ is sent by $𝟭 C$ to a limit cone in $C$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.id_reflectsColimits instance

: ReflectsColimitsOfSize.{w, w'} (𝟭 C)

Full source

instance id_reflectsColimits : ReflectsColimitsOfSize.{w, w'} (𝟭 C) where
  reflectsColimitsOfShape {J} 𝒥 :=
    { reflectsColimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.desc ⟨s.pt, fun j => s.ι.app j, fun _ _ f => s.ι.naturality f⟩, by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j, by
            cases K; rcases c with ⟨_, _, _⟩; intro s m w; rcases s with ⟨_, _, _⟩;
              exact h.uniq _ m w⟩⟩ }

Identity Functor Reflects Colimits

Informal description

The identity functor $𝟭 C$ on a category $C$ reflects all colimits. That is, if the image of a cocone under $𝟭 C$ is a colimit cocone, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.idReflectsColimits theorem

: ReflectsColimitsOfSize.{w, w'} (𝟭 C)

Full source

@[deprecated "use id_reflectsColimits" (since := "2024-11-19")]
lemma idReflectsColimits : ReflectsColimitsOfSize.{w, w'} (𝟭 C) := id_reflectsColimits

Identity Functor Reflects All Colimits

Informal description

The identity functor $𝟭_C \colon C \to C$ reflects all colimits. That is, for any cocone in $C$, if its image under $𝟭_C$ is a colimit cocone in $C$, then the original cocone was already a colimit cocone.

CategoryTheory.Limits.comp_reflectsLimit instance

[ReflectsLimit K F] [ReflectsLimit (K ⋙ F) G] : ReflectsLimit K (F ⋙ G)

Full source

instance comp_reflectsLimit [ReflectsLimit K F] [ReflectsLimit (K ⋙ F) G] :
    ReflectsLimit K (F ⋙ G) :=
  ⟨fun h => ReflectsLimit.reflects (isLimitOfReflects G h)⟩

Composition of Limit-Reflecting Functors Reflects Limits

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects limits for a diagram $K \colon J \to C$ and $G$ reflects limits for the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ reflects limits for $K$.

CategoryTheory.Limits.comp_reflectsLimitsOfShape instance

[ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] : ReflectsLimitsOfShape J (F ⋙ G)

Full source

instance comp_reflectsLimitsOfShape [ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] :
    ReflectsLimitsOfShape J (F ⋙ G) where

Composition of Functors Preserves Limit Reflection for a Given Shape

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects limits of shape $J$ and $G$ reflects limits of shape $J$, then the composition $F \circ G \colon C \to E$ also reflects limits of shape $J$.

CategoryTheory.Limits.comp_reflectsLimits instance

[ReflectsLimitsOfSize.{w', w} F] [ReflectsLimitsOfSize.{w', w} G] : ReflectsLimitsOfSize.{w', w} (F ⋙ G)

Full source

instance comp_reflectsLimits [ReflectsLimitsOfSize.{w', w} F] [ReflectsLimitsOfSize.{w', w} G] :
    ReflectsLimitsOfSize.{w', w} (F ⋙ G) where

Composition of Limit-Reflecting Functors Reflects Limits of Any Size

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if both $F$ and $G$ reflect limits of any size, then their composition $F \circ G \colon C \to E$ also reflects limits of any size.

CategoryTheory.Limits.comp_reflectsColimit instance

[ReflectsColimit K F] [ReflectsColimit (K ⋙ F) G] : ReflectsColimit K (F ⋙ G)

Full source

instance comp_reflectsColimit [ReflectsColimit K F] [ReflectsColimit (K ⋙ F) G] :
    ReflectsColimit K (F ⋙ G) :=
  ⟨fun h => ReflectsColimit.reflects (isColimitOfReflects G h)⟩

Composition of Functors Preserves Colimit Reflection

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects colimits of a diagram $K \colon J \to C$ and $G$ reflects colimits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ reflects colimits of $K$.

CategoryTheory.Limits.comp_reflectsColimitsOfShape instance

[ReflectsColimitsOfShape J F] [ReflectsColimitsOfShape J G] : ReflectsColimitsOfShape J (F ⋙ G)

Full source

instance comp_reflectsColimitsOfShape [ReflectsColimitsOfShape J F] [ReflectsColimitsOfShape J G] :
    ReflectsColimitsOfShape J (F ⋙ G) where

Composition of Functors Preserves Colimit Reflection for a Given Shape

Informal description

For any category $J$, if functors $F \colon C \to D$ and $G \colon D \to E$ both reflect colimits of shape $J$, then their composition $F \circ G \colon C \to E$ also reflects colimits of shape $J$.

CategoryTheory.Limits.comp_reflectsColimits instance

[ReflectsColimitsOfSize.{w', w} F] [ReflectsColimitsOfSize.{w', w} G] : ReflectsColimitsOfSize.{w', w} (F ⋙ G)

Full source

instance comp_reflectsColimits [ReflectsColimitsOfSize.{w', w} F]
    [ReflectsColimitsOfSize.{w', w} G] : ReflectsColimitsOfSize.{w', w} (F ⋙ G) where

Composition of Colimit-Reflecting Functors Reflects Colimits

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ that both reflect colimits of any size, their composition $F \circ G \colon C \to E$ also reflects colimits of any size. This means that if the image of a cocone under $F \circ G$ is a colimit cocone in $E$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.compReflectsLimit theorem

[ReflectsLimit K F] [ReflectsLimit (K ⋙ F) G] : ReflectsLimit K (F ⋙ G)

Full source

@[deprecated "use comp_reflectsLimit" (since := "2024-11-19")]
lemma compReflectsLimit [ReflectsLimit K F] [ReflectsLimit (K ⋙ F) G] :
    ReflectsLimit K (F ⋙ G) := inferInstance

Composition of Limit-Reflecting Functors Reflects Limits

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects limits for a diagram $K \colon J \to C$ and $G$ reflects limits for the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ reflects limits for $K$.

CategoryTheory.Limits.compReflectsLimitsOfShape theorem

[ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] : ReflectsLimitsOfShape J (F ⋙ G)

Full source

@[deprecated "use comp_reflectsLimitsOfShape " (since := "2024-11-19")]
lemma compReflectsLimitsOfShape [ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] :
    ReflectsLimitsOfShape J (F ⋙ G) := inferInstance

Composition of Limit-Reflecting Functors Reflects Limits of Shape $J$

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects limits of shape $J$ and $G$ reflects limits of shape $J$, then their composition $F \circ G \colon C \to E$ also reflects limits of shape $J$.

CategoryTheory.Limits.compReflectsLimits theorem

[ReflectsLimitsOfSize.{w', w} F] [ReflectsLimitsOfSize.{w', w} G] : ReflectsLimitsOfSize.{w', w} (F ⋙ G)

Full source

@[deprecated "use comp_reflectsLimits" (since := "2024-11-19")]
lemma compReflectsLimits [ReflectsLimitsOfSize.{w', w} F] [ReflectsLimitsOfSize.{w', w} G] :
    ReflectsLimitsOfSize.{w', w} (F ⋙ G) := inferInstance

Composition of Limit-Reflecting Functors Reflects Limits of Any Size

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if both $F$ and $G$ reflect limits of any size, then their composition $F \circ G \colon C \to E$ also reflects limits of any size.

CategoryTheory.Limits.compReflectsColimit theorem

[ReflectsColimit K F] [ReflectsColimit (K ⋙ F) G] : ReflectsColimit K (F ⋙ G)

Full source

@[deprecated "use comp_reflectsColimit" (since := "2024-11-19")]
lemma compReflectsColimit [ReflectsColimit K F] [ReflectsColimit (K ⋙ F) G] :
    ReflectsColimit K (F ⋙ G) := inferInstance

Composition of Functors Preserves Colimit Reflection

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to E$, if $F$ reflects colimits of a diagram $K \colon J \to C$ and $G$ reflects colimits of the composed diagram $K \circ F \colon J \to D$, then the composition $F \circ G \colon C \to E$ reflects colimits of $K$.

CategoryTheory.Limits.compReflectsColimitsOfShape theorem

[ReflectsColimitsOfShape J F] [ReflectsColimitsOfShape J G] : ReflectsColimitsOfShape J (F ⋙ G)

Full source

@[deprecated "use comp_reflectsColimitsOfShape " (since := "2024-11-19")]
lemma compReflectsColimitsOfShape [ReflectsColimitsOfShape J F] [ReflectsColimitsOfShape J G] :
    ReflectsColimitsOfShape J (F ⋙ G) := inferInstance

Composition of Functors Preserves Colimit Reflection for a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If both $F$ and $G$ reflect colimits of shape $J$, then their composition $F \circ G \colon C \to E$ also reflects colimits of shape $J$.

CategoryTheory.Limits.compReflectsColimits theorem

[ReflectsColimitsOfSize.{w', w} F] [ReflectsColimitsOfSize.{w', w} G] : ReflectsColimitsOfSize.{w', w} (F ⋙ G)

Full source

@[deprecated "use comp_reflectsColimits" (since := "2024-11-19")]
lemma compReflectsColimits [ReflectsColimitsOfSize.{w', w} F] [ReflectsColimitsOfSize.{w', w} G] :
    ReflectsColimitsOfSize.{w', w} (F ⋙ G) := inferInstance

Composition of Colimit-Reflecting Functors Reflects Colimits

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If both $F$ and $G$ reflect colimits of any size, then their composition $F \circ G \colon C \to E$ also reflects colimits of any size. This means that if the image of a cocone under $F \circ G$ is a colimit cocone in $E$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves theorem

[PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] : PreservesLimit K F

Full source

/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`,
then `F` preserves limits for `K`. -/
lemma preservesLimit_of_reflects_of_preserves [PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] :
    PreservesLimit K F :=
  ⟨fun h => ⟨by
    apply isLimitOfReflects G
    apply isLimitOfPreserves (F ⋙ G) h⟩⟩

Preservation of Limits via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $K \colon J \to C$ be a diagram. If the composition $F \circ G$ preserves limits for $K$ and $G$ reflects limits for $K \circ F$, then $F$ preserves limits for $K$.

CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves theorem

[PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] : PreservesLimit K F

Full source

@[deprecated "use preservesLimit_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesLimitOfReflectsOfPreserves [PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] :
    PreservesLimit K F :=
  preservesLimit_of_reflects_of_preserves F G

Preservation of Limits via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $K \colon J \to C$ be a diagram. If the composition $F \circ G$ preserves limits of $K$ and $G$ reflects limits of $K \circ F$, then $F$ preserves limits of $K$.

CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves theorem

[PreservesLimitsOfShape J (F ⋙ G)] [ReflectsLimitsOfShape J G] : PreservesLimitsOfShape J F

Full source

/--
If `F ⋙ G` preserves limits of shape `J` and `G` reflects limits of shape `J`, then `F` preserves
limits of shape `J`.
-/
lemma preservesLimitsOfShape_of_reflects_of_preserves [PreservesLimitsOfShape J (F ⋙ G)]
    [ReflectsLimitsOfShape J G] : PreservesLimitsOfShape J F where
  preservesLimit := preservesLimit_of_reflects_of_preserves F G

Preservation of Limits via Composition and Reflection for a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $J$ be a small category. If the composition $F \circ G$ preserves limits of shape $J$ and $G$ reflects limits of shape $J$, then $F$ preserves limits of shape $J$.

CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves theorem

[PreservesLimitsOfShape J (F ⋙ G)] [ReflectsLimitsOfShape J G] : PreservesLimitsOfShape J F

Full source

@[deprecated "use preservesLimitsOfShape_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesLimitsOfShapeOfReflectsOfPreserves [PreservesLimitsOfShape J (F ⋙ G)]
    [ReflectsLimitsOfShape J G] : PreservesLimitsOfShape J F :=
  preservesLimitsOfShape_of_reflects_of_preserves F G

Preservation of Limits via Composition and Reflection for a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $J$ be a small category. If the composition $F \circ G$ preserves limits of shape $J$ and $G$ reflects limits of shape $J$, then $F$ preserves limits of shape $J$.

CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves theorem

[PreservesLimitsOfSize.{w', w} (F ⋙ G)] [ReflectsLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} F

Full source

/-- If `F ⋙ G` preserves limits and `G` reflects limits, then `F` preserves limits. -/
lemma preservesLimits_of_reflects_of_preserves [PreservesLimitsOfSize.{w', w} (F ⋙ G)]
    [ReflectsLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} F where
  preservesLimitsOfShape := preservesLimitsOfShape_of_reflects_of_preserves F G

Preservation of Limits via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors. If the composition $F \circ G$ preserves limits of all sizes and $G$ reflects limits of all sizes, then $F$ preserves limits of all sizes.

CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves theorem

[PreservesLimitsOfSize.{w', w} (F ⋙ G)] [ReflectsLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} F

Full source

@[deprecated "use preservesLimits_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesLimitsOfReflectsOfPreserves [PreservesLimitsOfSize.{w', w} (F ⋙ G)]
    [ReflectsLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} F :=
  preservesLimits_of_reflects_of_preserves.{w', w} F G

Preservation of Limits via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors. If the composition $F \circ G$ preserves limits of all sizes and $G$ reflects limits of all sizes, then $F$ preserves limits of all sizes.

CategoryTheory.Limits.reflectsLimit_of_iso_diagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] : ReflectsLimit K₂ F

Full source

/-- Transfer reflection of limits along a natural isomorphism in the diagram. -/
lemma reflectsLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] :
    ReflectsLimit K₂ F where
  reflects {c} t := ⟨by
    apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
    apply ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _).symm t).ofIsoLimit _
    exact Cones.ext (Iso.refl _)⟩

Reflection of Limits under Diagram Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two diagrams $K_1, K_2 \colon J \to \mathcal{C}$ and a natural isomorphism $h \colon K_1 \cong K_2$, if $F$ reflects limits of $K_1$, then $F$ also reflects limits of $K_2$. Here, "$F$ reflects limits of $K_i$" means that for any cone $c$ over $K_i$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitOfIsoDiagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] : ReflectsLimit K₂ F

Full source

@[deprecated "use reflectsLimit_of_iso_diagram" (since := "2024-11-19")]
lemma reflectsLimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] :
    ReflectsLimit K₂ F :=
  reflectsLimit_of_iso_diagram F h

Reflection of Limits under Diagram Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two diagrams $K_1, K_2 \colon J \to \mathcal{C}$ and a natural isomorphism $h \colon K_1 \cong K_2$, if $F$ reflects limits of $K_1$, then $F$ also reflects limits of $K_2$. Here, "$F$ reflects limits of $K_i$" means that for any cone $c$ over $K_i$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimit_of_natIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimit K F] : ReflectsLimit K G

Full source

/-- Transfer reflection of a limit along a natural isomorphism in the functor. -/
lemma reflectsLimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimit K F] :
    ReflectsLimit K G where
  reflects t := ReflectsLimit.reflects (IsLimit.mapConeEquiv h.symm t)

Reflection of Limits under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon J \to \mathcal{C}$ be a diagram. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $h \colon F \cong G$, if $F$ reflects limits of $K$, then $G$ also reflects limits of $K$. Here, "$F$ reflects limits of $K$" means that for any cone $c$ over $K$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitOfNatIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimit K F] : ReflectsLimit K G

Full source

@[deprecated "use reflectsLimit_of_natIso" (since := "2024-11-19")]
lemma reflectsLimitOfNatIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimit K F] :
    ReflectsLimit K G :=
  reflectsLimit_of_natIso K h

Reflection of Limits under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon J \to \mathcal{C}$ be a diagram. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $h \colon F \cong G$, if $F$ reflects limits of $K$, then $G$ also reflects limits of $K$. Here, "$F$ reflects limits of $K$" means that for any cone $c$ over $K$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitsOfShape_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J G

Full source

/-- Transfer reflection of limits of shape along a natural isomorphism in the functor. -/
lemma reflectsLimitsOfShape_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfShape J F] :
    ReflectsLimitsOfShape J G where
  reflectsLimit {K} := reflectsLimit_of_natIso K h

Reflection of Limits of Shape under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $h \colon F \cong G$, if $F$ reflects limits of shape $J$, then $G$ also reflects limits of shape $J$. Here, "$F$ reflects limits of shape $J$" means that for any diagram $K \colon J \to \mathcal{C}$ and any cone $c$ over $K$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J G

Full source

@[deprecated "use reflectsLimitsOfShape_of_natIso" (since := "2024-11-19")]
lemma reflectsLimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfShape J F] :
    ReflectsLimitsOfShape J G :=
  reflectsLimitsOfShape_of_natIso h

Reflection of Limits of Shape under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $h \colon F \cong G$, if $F$ reflects limits of shape $J$, then $G$ also reflects limits of shape $J$. Here, "$F$ reflects limits of shape $J$" means that for any diagram $K \colon J \to \mathcal{C}$ and any cone $c$ over $K$, if $F(c)$ is a limit cone in $\mathcal{D}$, then $c$ is already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimits_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfSize.{w', w} F] : ReflectsLimitsOfSize.{w', w} G

Full source

/-- Transfer reflection of limits along a natural isomorphism in the functor. -/
lemma reflectsLimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfSize.{w', w} F] :
    ReflectsLimitsOfSize.{w', w} G where
  reflectsLimitsOfShape := reflectsLimitsOfShape_of_natIso h

Reflection of Limits under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $h \colon F \cong G$. If $F$ reflects limits of any size (i.e., for any diagram shape $J$, if $F$ maps a cone over $K \colon J \to \mathcal{C}$ to a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$), then $G$ also reflects limits of any size.

CategoryTheory.Limits.reflectsLimitsOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfSize.{w', w} F] : ReflectsLimitsOfSize.{w', w} G

Full source

@[deprecated "use reflectsLimits_of_natIso" (since := "2024-11-19")]
lemma reflectsLimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfSize.{w', w} F] :
    ReflectsLimitsOfSize.{w', w} G :=
  reflectsLimits_of_natIso h

Reflection of Limits under Naturally Isomorphic Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $h \colon F \cong G$. If $F$ reflects limits of any size (i.e., for any diagram shape $J$, if $F$ maps a cone over $K \colon J \to \mathcal{C}$ to a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$), then $G$ also reflects limits of any size.

CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F

Full source

/-- Transfer reflection of limits along an equivalence in the shape. -/
lemma reflectsLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F where
  reflectsLimit {K} :=
    { reflects := fun {c} t => ⟨by
        apply IsLimit.ofWhiskerEquivalence e
        apply isLimitOfReflects F
        apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
        exact IsLimit.whiskerEquivalence t _⟩ }

Reflection of Limits Along Equivalent Diagram Shapes

Informal description

Let $J$ and $J'$ be categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that reflects limits of shape $J$. Then $F$ also reflects limits of shape $J'$. In other words, if $F$ maps a cone over any diagram of shape $J$ to a limit cone in $D$ only when the original cone was a limit cone in $C$, then the same property holds for diagrams of shape $J'$.

CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F

Full source

@[deprecated "use reflectsLimitsOfShape_of_equiv" (since := "2024-11-19")]
lemma reflectsLimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F :=
  reflectsLimitsOfShape_of_equiv e F

Reflection of Limits Along Equivalent Diagram Shapes

Informal description

Let $J$ and $J'$ be categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that reflects limits of shape $J$. Then $F$ also reflects limits of shape $J'$. In other words, if $F$ maps a cone over any diagram of shape $J$ to a limit cone in $D$ only when the original cone was a limit cone in $C$, then the same property holds for diagrams of shape $J'$.

CategoryTheory.Limits.reflectsLimitsOfSize_of_univLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F

Full source

/-- A functor reflecting larger limits also reflects smaller limits. -/
lemma reflectsLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F where
  reflectsLimitsOfShape {J} := reflectsLimitsOfShape_of_equiv
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

Reflection of Limits Under Universe Level Constraints

Informal description

Let $F \colon C \to D$ be a functor between categories, and suppose that universe levels satisfy $w \leq w'$ and $w_2 \leq w_2'$. If $F$ reflects limits of size $(w', w_2')$, then $F$ also reflects limits of size $(w, w_2)$.

CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F

Full source

@[deprecated "use reflectsLimitsOfSize_of_univLE" (since := "2024-11-19")]
lemma reflectsLimitsOfSizeOfUnivLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F :=
  reflectsLimitsOfSize_of_univLE.{w'} F

Reflection of Limits Under Universe Inequality

Informal description

Let $F \colon C \to D$ be a functor between categories, and suppose that the universe levels satisfy $w \leq w'$ and $w_2 \leq w_2'$. If $F$ reflects limits of size $(w', w_2')$, then $F$ also reflects limits of size $(w, w_2)$.

CategoryTheory.Limits.reflectsLimitsOfSize_shrink theorem

(F : C ⥤ D) [ReflectsLimitsOfSize.{max w w₂, max w' w₂'} F] : ReflectsLimitsOfSize.{w, w'} F

Full source

/-- `reflectsLimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsLimitsOfSize.{w w'} F`
from some other `reflectsLimitsOfSize F`.
-/
lemma reflectsLimitsOfSize_shrink (F : C ⥤ D) [ReflectsLimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsLimitsOfSize.{w, w'} F := reflectsLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Reflection of Limits Under Size Shrinkage

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects limits of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also reflects limits of size $(w, w')$.

CategoryTheory.Limits.reflectsLimitsOfSizeShrink theorem

(F : C ⥤ D) [ReflectsLimitsOfSize.{max w w₂, max w' w₂'} F] : ReflectsLimitsOfSize.{w, w'} F

Full source

@[deprecated "use reflectsLimitsOfSize_shrink" (since := "2024-11-19")]
lemma reflectsLimitsOfSizeShrink (F : C ⥤ D) [ReflectsLimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsLimitsOfSize.{w, w'} F :=
  reflectsLimitsOfSize_shrink F

Reflection of Limits Under Size Reduction

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects limits of diagrams of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also reflects limits of diagrams of size $(w, w')$.

CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits theorem

(F : C ⥤ D) [ReflectsLimitsOfSize.{v₃, u₃} F] : ReflectsLimitsOfSize.{0, 0} F

Full source

/-- Reflecting limits at any universe implies reflecting limits at universe `0`. -/
lemma reflectsSmallestLimits_of_reflectsLimits (F : C ⥤ D) [ReflectsLimitsOfSize.{v₃, u₃} F] :
    ReflectsLimitsOfSize.{0, 0} F :=
  reflectsLimitsOfSize_shrink F

Reflection of smallest limits by a limit-reflecting functor

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects limits of any size, then $F$ also reflects limits of the smallest size (i.e., limits indexed by finite categories).

CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits theorem

(F : C ⥤ D) [ReflectsLimitsOfSize.{v₃, u₃} F] : ReflectsLimitsOfSize.{0, 0} F

Full source

@[deprecated "use reflectsSmallestLimits_of_reflectsLimits" (since := "2024-11-19")]
lemma reflectsSmallestLimitsOfReflectsLimits (F : C ⥤ D) [ReflectsLimitsOfSize.{v₃, u₃} F] :
    ReflectsLimitsOfSize.{0, 0} F :=
  reflectsSmallestLimits_of_reflectsLimits F

Reflection of Finite Limits by a Limit-Reflecting Functor

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects limits of any size (i.e., for diagrams of any shape), then $F$ also reflects limits of the smallest size (i.e., limits indexed by finite categories).

CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms theorem

(F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasLimit F] [PreservesLimit F G] : ReflectsLimit F G

Full source

/-- If the limit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the limit of `F`.
-/ -- Porting note: previous behavior of apply pushed instance holes into hypotheses, this errors
lemma reflectsLimit_of_reflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms]
    [HasLimit F] [PreservesLimit F G] : ReflectsLimit F G where
  reflects {c} t := by
    suffices IsIso (IsLimit.lift (limit.isLimit F) c) from ⟨by
      apply IsLimit.ofPointIso (limit.isLimit F)⟩
    change IsIso ((Cones.forget _).map ((limit.isLimit F).liftConeMorphism c))
    suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by
      apply (Cones.forget F).map_isIso _
    suffices IsIso (Prefunctor.map (Cones.functoriality F G).toPrefunctor
      (IsLimit.liftConeMorphism (limit.isLimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cones.functoriality F G)
    exact t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _

Reflection of limits by a functor that reflects isomorphisms

Informal description

Let $F \colon J \to C$ be a functor and $G \colon C \to D$ a functor that reflects isomorphisms. If the limit of $F$ exists in $C$ and $G$ preserves this limit, then $G$ reflects the limit of $F$. That is, if the image of a cone over $F$ under $G$ is a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms theorem

(F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasLimit F] [PreservesLimit F G] : ReflectsLimit F G

Full source

@[deprecated "use reflectsLimit_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsLimitOfReflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms]
    [HasLimit F] [PreservesLimit F G] : ReflectsLimit F G :=
  reflectsLimit_of_reflectsIsomorphisms F G

Reflection of Limits by a Functor that Reflects Isomorphisms

Informal description

Let $F \colon J \to C$ be a functor and $G \colon C \to D$ a functor that reflects isomorphisms. If the limit of $F$ exists in $C$ and $G$ preserves this limit, then $G$ reflects the limit of $F$. That is, if the image of a cone over $F$ under $G$ is a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms theorem

{G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfShape J C] [PreservesLimitsOfShape J G] : ReflectsLimitsOfShape J G

Full source

/-- If `C` has limits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects limits of shape `J`.
-/
lemma reflectsLimitsOfShape_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasLimitsOfShape J C] [PreservesLimitsOfShape J G] : ReflectsLimitsOfShape J G where
  reflectsLimit {F} := reflectsLimit_of_reflectsIsomorphisms F G

Reflection of Limits by Isomorphism-Reflecting Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor that reflects isomorphisms. If $\mathcal{C}$ has limits of shape $J$ and $G$ preserves them, then $G$ reflects limits of shape $J$. That is, for any diagram $F \colon J \to \mathcal{C}$, if the image under $G$ of a cone over $F$ is a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms theorem

{G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfShape J C] [PreservesLimitsOfShape J G] : ReflectsLimitsOfShape J G

Full source

@[deprecated "use reflectsLimitsOfShape_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsLimitsOfShapeOfReflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasLimitsOfShape J C] [PreservesLimitsOfShape J G] : ReflectsLimitsOfShape J G :=
  reflectsLimitsOfShape_of_reflectsIsomorphisms

Reflection of Limits of Shape by Isomorphism-Reflecting Functors

Informal description

Let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories that reflects isomorphisms. If $\mathcal{C}$ has all limits of shape $J$ and $G$ preserves them, then $G$ reflects limits of shape $J$. That is, for any diagram $F \colon J \to \mathcal{C}$, if the image under $G$ of a cone over $F$ is a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfSize.{w', w} C] [PreservesLimitsOfSize.{w', w} G] :
  ReflectsLimitsOfSize.{w', w} G

Full source

/-- If `C` has limits and `G` preserves limits, then if `G` reflects isomorphisms then it reflects
limits.
-/
lemma reflectsLimits_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasLimitsOfSize.{w', w} C] [PreservesLimitsOfSize.{w', w} G] :
    ReflectsLimitsOfSize.{w', w} G where
  reflectsLimitsOfShape := reflectsLimitsOfShape_of_reflectsIsomorphisms

Reflection of Limits by Isomorphism-Reflecting Functors with Preserved Limits

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor that reflects isomorphisms. If $\mathcal{C}$ has all limits of a given size and $G$ preserves them, then $G$ reflects all limits of that size. That is, for any diagram $K \colon J \to \mathcal{C}$ where $J$ is a small category of the given size, if the image under $G$ of a cone over $K$ is a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfSize.{w', w} C] [PreservesLimitsOfSize.{w', w} G] :
  ReflectsLimitsOfSize.{w', w} G

Full source

@[deprecated "use reflectsLimits_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsLimitsOfReflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasLimitsOfSize.{w', w} C] [PreservesLimitsOfSize.{w', w} G] :
    ReflectsLimitsOfSize.{w', w} G :=
  reflectsLimits_of_reflectsIsomorphisms

Reflection of Limits by Isomorphism-Reflecting Functors with Preserved Limits

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor that reflects isomorphisms. If $\mathcal{C}$ has all limits of a given size and $G$ preserves them, then $G$ reflects all limits of that size. That is, for any diagram $K \colon J \to \mathcal{C}$ where $J$ is a small category of the given size, if the image under $G$ of a cone over $K$ is a limit cone in $\mathcal{D}$, then the original cone was already a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves theorem

[PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] : PreservesColimit K F

Full source

/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
then `F` preserves colimits for `K`. -/
lemma preservesColimit_of_reflects_of_preserves
    [PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] :
    PreservesColimit K F :=
  ⟨fun {c} h => ⟨by
    apply isColimitOfReflects G
    apply isColimitOfPreserves (F ⋙ G) h⟩⟩

Preservation of colimits via reflection and composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $K \colon J \to C$ be a diagram. If the composition $F \circ G$ preserves colimits for $K$, and $G$ reflects colimits for $K \circ F$, then $F$ preserves colimits for $K$.

CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves theorem

[PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] : PreservesColimit K F

Full source

@[deprecated "use preservesColimit_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesColimitOfReflectsOfPreserves
    [PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] :
    PreservesColimit K F :=
  preservesColimit_of_reflects_of_preserves F G

Preservation of colimits via reflection and composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $K \colon J \to C$ be a diagram. If the composition $F \circ G$ preserves colimits of $K$, and $G$ reflects colimits of $K \circ F$, then $F$ preserves colimits of $K$.

CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves theorem

[PreservesColimitsOfShape J (F ⋙ G)] [ReflectsColimitsOfShape J G] : PreservesColimitsOfShape J F

Full source

/-- If `F ⋙ G` preserves colimits of shape `J` and `G` reflects colimits of shape `J`, then `F`
preserves colimits of shape `J`.
-/
lemma preservesColimitsOfShape_of_reflects_of_preserves [PreservesColimitsOfShape J (F ⋙ G)]
    [ReflectsColimitsOfShape J G] : PreservesColimitsOfShape J F where
  preservesColimit := preservesColimit_of_reflects_of_preserves F G

Preservation of Colimits via Reflection and Composition for a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $J$ be a category. If the composition $F \circ G$ preserves all colimits of shape $J$, and $G$ reflects all colimits of shape $J$, then $F$ preserves all colimits of shape $J$.

CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves theorem

[PreservesColimitsOfShape J (F ⋙ G)] [ReflectsColimitsOfShape J G] : PreservesColimitsOfShape J F

Full source

@[deprecated "use preservesColimitsOfShape_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesColimitsOfShapeOfReflectsOfPreserves [PreservesColimitsOfShape J (F ⋙ G)]
    [ReflectsColimitsOfShape J G] : PreservesColimitsOfShape J F :=
  preservesColimitsOfShape_of_reflects_of_preserves F G

Preservation of Colimits via Reflection and Composition for a Given Shape

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $J$ be a category. If the composition $F \circ G$ preserves all colimits of shape $J$, and $G$ reflects all colimits of shape $J$, then $F$ preserves all colimits of shape $J$.

CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves theorem

[PreservesColimitsOfSize.{w', w} (F ⋙ G)] [ReflectsColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} F

Full source

/-- If `F ⋙ G` preserves colimits and `G` reflects colimits, then `F` preserves colimits. -/
lemma preservesColimits_of_reflects_of_preserves [PreservesColimitsOfSize.{w', w} (F ⋙ G)]
    [ReflectsColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} F where
  preservesColimitsOfShape := preservesColimitsOfShape_of_reflects_of_preserves F G

Preservation of Colimits via Reflection and Composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors. If the composition $F \circ G$ preserves all colimits (of any size), and $G$ reflects all colimits (of any size), then $F$ preserves all colimits (of any size).

CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves theorem

[PreservesColimitsOfSize.{w', w} (F ⋙ G)] [ReflectsColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} F

Full source

@[deprecated "use preservesColimits_of_reflects_of_preserves" (since := "2024-11-19")]
lemma preservesColimitsOfReflectsOfPreserves [PreservesColimitsOfSize.{w', w} (F ⋙ G)]
    [ReflectsColimitsOfSize.{w', w} G] : PreservesColimitsOfSize.{w', w} F :=
  preservesColimits_of_reflects_of_preserves F G

Preservation of Colimits via Reflection and Composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors. If the composition $F \circ G$ preserves all colimits (of any size), and $G$ reflects all colimits (of any size), then $F$ preserves all colimits (of any size).

CategoryTheory.Limits.reflectsColimit_of_iso_diagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsColimit K₁ F] : ReflectsColimit K₂ F

Full source

/-- Transfer reflection of colimits along a natural isomorphism in the diagram. -/
lemma reflectsColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [ReflectsColimit K₁ F] :
    ReflectsColimit K₂ F where
  reflects {c} t := ⟨by
    apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
    apply ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _).symm t).ofIsoColimit _
    exact Cocones.ext (Iso.refl _)⟩

Reflection of Colimits under Diagram Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Suppose $K_1, K_2 \colon J \to \mathcal{C}$ are naturally isomorphic diagrams via an isomorphism $h \colon K_1 \cong K_2$. If $F$ reflects colimits of $K_1$, then $F$ also reflects colimits of $K_2$.

CategoryTheory.Limits.reflectsColimitOfIsoDiagram theorem

{K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsColimit K₁ F] : ReflectsColimit K₂ F

Full source

@[deprecated "use reflectsColimit_of_iso_diagram" (since := "2024-11-19")]
lemma reflectsColimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [ReflectsColimit K₁ F] :
    ReflectsColimit K₂ F :=
  reflectsColimit_of_iso_diagram F h

Reflection of Colimits under Diagram Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two naturally isomorphic diagrams $K_1, K_2 \colon J \to \mathcal{C}$ with an isomorphism $h \colon K_1 \cong K_2$, if $F$ reflects colimits of $K_1$, then $F$ also reflects colimits of $K_2$.

CategoryTheory.Limits.reflectsColimit_of_natIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimit K F] : ReflectsColimit K G

Full source

/-- Transfer reflection of a colimit along a natural isomorphism in the functor. -/
lemma reflectsColimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimit K F] :
    ReflectsColimit K G where
  reflects t := ReflectsColimit.reflects (IsColimit.mapCoconeEquiv h.symm t)

Reflection of Colimits under Functor Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $K \colon J \to \mathcal{C}$ be a diagram. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ with an isomorphism $h \colon F \cong G$, if $F$ reflects colimits of $K$, then $G$ also reflects colimits of $K$.

CategoryTheory.Limits.reflectsColimitOfNatIso theorem

(K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimit K F] : ReflectsColimit K G

Full source

@[deprecated "use reflectsColimit_of_natIso" (since := "2024-11-19")]
lemma reflectsColimitOfNatIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimit K F] :
    ReflectsColimit K G :=
  reflectsColimit_of_natIso K h

Reflection of Colimits under Natural Isomorphism of Functors

Informal description

Let $K \colon J \to \mathcal{C}$ be a diagram in a category $\mathcal{C}$, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be naturally isomorphic functors with an isomorphism $h \colon F \cong G$. If $F$ reflects colimits of $K$, then $G$ also reflects colimits of $K$.

CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J G

Full source

/-- Transfer reflection of colimits of shape along a natural isomorphism in the functor. -/
lemma reflectsColimitsOfShape_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfShape J F] :
    ReflectsColimitsOfShape J G where
  reflectsColimit {K} := reflectsColimit_of_natIso K h

Reflection of Colimits of Shape under Functor Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ with an isomorphism $h \colon F \cong G$, if $F$ reflects colimits of shape $J$, then $G$ also reflects colimits of shape $J$.

CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J G

Full source

@[deprecated "use reflectsColimitsOfShape_of_natIso" (since := "2024-11-19")]
lemma reflectsColimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfShape J F] :
    ReflectsColimitsOfShape J G :=
  reflectsColimitsOfShape_of_natIso h

Reflection of Colimits of Shape under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $J$ be a small category. Given two naturally isomorphic functors $F, G \colon \mathcal{C} \to \mathcal{D}$ with an isomorphism $h \colon F \cong G$, if $F$ reflects colimits of shape $J$, then $G$ also reflects colimits of shape $J$.

CategoryTheory.Limits.reflectsColimits_of_natIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfSize.{w, w'} F] : ReflectsColimitsOfSize.{w, w'} G

Full source

/-- Transfer reflection of colimits along a natural isomorphism in the functor. -/
lemma reflectsColimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfSize.{w, w'} F] :
    ReflectsColimitsOfSize.{w, w'} G where
  reflectsColimitsOfShape := reflectsColimitsOfShape_of_natIso h

Reflection of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $h \colon F \cong G$. If $F$ reflects colimits of any size, then $G$ also reflects colimits of the same size. In other words, if for any diagram $K \colon J \to \mathcal{C}$, the functor $F$ maps a cocone over $K$ to a colimit cocone in $\mathcal{D}$ only when the original cocone was a colimit cocone in $\mathcal{C}$, then the same property holds for $G$.

CategoryTheory.Limits.reflectsColimitsOfNatIso theorem

{F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfSize.{w, w'} F] : ReflectsColimitsOfSize.{w, w'} G

Full source

@[deprecated "use reflectsColimits_of_natIso" (since := "2024-11-19")]
lemma reflectsColimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfSize.{w, w'} F] :
    ReflectsColimitsOfSize.{w, w'} G :=
  reflectsColimits_of_natIso h

Reflection of Colimits under Natural Isomorphism of Functors

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $h \colon F \cong G$. If $F$ reflects colimits of any size, then $G$ also reflects colimits of the same size. In other words, if for any diagram $K \colon J \to \mathcal{C}$, the functor $F$ maps a cocone over $K$ to a colimit cocone in $\mathcal{D}$ only when the original cocone was a colimit cocone in $\mathcal{C}$, then the same property holds for $G$.

CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [ReflectsColimitsOfShape J F] :
  ReflectsColimitsOfShape J' F

Full source

/-- Transfer reflection of colimits along an equivalence in the shape. -/
lemma reflectsColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J' F where
  reflectsColimit :=
    { reflects := fun {c} t => ⟨by
        apply IsColimit.ofWhiskerEquivalence e
        apply isColimitOfReflects F
        apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
        exact IsColimit.whiskerEquivalence t _⟩ }

Reflection of Colimits under Equivalence of Diagram Shapes

Informal description

Let $J$ and $J'$ be categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that reflects colimits of shape $J$. Then $F$ also reflects colimits of shape $J'$. In other words, if for any diagram $K \colon J \to C$, the functor $F$ maps a cocone over $K$ to a colimit cocone in $D$ only when the original cocone was a colimit cocone in $C$, then the same property holds for any diagram $K' \colon J' \to C$.

CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv theorem

 {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D) [ReflectsColimitsOfShape J F] :
  ReflectsColimitsOfShape J' F

Full source

@[deprecated "use reflectsColimitsOfShape_of_equiv" (since := "2024-11-19")]
lemma reflectsColimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J' F :=
  reflectsColimitsOfShape_of_equiv e F

Reflection of Colimits under Equivalence of Diagram Shapes

Informal description

Let $J$ and $J'$ be categories with an equivalence $e \colon J \simeq J'$, and let $F \colon C \to D$ be a functor that reflects colimits of shape $J$. Then $F$ also reflects colimits of shape $J'$. In other words, if for any diagram $K \colon J \to C$, the functor $F$ maps a cocone over $K$ to a colimit cocone in $D$ only when the original cocone was a colimit cocone in $C$, then the same property holds for any diagram $K' \colon J' \to C$.

CategoryTheory.Limits.reflectsColimitsOfSize_of_univLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F

Full source

/-- A functor reflecting larger colimits also reflects smaller colimits. -/
lemma reflectsColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F where
  reflectsColimitsOfShape {J} := reflectsColimitsOfShape_of_equiv
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

Reflection of Colimits under Universe Level Constraints

Informal description

Let $F \colon C \to D$ be a functor between categories, and suppose there are universe inequalities $\text{UnivLE}\{w, w'\}$ and $\text{UnivLE}\{w_2, w_2'\}$. If $F$ reflects colimits of size $(w', w_2')$, then $F$ also reflects colimits of size $(w, w_2)$.

CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE theorem

 (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F

Full source

@[deprecated "use reflectsColimitsOfSize_of_univLE" (since := "2024-11-19")]
lemma reflectsColimitsOfSizeOfUnivLE (F : C ⥤ D) [UnivLEUnivLE.{w, w'}] [UnivLEUnivLE.{w₂, w₂'}]
    [ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F :=
  reflectsColimitsOfSize_of_univLE.{w'} F

Reflection of Colimits under Universe Level Constraints

Informal description

Let $F \colon C \to D$ be a functor between categories, and suppose there are universe inequalities $u \leq u'$ and $v \leq v'$. If $F$ reflects colimits of size $(u', v')$, then $F$ also reflects colimits of size $(u, v)$.

CategoryTheory.Limits.reflectsColimitsOfSize_shrink theorem

(F : C ⥤ D) [ReflectsColimitsOfSize.{max w w₂, max w' w₂'} F] : ReflectsColimitsOfSize.{w, w'} F

Full source

/-- `reflectsColimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsColimitsOfSize.{w w'} F`
from some other `reflectsColimitsOfSize F`.
-/
lemma reflectsColimitsOfSize_shrink (F : C ⥤ D) [ReflectsColimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsColimitsOfSize.{w, w'} F := reflectsColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Reflection of Colimits under Size Shrinkage

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects colimits of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also reflects colimits of size $(w, w')$.

CategoryTheory.Limits.reflectsColimitsOfSizeShrink theorem

(F : C ⥤ D) [ReflectsColimitsOfSize.{max w w₂, max w' w₂'} F] : ReflectsColimitsOfSize.{w, w'} F

Full source

@[deprecated "use reflectsColimitsOfSize_shrink" (since := "2024-11-19")]
lemma reflectsColimitsOfSizeShrink (F : C ⥤ D) [ReflectsColimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsColimitsOfSize.{w, w'} F :=
  reflectsColimitsOfSize_shrink F

Reflection of Colimits under Size Reduction

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects colimits of diagrams of size $(\max(w, w_2), \max(w', w_2'))$, then $F$ also reflects colimits of diagrams of size $(w, w')$.

CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits theorem

(F : C ⥤ D) [ReflectsColimitsOfSize.{v₃, u₃} F] : ReflectsColimitsOfSize.{0, 0} F

Full source

/-- Reflecting colimits at any universe implies reflecting colimits at universe `0`. -/
lemma reflectsSmallestColimits_of_reflectsColimits (F : C ⥤ D) [ReflectsColimitsOfSize.{v₃, u₃} F] :
    ReflectsColimitsOfSize.{0, 0} F :=
  reflectsColimitsOfSize_shrink F

Reflection of Smallest Colimits from General Colimit Reflection

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects colimits of any size, then $F$ also reflects colimits of the smallest size (i.e., colimits indexed by diagrams in universe level 0).

CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits theorem

(F : C ⥤ D) [ReflectsColimitsOfSize.{v₃, u₃} F] : ReflectsColimitsOfSize.{0, 0} F

Full source

@[deprecated "use reflectsSmallestColimits_of_reflectsColimits" (since := "2024-11-19")]
lemma reflectsSmallestColimitsOfReflectsColimits (F : C ⥤ D) [ReflectsColimitsOfSize.{v₃, u₃} F] :
    ReflectsColimitsOfSize.{0, 0} F :=
  reflectsSmallestColimits_of_reflectsColimits F

Reflection of smallest colimits by a colimit-reflecting functor

Informal description

Let $F \colon C \to D$ be a functor between categories. If $F$ reflects colimits of any size, then $F$ also reflects colimits of the smallest size (i.e., colimits indexed by diagrams in the smallest universe level).

CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms theorem

(F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasColimit F] [PreservesColimit F G] : ReflectsColimit F G

Full source

/-- If the colimit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the colimit of `F`.
-/ -- Porting note: previous behavior of apply pushed instance holes into hypotheses, this errors
lemma reflectsColimit_of_reflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms]
    [HasColimit F] [PreservesColimit F G] : ReflectsColimit F G where
  reflects {c} t := by
    suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by
      apply IsColimit.ofPointIso (colimit.isColimit F)⟩
    change IsIso ((Cocones.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
    suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by
      apply (Cocones.forget F).map_isIso _
    suffices IsIso (Prefunctor.map (Cocones.functoriality F G).toPrefunctor
      (IsColimit.descCoconeMorphism (colimit.isColimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
    exact (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _

Reflection of Colimits by Isomorphism-Reflecting Functors

Informal description

Let $F \colon J \to C$ be a functor and $G \colon C \to D$ a functor that reflects isomorphisms. If $F$ has a colimit in $C$ and $G$ preserves this colimit, then $G$ reflects the colimit of $F$. That is, if the image of a cocone over $F$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms theorem

(F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasColimit F] [PreservesColimit F G] : ReflectsColimit F G

Full source

@[deprecated "use reflectsColimit_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsColimitOfReflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms]
    [HasColimit F] [PreservesColimit F G] : ReflectsColimit F G :=
  reflectsColimit_of_reflectsIsomorphisms F G

Reflection of Colimits by Isomorphism-Reflecting Functors

Informal description

Let $F \colon J \to C$ be a functor and $G \colon C \to D$ a functor that reflects isomorphisms. If $F$ has a colimit in $C$ and $G$ preserves this colimit, then $G$ reflects the colimit of $F$. That is, if the image of a cocone over $F$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfShape J C] [PreservesColimitsOfShape J G] :
  ReflectsColimitsOfShape J G

Full source

/--
If `C` has colimits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects colimits of shape `J`.
-/
lemma reflectsColimitsOfShape_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasColimitsOfShape J C] [PreservesColimitsOfShape J G] : ReflectsColimitsOfShape J G where
  reflectsColimit {F} := reflectsColimit_of_reflectsIsomorphisms F G

Reflection of Colimits by Isomorphism-Reflecting Functors with Given Shape

Informal description

Let $C$ be a category with colimits of shape $J$, and let $G \colon C \to D$ be a functor that preserves colimits of shape $J$ and reflects isomorphisms. Then $G$ reflects colimits of shape $J$, meaning that for any diagram $K \colon J \to C$, if the image of a cocone over $K$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfShape J C] [PreservesColimitsOfShape J G] :
  ReflectsColimitsOfShape J G

Full source

@[deprecated "use reflectsColimitsOfShape_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsColimitsOfShapeOfReflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasColimitsOfShape J C] [PreservesColimitsOfShape J G] : ReflectsColimitsOfShape J G :=
  reflectsColimitsOfShape_of_reflectsIsomorphisms

Reflection of Colimits by Isomorphism-Reflecting Functors with Given Shape

Informal description

Let $C$ be a category with colimits of shape $J$, and let $G \colon C \to D$ be a functor that preserves colimits of shape $J$ and reflects isomorphisms. Then $G$ reflects colimits of shape $J$, meaning that for any diagram $K \colon J \to C$, if the image of a cocone over $K$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfSize.{w', w} C] [PreservesColimitsOfSize.{w', w} G] :
  ReflectsColimitsOfSize.{w', w} G

Full source

/--
If `C` has colimits and `G` preserves colimits, then if `G` reflects isomorphisms then it reflects
colimits.
-/
lemma reflectsColimits_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasColimitsOfSize.{w', w} C] [PreservesColimitsOfSize.{w', w} G] :
    ReflectsColimitsOfSize.{w', w} G where
  reflectsColimitsOfShape := reflectsColimitsOfShape_of_reflectsIsomorphisms

Reflection of Colimits by Isomorphism-Reflecting Functors

Informal description

Let $C$ and $D$ be categories, and let $G \colon C \to D$ be a functor that reflects isomorphisms. If $C$ has all colimits of size $(w', w)$ and $G$ preserves colimits of size $(w', w)$, then $G$ reflects colimits of size $(w', w)$. That is, for any diagram $K \colon J \to C$ where $J$ is a category of size $(w', w)$, if the image of a cocone over $K$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms theorem

 {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfSize.{w', w} C] [PreservesColimitsOfSize.{w', w} G] :
  ReflectsColimitsOfSize.{w', w} G

Full source

@[deprecated "use reflectsColimits_of_reflectsIsomorphisms" (since := "2024-11-19")]
lemma reflectsColimitsOfReflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms]
    [HasColimitsOfSize.{w', w} C] [PreservesColimitsOfSize.{w', w} G] :
    ReflectsColimitsOfSize.{w', w} G :=
  reflectsColimits_of_reflectsIsomorphisms

Isomorphism-Reflecting Functors Reflect Colimits When Preserving Them

Informal description

Let $C$ and $D$ be categories, and let $G \colon C \to D$ be a functor that reflects isomorphisms. If $C$ has all colimits of size $(w', w)$ and $G$ preserves colimits of size $(w', w)$, then $G$ reflects colimits of size $(w', w)$. That is, for any diagram $K \colon J \to C$ where $J$ is a category of size $(w', w)$, if the image of a cocone over $K$ under $G$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.fullyFaithful_reflectsLimits instance

[F.Full] [F.Faithful] : ReflectsLimitsOfSize.{w, w'} F

Full source

/-- A fully faithful functor reflects limits. -/
instance fullyFaithful_reflectsLimits [F.Full] [F.Faithful] : ReflectsLimitsOfSize.{w, w'} F where
  reflectsLimitsOfShape {J} 𝒥₁ :=
    { reflectsLimit := fun {K} =>
        { reflects := fun {c} t =>
            ⟨(IsLimit.mkConeMorphism fun _ =>
                (Cones.functoriality K F).preimage (t.liftConeMorphism _)) <| by
              apply fun s m => (Cones.functoriality K F).map_injective _
              intro s m
              rw [Functor.map_preimage]
              apply t.uniq_cone_morphism⟩ } }

Fully Faithful Functors Reflect Limits

Informal description

A fully faithful functor $F \colon C \to D$ reflects limits. That is, if the image of a cone over a diagram $K \colon J \to C$ under $F$ is a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.fullyFaithfulReflectsLimits theorem

[F.Full] [F.Faithful] : ReflectsLimitsOfSize.{w, w'} F

Full source

@[deprecated "use fullyFaithful_reflectsLimits" (since := "2024-11-19")]
lemma fullyFaithfulReflectsLimits [F.Full] [F.Faithful] : ReflectsLimitsOfSize.{w, w'} F :=
  inferInstance

Fully Faithful Functors Reflect All Limits

Informal description

A fully faithful functor $F \colon C \to D$ reflects limits of all sizes. That is, for any diagram $K \colon J \to C$, if the image of a cone over $K$ under $F$ is a limit cone in $D$, then the original cone was already a limit cone in $C$.

CategoryTheory.Limits.fullyFaithful_reflectsColimits instance

[F.Full] [F.Faithful] : ReflectsColimitsOfSize.{w, w'} F

Full source

/-- A fully faithful functor reflects colimits. -/
instance fullyFaithful_reflectsColimits [F.Full] [F.Faithful] :
    ReflectsColimitsOfSize.{w, w'} F where
  reflectsColimitsOfShape {J} 𝒥₁ :=
    { reflectsColimit := fun {K} =>
        { reflects := fun {c} t =>
            ⟨(IsColimit.mkCoconeMorphism fun _ =>
                (Cocones.functoriality K F).preimage (t.descCoconeMorphism _)) <| by
              apply fun s m => (Cocones.functoriality K F).map_injective _
              intro s m
              rw [Functor.map_preimage]
              apply t.uniq_cocone_morphism⟩ }}

Fully Faithful Functors Reflect Colimits

Informal description

A fully faithful functor $F \colon C \to D$ reflects colimits. That is, for any functor $K \colon J \to C$, if the image of a cocone under $F$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.

CategoryTheory.Limits.fullyFaithfulReflectsColimits theorem

[F.Full] [F.Faithful] : ReflectsColimitsOfSize.{w, w'} F

Full source

@[deprecated "use fullyFaithful_reflectsColimits" (since := "2024-11-19")]
lemma fullyFaithfulReflectsColimits [F.Full] [F.Faithful] : ReflectsColimitsOfSize.{w, w'} F :=
  inferInstance

Fully Faithful Functors Reflect All Colimits

Informal description

A fully faithful functor $F \colon C \to D$ reflects colimits of any size. That is, for any diagram $K \colon J \to C$, if the image under $F$ of a cocone over $K$ is a colimit cocone in $D$, then the original cocone was already a colimit cocone in $C$.