Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv definition

: IsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g))

Full source

/--
The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `BinaryFan.mk` with `Functor.mapCone`.
-/
def isLimitMapConeBinaryFanEquiv :
    IsLimitIsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
  (IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm.trans
    (IsLimit.equivIsoLimit
      (Cones.ext (Iso.refl _)
        (by rintro (_ | _) <;> simp)))

Equivalence of limit conditions for mapped binary fans

Informal description

The property that the image of a binary fan under a functor $G$ is a limit cone is equivalent to the property that the binary fan formed by the images of the morphisms under $G$ is a limit cone. More precisely, for a binary fan $(f, g)$ in a category $\mathcal{C}$ and a functor $G \colon \mathcal{C} \to \mathcal{D}$, the following are equivalent: 1. The cone obtained by applying $G$ to the binary fan $\mathrm{BinaryFan.mk}\,f\,g$ is a limit cone in $\mathcal{D}$. 2. The binary fan $\mathrm{BinaryFan.mk}\,(G f)\,(G g)$ is a limit cone in $\mathcal{D}$. This equivalence is established by transporting the limit structure along the isomorphism between the two cones.

CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit definition

[PreservesLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk f g)) : IsLimit (BinaryFan.mk (G.map f) (G.map g))

Full source

/-- The property of preserving products expressed in terms of binary fans. -/
def mapIsLimitOfPreservesOfIsLimit [PreservesLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk f g)) :
    IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
  isLimitMapConeBinaryFanEquiv G f g (isLimitOfPreserves G l)

Preservation of binary product limits under a functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves the product of objects $X$ and $Y$, and a limit cone $(f, g)$ for the binary product of $X$ and $Y$ in $\mathcal{C}$, the image of this cone under $G$ is a limit cone for the binary product of $G(X)$ and $G(Y)$ in $\mathcal{D}$. More precisely, if $(f, g)$ is a limit cone for the binary product of $X$ and $Y$ in $\mathcal{C}$, then $(G(f), G(g))$ is a limit cone for the binary product of $G(X)$ and $G(Y)$ in $\mathcal{D}$.

CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit definition

[ReflectsLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk (G.map f) (G.map g))) : IsLimit (BinaryFan.mk f g)

Full source

/-- The property of reflecting products expressed in terms of binary fans. -/
def isLimitOfReflectsOfMapIsLimit [ReflectsLimit (pair X Y) G]
    (l : IsLimit (BinaryFan.mk (G.map f) (G.map g))) : IsLimit (BinaryFan.mk f g) :=
  isLimitOfReflects G ((isLimitMapConeBinaryFanEquiv G f g).symm l)

Reflection of binary product limits under a functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that reflects limits of pairs $(X, Y)$, if the binary fan formed by the images $(G f, G g)$ is a limit cone in $\mathcal{D}$, then the original binary fan $(f, g)$ is a limit cone in $\mathcal{C}$.

CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit definition

 [PreservesLimit (pair X Y) G] : IsLimit (BinaryFan.mk (G.map (Limits.prod.fst : X ⨯ Y ⟶ X)) (G.map Limits.prod.snd))

Full source

/-- If `G` preserves binary products and `C` has them, then the binary fan constructed of the mapped
morphisms of the binary product cone is a limit.
-/
def isLimitOfHasBinaryProductOfPreservesLimit [PreservesLimit (pair X Y) G] :
    IsLimit (BinaryFan.mk (G.map (Limits.prod.fst : X ⨯ YX ⨯ Y ⟶ X)) (G.map Limits.prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd X Y)

Limit cone of preserved binary product under a functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves the binary product of objects $X$ and $Y$, the binary fan formed by the images of the product projections $(G(\pi_1), G(\pi_2))$ under $G$ is a limit cone in $\mathcal{D}$ for the binary product of $G(X)$ and $G(Y)$. Here, $\pi_1 \colon X \times Y \to X$ and $\pi_2 \colon X \times Y \to Y$ are the product projections in $\mathcal{C}$.

CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison theorem

[i : IsIso (prodComparison G X Y)] : PreservesLimit (pair X Y) G

Full source

/-- If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
lemma PreservesLimitPair.of_iso_prod_comparison [i : IsIso (prodComparison G X Y)] :
    PreservesLimit (pair X Y) G := by
  apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)
  apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
  refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

Preservation of Binary Products via Isomorphic Product Comparison

Informal description

If the product comparison morphism $\mathrm{prodComparison}\,G\,X\,Y$ for a functor $G \colon \mathcal{C} \to \mathcal{D}$ at objects $X$ and $Y$ is an isomorphism, then $G$ preserves the binary product of $X$ and $Y$. Here, $\mathrm{prodComparison}\,G\,X\,Y$ is the canonical morphism from $G(X \times Y)$ to $G X \times G Y$ induced by the functor $G$ applied to the product projections.

CategoryTheory.Limits.PreservesLimitPair.iso definition

: G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y

Full source

/-- If `G` preserves the product of `(X,Y)`, then the product comparison map for `G` at `(X,Y)` is
an isomorphism.
-/
def PreservesLimitPair.iso : G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y :=
  IsLimit.conePointUniqueUpToIso (isLimitOfHasBinaryProductOfPreservesLimit G X Y) (limit.isLimit _)

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

Informal description

Given a functor $ G \colon \mathcal{C} \to \mathcal{D} $ that preserves the binary product of objects $ X $ and $ Y $, there is a canonical isomorphism $ G(X \times Y) \cong G(X) \times G(Y) $ in the category $\mathcal{D}$. This isomorphism is constructed by comparing the limit cone of the product in $\mathcal{C}$ with the limit cone of the product in $\mathcal{D}$ under the functor $ G $.

CategoryTheory.Limits.PreservesLimitPair.iso_hom theorem

: (PreservesLimitPair.iso G X Y).hom = prodComparison G X Y

Full source

@[simp]
theorem PreservesLimitPair.iso_hom : (PreservesLimitPair.iso G X Y).hom = prodComparison G X Y :=
  rfl

Homomorphism of Product Preservation Isomorphism Equals Product Comparison Morphism

Informal description

The homomorphism component of the isomorphism $\mathrm{PreservesLimitPair.iso}\,G\,X\,Y$ is equal to the product comparison morphism $\mathrm{prodComparison}\,G\,X\,Y$. Here, $\mathrm{PreservesLimitPair.iso}\,G\,X\,Y$ is the canonical isomorphism $G(X \times Y) \cong G(X) \times G(Y)$ induced by a functor $G$ that preserves the binary product of objects $X$ and $Y$, and $\mathrm{prodComparison}\,G\,X\,Y$ is the natural morphism from $G(X \times Y)$ to $G(X) \times G(Y)$.

CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst theorem

: (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.fst = prod.fst

Full source

@[simp, reassoc]
theorem PreservesLimitPair.iso_inv_fst :
    (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.fst = prod.fst := by
  rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
  simp

Inverse of Product-Preserving Isomorphism Commutes with First Projection

Informal description

For a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves the binary product of objects $X$ and $Y$ in $\mathcal{C}$, the inverse of the canonical isomorphism $G(X \times Y) \cong G(X) \times G(Y)$ satisfies the equation: $(G(X \times Y) \cong G(X) \times G(Y))^{-1} \circ G(\pi_1) = \pi_1$, where $\pi_1 \colon X \times Y \to X$ is the first projection morphism in $\mathcal{C}$.

CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd theorem

: (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.snd = prod.snd

Full source

@[simp, reassoc]
theorem PreservesLimitPair.iso_inv_snd :
    (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.snd = prod.snd := by
  rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
  simp

Inverse isomorphism preserves second projection in binary product

Informal description

For a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves the binary product of objects $X$ and $Y$, the inverse of the isomorphism $G(X \times Y) \cong G(X) \times G(Y)$ composed with $G$ applied to the second projection $\mathrm{prod.snd} \colon X \times Y \to Y$ equals the second projection $\mathrm{prod.snd} \colon G(X) \times G(Y) \to G(Y)$.

CategoryTheory.Limits.instIsIsoProdComparison instance

: IsIso (prodComparison G X Y)

Full source

instance : IsIso (prodComparison G X Y) := by
  rw [← PreservesLimitPair.iso_hom]
  infer_instance

Product Comparison Morphism is an Isomorphism

Informal description

The product comparison morphism $\mathrm{prodComparison}\,G\,X\,Y : G(X \times Y) \to G(X) \times G(Y)$ is an isomorphism in the category $\mathcal{D}$ for any functor $G \colon \mathcal{C} \to \mathcal{D}$ and objects $X, Y$ in $\mathcal{C}$.

CategoryTheory.Limits.preservesBinaryProducts_of_isIso_prodComparison theorem

 [HasBinaryProducts C] [HasBinaryProducts D] [i : ∀ {X Y : C}, IsIso (prodComparison G X Y)] :
  PreservesLimitsOfShape (Discrete WalkingPair) G

Full source

/-- If the product comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary products. -/
lemma preservesBinaryProducts_of_isIso_prodComparison
    [HasBinaryProducts C] [HasBinaryProducts D]
    [i : ∀ {X Y : C}, IsIso (prodComparison G X Y)] :
    PreservesLimitsOfShape (Discrete WalkingPair) G where
  preservesLimit := by
    intro K
    have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesLimitPair.of_iso_prod_comparison ..
    apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm

Preservation of Binary Products via Isomorphic Product Comparisons

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary products. If for every pair of objects $X, Y$ in $\mathcal{C}$, the product comparison morphism $\mathrm{prodComparison}\,G\,X\,Y$ is an isomorphism, then the functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves binary products. Here, $\mathrm{prodComparison}\,G\,X\,Y$ denotes the canonical morphism $G(X \times Y) \to G X \times G Y$ induced by applying $G$ to the product projections.

CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv definition

: IsColimit (Functor.mapCocone G (BinaryCofan.mk f g)) ≃ IsColimit (BinaryCofan.mk (G.map f) (G.map g))

Full source

/-- The map of a binary cofan is a colimit iff
the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `BinaryCofan.mk` with `Functor.mapCocone`.
-/
def isColimitMapCoconeBinaryCofanEquiv :
    IsColimitIsColimit (Functor.mapCocone G (BinaryCofan.mk f g))
    ≃ IsColimit (BinaryCofan.mk (G.map f) (G.map g)) :=
  (IsColimit.precomposeHomEquiv (diagramIsoPair _).symm _).symm.trans
    (IsColimit.equivIsoColimit
      (Cocones.ext (Iso.refl _)
        (by rintro (_ | _) <;> simp)))

Equivalence of colimit properties for mapped binary cofans

Informal description

The mapped binary cofan under a functor $ G $ is a colimit if and only if the cofork formed by the images of the morphisms under $ G $ is a colimit. This provides an equivalence between the colimit properties of the two constructions.

CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit definition

[PreservesColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk f g)) : IsColimit (BinaryCofan.mk (G.map f) (G.map g))

Full source

/-- The property of preserving coproducts expressed in terms of binary cofans. -/
def mapIsColimitOfPreservesOfIsColimit [PreservesColimit (pair X Y) G]
    (l : IsColimit (BinaryCofan.mk f g)) : IsColimit (BinaryCofan.mk (G.map f) (G.map g)) :=
  isColimitMapCoconeBinaryCofanEquiv G f g (isColimitOfPreserves G l)

Preservation of binary coproducts under colimit-preserving functors

Informal description

Given a functor $ G \colon C \to D $ that preserves the colimit of the pair $(X, Y)$, and given a colimit cocone $(f, g)$ on the binary cofan $(X, Y)$ in $ C $, the image of this cocone under $ G $ is a colimit cocone in $ D $. Specifically, the binary cofan $(G(f), G(g))$ is a colimit cocone in $ D $.

CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit definition

[ReflectsColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk (G.map f) (G.map g))) : IsColimit (BinaryCofan.mk f g)

Full source

/-- The property of reflecting coproducts expressed in terms of binary cofans. -/
def isColimitOfReflectsOfMapIsColimit [ReflectsColimit (pair X Y) G]
    (l : IsColimit (BinaryCofan.mk (G.map f) (G.map g))) : IsColimit (BinaryCofan.mk f g) :=
  isColimitOfReflects G ((isColimitMapCoconeBinaryCofanEquiv G f g).symm l)

Reflection of colimits for binary cofans

Informal description

Given a functor $ G $ that reflects colimits of the pair $(X, Y)$, if the binary cofan formed by the images $ G(f) $ and $ G(g) $ is a colimit, then the original binary cofan formed by $ f $ and $ g $ is also a colimit.

CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit definition

 [PreservesColimit (pair X Y) G] :
  IsColimit (BinaryCofan.mk (G.map (Limits.coprod.inl : X ⟶ X ⨿ Y)) (G.map Limits.coprod.inr))

Full source

/--
If `G` preserves binary coproducts and `C` has them, then the binary cofan constructed of the mapped
morphisms of the binary product cocone is a colimit.
-/
def isColimitOfHasBinaryCoproductOfPreservesColimit [PreservesColimit (pair X Y) G] :
    IsColimit (BinaryCofan.mk (G.map (Limits.coprod.inl : X ⟶ X ⨿ Y)) (G.map Limits.coprod.inr)) :=
  mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod X Y)

Preservation of binary coproducts under colimit-preserving functors

Informal description

Given a functor $ G \colon C \to D $ that preserves the colimit of the pair $(X, Y)$, the binary cofan formed by the images of the coproduct inclusions $ G(\mathrm{coprod.inl}) $ and $ G(\mathrm{coprod.inr}) $ is a colimit cocone in $ D $. Here, $ \mathrm{coprod.inl} \colon X \to X \sqcup Y $ and $ \mathrm{coprod.inr} \colon Y \to X \sqcup Y $ are the canonical morphisms into the coproduct $ X \sqcup Y $ in $ C $.

CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison theorem

[i : IsIso (coprodComparison G X Y)] : PreservesColimit (pair X Y) G

Full source

/-- If the coproduct comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
lemma PreservesColimitPair.of_iso_coprod_comparison [i : IsIso (coprodComparison G X Y)] :
    PreservesColimit (pair X Y) G := by
  apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)
  apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
  refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

Preservation of Coproduct via Isomorphism of Coproduct Comparison

Informal description

If the coproduct comparison morphism $\mathrm{coprodComparison}\,G\,X\,Y$ for a functor $G$ at objects $X$ and $Y$ is an isomorphism, then $G$ preserves the coproduct of $X$ and $Y$.

CategoryTheory.Limits.PreservesColimitPair.iso definition

: G.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y)

Full source

/--
If `G` preserves the coproduct of `(X,Y)`, then the coproduct comparison map for `G` at `(X,Y)` is
an isomorphism.
-/
def PreservesColimitPair.iso : G.obj X ⨿ G.obj YG.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y) :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
    (isColimitOfHasBinaryCoproductOfPreservesColimit G X Y)

Natural isomorphism for preserved coproducts under colimit-preserving functors

Informal description

Given a functor $G \colon C \to D$ that preserves the colimit of the pair $(X, Y)$, there exists a natural isomorphism between the coproduct of $G(X)$ and $G(Y)$ in $D$ and the image under $G$ of the coproduct of $X$ and $Y$ in $C$, i.e., $G(X) \sqcup G(Y) \cong G(X \sqcup Y)$.

CategoryTheory.Limits.PreservesColimitPair.iso_hom theorem

: (PreservesColimitPair.iso G X Y).hom = coprodComparison G X Y

Full source

@[simp]
theorem PreservesColimitPair.iso_hom :
    (PreservesColimitPair.iso G X Y).hom = coprodComparison G X Y := rfl

Homomorphism of Preserved Coproduct Isomorphism Equals Coproduct Comparison

Informal description

The homomorphism component of the natural isomorphism $\mathrm{PreservesColimitPair.iso}\,G\,X\,Y$ is equal to the coproduct comparison morphism $\mathrm{coprodComparison}\,G\,X\,Y$.

CategoryTheory.Limits.instIsIsoCoprodComparison instance

: IsIso (coprodComparison G X Y)

Full source

instance : IsIso (coprodComparison G X Y) := by
  rw [← PreservesColimitPair.iso_hom]
  infer_instance

Coproduct Comparison Morphism is an Isomorphism

Informal description

For any functor $G \colon C \to D$ between categories with binary coproducts, the coproduct comparison morphism $\mathrm{coprodComparison}\,G\,X\,Y \colon G(X) \sqcup G(Y) \to G(X \sqcup Y)$ is an isomorphism.

CategoryTheory.Limits.preservesBinaryCoproducts_of_isIso_coprodComparison theorem

 [HasBinaryCoproducts C] [HasBinaryCoproducts D] [i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)] :
  PreservesColimitsOfShape (Discrete WalkingPair) G

Full source

/-- If the coproduct comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary coproducts. -/
lemma preservesBinaryCoproducts_of_isIso_coprodComparison
    [HasBinaryCoproducts C] [HasBinaryCoproducts D]
    [i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)] :
    PreservesColimitsOfShape (Discrete WalkingPair) G where
  preservesColimit := by
    intro K
    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
    apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

Preservation of Binary Coproducts via Isomorphic Coproduct Comparisons

Informal description

Let $C$ and $D$ be categories with binary coproducts, and let $G \colon C \to D$ be a functor. If for every pair of objects $X, Y$ in $C$, the coproduct comparison morphism $\mathrm{coprodComparison}\,G\,X\,Y$ is an isomorphism, then $G$ preserves all binary coproducts (i.e., $G$ preserves colimits of shape $\mathrm{Discrete}\,\mathrm{WalkingPair}$).