Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

CategoryTheory.Limits.isLimitMapConeFanMkEquiv definition

 {P : C} (g : ∀ j, P ⟶ f j) :
  IsLimit (Functor.mapCone G (Fan.mk P g)) ≃ IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j))

Full source

/-- The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This
essentially lets us commute `Fan.mk` with `Functor.mapCone`.
-/
def isLimitMapConeFanMkEquiv {P : C} (g : ∀ j, P ⟶ f j) :
    IsLimitIsLimit (Functor.mapCone G (Fan.mk P g)) ≃
      IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j)) := by
  refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
  · refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
  refine Cones.ext (Iso.refl _) fun j =>
      by dsimp; cases j; simp

Equivalence of limit conditions for mapped fan construction

Informal description

Given a functor $ G \colon C \to D $, an object $ P $ in $ C $, and a family of morphisms $ g_j \colon P \to f(j) $ for each $ j $ in some indexing set, there is an equivalence between: 1. The property that the image under $ G $ of the fan $ \mathrm{Fan.mk}\,P\,g $ is a limit cone in $ D $. 2. The property that the fan $ \mathrm{Fan.mk}\,(G.obj\,P)\,(\lambda j, G.map\,(g_j)) $ is a limit cone in $ D $. This equivalence is established by composing with a natural isomorphism and transporting the limit structure along a cone isomorphism.

CategoryTheory.Limits.isLimitFanMkObjOfIsLimit definition

 [PreservesLimit (Discrete.functor f) G] {P : C} (g : ∀ j, P ⟶ f j) (t : IsLimit (Fan.mk _ g)) :
  IsLimit (Fan.mk (G.obj P) fun j => G.map (g j) : Fan fun j => G.obj (f j))

Full source

/-- The property of preserving products expressed in terms of fans. -/
def isLimitFanMkObjOfIsLimit [PreservesLimit (Discrete.functor f) G] {P : C} (g : ∀ j, P ⟶ f j)
    (t : IsLimit (Fan.mk _ g)) :
    IsLimit (Fan.mk (G.obj P) fun j => G.map (g j) : Fan fun j => G.obj (f j)) :=
  isLimitMapConeFanMkEquiv _ _ _ (isLimitOfPreserves G t)

Preservation of limit fan under a functor

Informal description

Given a functor $G \colon C \to D$ that preserves the limit of the discrete functor $\mathrm{Discrete.functor}\,f$, an object $P$ in $C$, and a family of morphisms $g_j \colon P \to f(j)$ for each $j$ in some indexing set, if the fan $\mathrm{Fan.mk}\,P\,g$ is a limit cone in $C$, then the fan $\mathrm{Fan.mk}\,(G.obj\,P)\,(\lambda j, G.map\,(g_j))$ is a limit cone in $D$.

CategoryTheory.Limits.isLimitOfIsLimitFanMkObj definition

 [ReflectsLimit (Discrete.functor f) G] {P : C} (g : ∀ j, P ⟶ f j)
  (t : IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j))) : IsLimit (Fan.mk P g)

Full source

/-- The property of reflecting products expressed in terms of fans. -/
def isLimitOfIsLimitFanMkObj [ReflectsLimit (Discrete.functor f) G] {P : C} (g : ∀ j, P ⟶ f j)
    (t : IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j))) :
    IsLimit (Fan.mk P g) :=
  isLimitOfReflects G ((isLimitMapConeFanMkEquiv _ _ _).symm t)

Reflection of limit cones via fans under a functor

Informal description

Given a functor $ G \colon C \to D $ that reflects limits of the discrete functor $ \mathrm{Discrete.functor}\,f $, an object $ P $ in $ C $, and a family of morphisms $ g_j \colon P \to f(j) $ for each $ j $ in some indexing set, if the fan $ \mathrm{Fan.mk}\,(G.obj\,P)\,(\lambda j, G.map\,(g_j)) $ is a limit cone in $ D $, then the original fan $ \mathrm{Fan.mk}\,P\,g $ is a limit cone in $ C $.

CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit definition

[PreservesLimit (Discrete.functor f) G] : IsLimit (Fan.mk _ fun j : J => G.map (Pi.π f j) : Fan fun j => G.obj (f j))

Full source

/--
If `G` preserves products and `C` has them, then the fan constructed of the mapped projection of a
product is a limit.
-/
def isLimitOfHasProductOfPreservesLimit [PreservesLimit (Discrete.functor f) G] :
    IsLimit (Fan.mk _ fun j : J => G.map (Pi.π f j) : Fan fun j => G.obj (f j)) :=
  isLimitFanMkObjOfIsLimit G f _ (productIsProduct _)

Preservation of product limits under a functor

Informal description

Given a functor $G \colon C \to D$ that preserves the limit of the discrete functor $\mathrm{Discrete.functor}\,f$ and a category $C$ that has products indexed by $J$, the fan constructed from the images under $G$ of the canonical projections $\pi_j \colon \prod_{j \in J} f(j) \to f(j)$ is a limit cone in $D$. Specifically, the fan $\mathrm{Fan.mk}\,(G.obj\,(\prod_{j \in J} f(j)))\,(\lambda j, G.map\,(\pi_j))$ is a limit cone over the family $\{G.obj\,(f(j))\}_{j \in J}$ in $D$.

CategoryTheory.Limits.PreservesProduct.of_iso_comparison theorem

[i : IsIso (piComparison G f)] : PreservesLimit (Discrete.functor f) G

Full source

/-- If `pi_comparison G f` is an isomorphism, then `G` preserves the limit of `f`. -/
lemma PreservesProduct.of_iso_comparison [i : IsIso (piComparison G f)] :
    PreservesLimit (Discrete.functor f) G := by
  apply preservesLimit_of_preserves_limit_cone (productIsProduct f)
  apply (isLimitMapConeFanMkEquiv _ _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _
    (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

Preservation of Products via Isomorphic Comparison Morphism

Informal description

If the comparison morphism $\mathrm{piComparison}\,G\,f$ is an isomorphism, then the functor $G$ preserves the product of the family of objects $\{f(b)\}_{b \in \beta}$.

CategoryTheory.Limits.PreservesProduct.iso definition

: G.obj (∏ᶜ f) ≅ ∏ᶜ fun j => G.obj (f j)

Full source

/--
If `G` preserves limits, we have an isomorphism from the image of a product to the product of the
images.
-/
def PreservesProduct.iso : G.obj (∏ᶜ f) ≅ ∏ᶜ fun j => G.obj (f j) :=
  IsLimit.conePointUniqueUpToIso (isLimitOfHasProductOfPreservesLimit G f) (limit.isLimit _)

Isomorphism between image of product and product of images under a functor

Informal description

Given a functor $G \colon C \to D$ that preserves the product of a family of objects $\{f(b)\}_{b \in \beta}$ in $C$, there is a natural isomorphism between the image of the product $\prod_{b \in \beta} f(b)$ under $G$ and the product of the images $\prod_{b \in \beta} G(f(b))$ in $D$. This isomorphism is constructed using the universal property of limits, specifically by comparing the limit cones of the product in $C$ and its image under $G$ in $D$.

CategoryTheory.Limits.PreservesProduct.iso_hom theorem

: (PreservesProduct.iso G f).hom = piComparison G f

Full source

@[simp]
theorem PreservesProduct.iso_hom : (PreservesProduct.iso G f).hom = piComparison G f :=
  rfl

Homomorphism of Product Preservation Isomorphism Equals Comparison Morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves the product of a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$, the homomorphism component of the natural isomorphism $\mathrm{PreservesProduct.iso}\,G\,f$ is equal to the comparison morphism $\mathrm{piComparison}\,G\,f$.

CategoryTheory.Limits.instIsIsoPiComparison instance

: IsIso (piComparison G f)

Full source

instance : IsIso (piComparison G f) := by
  rw [← PreservesProduct.iso_hom]
  infer_instance

Comparison Morphism for Products is an Isomorphism

Informal description

For any functor $G \colon \mathcal{C} \to \mathcal{D}$ and any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ that has a product, the comparison morphism $\mathrm{piComparison}\,G\,f \colon G(\prod_{b \in \beta} f(b)) \to \prod_{b \in \beta} G(f(b))$ is an isomorphism.

CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv definition

 {P : C} (g : ∀ j, f j ⟶ P) :
  IsColimit (Functor.mapCocone G (Cofan.mk P g)) ≃
    IsColimit (Cofan.mk _ fun j => G.map (g j) : Cofan fun j => G.obj (f j))

Full source

/-- The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit.
This essentially lets us commute `Cofan.mk` with `Functor.mapCocone`.
-/
def isColimitMapCoconeCofanMkEquiv {P : C} (g : ∀ j, f j ⟶ P) :
    IsColimitIsColimit (Functor.mapCocone G (Cofan.mk P g)) ≃
      IsColimit (Cofan.mk _ fun j => G.map (g j) : Cofan fun j => G.obj (f j)) := by
  refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
  · refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
  refine Cocones.ext (Iso.refl _) fun j => by dsimp; cases j; simp

Equivalence of colimit properties for mapped cofans

Informal description

Given a functor $G \colon C \to D$, a family of objects $\{f(j)\}_{j \in J}$ in $C$, an object $P \in C$, and a family of morphisms $\{g_j \colon f(j) \to P\}_{j \in J}$, there is an equivalence between: 1. The property that the image under $G$ of the cofan $\mathrm{Cofan.mk}\,P\,g$ is a colimit cocone in $D$ 2. The property that the cofan $\mathrm{Cofan.mk}\,(G(P))\,(G \circ g)$ is a colimit cocone in $D$ This equivalence is established by precomposing with a natural isomorphism and then transporting the colimit property along a cocone isomorphism.

CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit definition

 [PreservesColimit (Discrete.functor f) G] {P : C} (g : ∀ j, f j ⟶ P) (t : IsColimit (Cofan.mk _ g)) :
  IsColimit (Cofan.mk (G.obj P) fun j => G.map (g j) : Cofan fun j => G.obj (f j))

Full source

/-- The property of preserving coproducts expressed in terms of cofans. -/
def isColimitCofanMkObjOfIsColimit [PreservesColimit (Discrete.functor f) G] {P : C}
    (g : ∀ j, f j ⟶ P) (t : IsColimit (Cofan.mk _ g)) :
    IsColimit (Cofan.mk (G.obj P) fun j => G.map (g j) : Cofan fun j => G.obj (f j)) :=
  isColimitMapCoconeCofanMkEquiv _ _ _ (isColimitOfPreserves G t)

Preservation of colimit cofan under a functor

Informal description

Given a functor $G \colon C \to D$ that preserves colimits of the discrete functor associated with a family of objects $\{f(j)\}_{j \in J}$ in $C$, an object $P \in C$, a family of morphisms $\{g_j \colon f(j) \to P\}_{j \in J}$, and a proof that the cofan $\mathrm{Cofan.mk}\,P\,g$ is a colimit cocone in $C$, then the cofan $\mathrm{Cofan.mk}\,(G(P))\,(G \circ g)$ is a colimit cocone in $D$.

CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj definition

 [ReflectsColimit (Discrete.functor f) G] {P : C} (g : ∀ j, f j ⟶ P)
  (t : IsColimit (Cofan.mk _ fun j => G.map (g j) : Cofan fun j => G.obj (f j))) : IsColimit (Cofan.mk P g)

Full source

/-- The property of reflecting coproducts expressed in terms of cofans. -/
def isColimitOfIsColimitCofanMkObj [ReflectsColimit (Discrete.functor f) G] {P : C}
    (g : ∀ j, f j ⟶ P)
    (t : IsColimit (Cofan.mk _ fun j => G.map (g j) : Cofan fun j => G.obj (f j))) :
    IsColimit (Cofan.mk P g) :=
  isColimitOfReflects G ((isColimitMapCoconeCofanMkEquiv _ _ _).symm t)

Reflection of colimits via cofans

Informal description

Given a functor $G \colon C \to D$ that reflects colimits of the discrete functor $\mathrm{Discrete.functor}\,f$, an object $P \in C$, and a family of morphisms $\{g_j \colon f(j) \to P\}_{j \in J}$, if the cofan $\mathrm{Cofan.mk}\,(G(P))\,(G \circ g)$ is a colimit cocone in $D$, then the original cofan $\mathrm{Cofan.mk}\,P\,g$ is a colimit cocone in $C$.

CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit definition

 [PreservesColimit (Discrete.functor f) G] :
  IsColimit (Cofan.mk _ fun j : J => G.map (Sigma.ι f j) : Cofan fun j => G.obj (f j))

Full source

/-- If `G` preserves coproducts and `C` has them,
then the cofan constructed of the mapped inclusion of a coproduct is a colimit.
-/
def isColimitOfHasCoproductOfPreservesColimit [PreservesColimit (Discrete.functor f) G] :
    IsColimit (Cofan.mk _ fun j : J => G.map (Sigma.ι f j) : Cofan fun j => G.obj (f j)) :=
  isColimitCofanMkObjOfIsColimit G f _ (coproductIsCoproduct _)

Preservation of coproducts under a colimit-preserving functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves colimits of the discrete functor associated with a family of objects $\{f(j)\}_{j \in J}$ in $\mathcal{C}$, the cofan constructed from the images under $G$ of the coprojection morphisms $\iota_j \colon f(j) \to \coprod_{j \in J} f(j)$ is a colimit cocone in $\mathcal{D}$. In other words, the functor $G$ preserves the coproduct of the family $\{f(j)\}_{j \in J}$.

CategoryTheory.Limits.PreservesCoproduct.of_iso_comparison theorem

[i : IsIso (sigmaComparison G f)] : PreservesColimit (Discrete.functor f) G

Full source

/-- If `sigma_comparison G f` is an isomorphism, then `G` preserves the colimit of `f`. -/
lemma PreservesCoproduct.of_iso_comparison [i : IsIso (sigmaComparison G f)] :
    PreservesColimit (Discrete.functor f) G := by
  apply preservesColimit_of_preserves_colimit_cocone (coproductIsCoproduct f)
  apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _
    (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i

Preservation of Coproducts via Isomorphic Comparison Morphism

Informal description

If the comparison morphism $\sigma \colon \coprod_{b \in \beta} G(f(b)) \to G(\coprod_{b \in \beta} f(b))$ is an isomorphism, then the functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves the colimit of the functor $\mathrm{Discrete.functor}\,f \colon \mathrm{Discrete}\,\beta \to \mathcal{C}$.

CategoryTheory.Limits.PreservesCoproduct.iso definition

: G.obj (∐ f) ≅ ∐ fun j => G.obj (f j)

Full source

/-- If `G` preserves colimits,
we have an isomorphism from the image of a coproduct to the coproduct of the images.
-/
def PreservesCoproduct.iso : G.obj (∐ f) ≅ ∐ fun j => G.obj (f j) :=
  IsColimit.coconePointUniqueUpToIso (isColimitOfHasCoproductOfPreservesColimit G f)
    (colimit.isColimit _)

Isomorphism between image of coproduct and coproduct of images under a coproduct-preserving functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves coproducts of a family of objects $\{f(j)\}_{j \in J}$ in $\mathcal{C}$, there is a natural isomorphism between $G(\coprod_{j \in J} f(j))$ and $\coprod_{j \in J} G(f(j))$ in $\mathcal{D}$. This isomorphism is constructed using the universal property of colimits and the fact that $G$ preserves the colimit of the discrete functor associated with $f$.

CategoryTheory.Limits.PreservesCoproduct.inv_hom theorem

: (PreservesCoproduct.iso G f).inv = sigmaComparison G f

Full source

@[simp]
theorem PreservesCoproduct.inv_hom : (PreservesCoproduct.iso G f).inv = sigmaComparison G f := rfl

Inverse of Coproduct-Preserving Isomorphism Equals Comparison Morphism

Informal description

The inverse of the isomorphism $\mathrm{PreservesCoproduct.iso}\,G\,f$ between $G(\coprod f)$ and $\coprod (G \circ f)$ is equal to the coproduct comparison morphism $\sigma \colon \coprod (G \circ f) \to G(\coprod f)$.

CategoryTheory.Limits.instIsIsoSigmaComparison instance

: IsIso (sigmaComparison G f)

Full source

instance : IsIso (sigmaComparison G f) := by
  rw [← PreservesCoproduct.inv_hom]
  infer_instance

Coproduct Comparison Morphism is an Isomorphism

Informal description

For any functor $G \colon \mathcal{C} \to \mathcal{D}$ and any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$, the coproduct comparison morphism $\sigma \colon \coprod_{b \in \beta} G(f(b)) \to G(\coprod_{b \in \beta} f(b))$ is an isomorphism.

CategoryTheory.Limits.preservesLimitsOfShape_of_discrete theorem

(F : C ⥤ D) [∀ (f : J → C), PreservesLimit (Discrete.functor f) F] : PreservesLimitsOfShape (Discrete J) F

Full source

/-- If `F` preserves the limit of every `Discrete.functor f`, it preserves all limits of shape
`Discrete J`. -/
lemma preservesLimitsOfShape_of_discrete (F : C ⥤ D)
    [∀ (f : J → C), PreservesLimit (Discrete.functor f) F] :
    PreservesLimitsOfShape (Discrete J) F where
  preservesLimit := preservesLimit_of_iso_diagram F (Discrete.natIsoFunctor).symm

Preservation of Limits of Discrete Shape via Preservation of All Discrete Functor Limits

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$. If $F$ preserves the limit of every functor $\mathrm{Discrete.functor}\,f \colon \mathrm{Discrete}\,J \to \mathcal{C}$ (where $f \colon J \to \mathcal{C}$ is any function), then $F$ preserves all limits of shape $\mathrm{Discrete}\,J$.

CategoryTheory.Limits.preservesColimitsOfShape_of_discrete theorem

(F : C ⥤ D) [∀ (f : J → C), PreservesColimit (Discrete.functor f) F] : PreservesColimitsOfShape (Discrete J) F

Full source

/-- If `F` preserves the colimit of every `Discrete.functor f`, it preserves all colimits of shape
`Discrete J`. -/
lemma preservesColimitsOfShape_of_discrete (F : C ⥤ D)
    [∀ (f : J → C), PreservesColimit (Discrete.functor f) F] :
    PreservesColimitsOfShape (Discrete J) F where
  preservesColimit := preservesColimit_of_iso_diagram F (Discrete.natIsoFunctor).symm

Preservation of Colimits over Discrete Categories

Informal description

Let $F \colon C \to D$ be a functor between categories $C$ and $D$. If $F$ preserves the colimit of every functor $\mathrm{Discrete.functor}\,f \colon \mathrm{Discrete}\,J \to C$ induced by a function $f \colon J \to C$, then $F$ preserves all colimits of shape $\mathrm{Discrete}\,J$.