Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

CategoryTheory.Limits.WalkingPair inductive

: Type

Full source

/-- The type of objects for the diagram indexing a binary (co)product. -/
inductive WalkingPair : Type
  | left
  | right
  deriving DecidableEq, Inhabited

Indexing category for binary (co)products

Informal description

The inductive type `WalkingPair` represents the indexing category for binary (co)product diagrams in category theory. It consists of two objects, typically interpreted as the left and right components of a binary (co)product.

CategoryTheory.Limits.instDecidableEqWalkingPair instance

: DecidableEq✝ CategoryTheory.Limits.WalkingPair

Full source

DecidableEq, Inhabited

Decidable Equality for the WalkingPair Category

Informal description

The indexing category `WalkingPair` for binary (co)products has decidable equality.

CategoryTheory.Limits.instInhabitedWalkingPair instance

: Inhabited✝ (@CategoryTheory.Limits.WalkingPair)

Full source

Inhabited

Inhabitedness of the WalkingPair Category

Informal description

The indexing category `WalkingPair` for binary (co)products is inhabited.

CategoryTheory.Limits.WalkingPair.swap definition

: WalkingPair ≃ WalkingPair

Full source

/-- The equivalence swapping left and right.
-/
def WalkingPair.swap : WalkingPairWalkingPair ≃ WalkingPair where
  toFun
    | left => right
    | right => left
  invFun
    | left => right
    | right => left
  left_inv j := by cases j <;> rfl
  right_inv j := by cases j <;> rfl

Swapping equivalence for binary (co)product indexing category

Informal description

The equivalence that swaps the left and right objects in the indexing category `WalkingPair` for binary (co)products. Specifically, it maps `left` to `right` and `right` to `left`, with its inverse doing the same mapping.

CategoryTheory.Limits.WalkingPair.swap_apply_left theorem

: WalkingPair.swap left = right

Full source

@[simp]
theorem WalkingPair.swap_apply_left : WalkingPair.swap left = right :=
  rfl

Swap Maps Left to Right in Walking Pair Indexing Category

Informal description

The swapping equivalence applied to the left object of the walking pair indexing category yields the right object, i.e., $\text{swap}(\text{left}) = \text{right}$.

CategoryTheory.Limits.WalkingPair.swap_apply_right theorem

: WalkingPair.swap right = left

Full source

@[simp]
theorem WalkingPair.swap_apply_right : WalkingPair.swap right = left :=
  rfl

Swap Maps Right to Left in Walking Pair Indexing Category

Informal description

The swapping equivalence applied to the right object of the walking pair indexing category yields the left object, i.e., $\text{swap}(\text{right}) = \text{left}$.

CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt theorem

: WalkingPair.swap.symm left = right

Full source

@[simp]
theorem WalkingPair.swap_symm_apply_tt : WalkingPair.swap.symm left = right :=
  rfl

Inverse Swap Maps Left to Right in Walking Pair Indexing Category

Informal description

The inverse of the swapping equivalence applied to the left object of the walking pair indexing category yields the right object, i.e., $\text{swap}^{-1}(\text{left}) = \text{right}$.

CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff theorem

: WalkingPair.swap.symm right = left

Full source

@[simp]
theorem WalkingPair.swap_symm_apply_ff : WalkingPair.swap.symm right = left :=
  rfl

Inverse Swap Maps Right to Left in Walking Pair Indexing Category

Informal description

The inverse of the swapping equivalence applied to the right object of the walking pair indexing category yields the left object, i.e., $\text{swap}^{-1}(\text{right}) = \text{left}$.

CategoryTheory.Limits.WalkingPair.equivBool definition

: WalkingPair ≃ Bool

Full source

/-- An equivalence from `WalkingPair` to `Bool`, sometimes useful when reindexing limits.
-/
def WalkingPair.equivBool : WalkingPairWalkingPair ≃ Bool where
  toFun
    | left => true
    | right => false
  -- to match equiv.sum_equiv_sigma_bool
  invFun b := Bool.recOn b right left
  left_inv j := by cases j <;> rfl
  right_inv b := by cases b <;> rfl

Equivalence between WalkingPair and Bool

Informal description

The equivalence between the indexing category `WalkingPair` (consisting of two objects `left` and `right`) and the Boolean type `Bool`, mapping `left` to `true` and `right` to `false`. This equivalence is sometimes useful when reindexing limits or colimits.

CategoryTheory.Limits.WalkingPair.equivBool_apply_left theorem

: WalkingPair.equivBool left = true

Full source

@[simp]
theorem WalkingPair.equivBool_apply_left : WalkingPair.equivBool left = true :=
  rfl

Equivalence Maps Left Object to True

Informal description

The equivalence between the indexing category `WalkingPair` and the Boolean type `Bool` maps the `left` object of `WalkingPair` to `true`, i.e., $\text{equivBool}(\text{left}) = \text{true}$.

CategoryTheory.Limits.WalkingPair.equivBool_apply_right theorem

: WalkingPair.equivBool right = false

Full source

@[simp]
theorem WalkingPair.equivBool_apply_right : WalkingPair.equivBool right = false :=
  rfl

Equivalence Maps Right Object to False

Informal description

The equivalence between the indexing category `WalkingPair` and the Boolean type `Bool` maps the `right` object of `WalkingPair` to `false`, i.e., $\text{equivBool}(\text{right}) = \text{false}$.

CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true theorem

: WalkingPair.equivBool.symm true = left

Full source

@[simp]
theorem WalkingPair.equivBool_symm_apply_true : WalkingPair.equivBool.symm true = left :=
  rfl

Inverse Equivalence Maps True to Left Object

Informal description

The inverse of the equivalence between `WalkingPair` and `Bool` maps `true` to the `left` object of `WalkingPair`, i.e., $\text{equivBool}^{-1}(\text{true}) = \text{left}$.

CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false theorem

: WalkingPair.equivBool.symm false = right

Full source

@[simp]
theorem WalkingPair.equivBool_symm_apply_false : WalkingPair.equivBool.symm false = right :=
  rfl

Inverse Equivalence Maps False to Right Object

Informal description

The inverse of the equivalence between `WalkingPair` and `Bool` maps `false` to the `right` object of `WalkingPair`, i.e., $\text{equivBool}^{-1}(\text{false}) = \text{right}$.

CategoryTheory.Limits.pairFunction definition

(X Y : C) : WalkingPair → C

Full source

/-- The function on the walking pair, sending the two points to `X` and `Y`. -/
def pairFunction (X Y : C) : WalkingPair → C := fun j => WalkingPair.casesOn j X Y

Pair indexing function

Informal description

The function `pairFunction X Y` maps the objects of the indexing category `WalkingPair` to the objects `X` and `Y` in the category `C`. Specifically, it sends the left object to `X` and the right object to `Y`.

CategoryTheory.Limits.pairFunction_left theorem

(X Y : C) : pairFunction X Y left = X

Full source

@[simp]
theorem pairFunction_left (X Y : C) : pairFunction X Y left = X :=
  rfl

Pair Function Maps Left to First Object

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$, the pair indexing function evaluated at the left object of the walking pair category equals $X$, i.e., $\text{pairFunction}(X,Y)(\text{left}) = X$.

CategoryTheory.Limits.pairFunction_right theorem

(X Y : C) : pairFunction X Y right = Y

Full source

@[simp]
theorem pairFunction_right (X Y : C) : pairFunction X Y right = Y :=
  rfl

Right Component of Pair Indexing Function

Informal description

For any objects $X$ and $Y$ in a category $C$, the pair indexing function maps the right object of the walking pair category to $Y$, i.e., $\text{pairFunction}(X, Y)(\text{right}) = Y$.

CategoryTheory.Limits.pair definition

(X Y : C) : Discrete WalkingPair ⥤ C

Full source

/-- The diagram on the walking pair, sending the two points to `X` and `Y`. -/
def pair (X Y : C) : DiscreteDiscrete WalkingPair ⥤ C :=
  Discrete.functor fun j => WalkingPair.casesOn j X Y

Functor representing a pair of objects in a category

Informal description

The functor $\mathrm{pair}\,X\,Y \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to \mathcal{C}$ maps the two objects of the discrete walking pair category to the objects $X$ and $Y$ in the category $\mathcal{C}$. Specifically: - The left object of $\mathrm{WalkingPair}$ is mapped to $X$. - The right object of $\mathrm{WalkingPair}$ is mapped to $Y$. This functor is used to define binary (co)product diagrams in $\mathcal{C}$.

CategoryTheory.Limits.pair_obj_left theorem

(X Y : C) : (pair X Y).obj ⟨left⟩ = X

Full source

@[simp]
theorem pair_obj_left (X Y : C) : (pair X Y).obj ⟨left⟩ = X :=
  rfl

Left Object Mapping in Pair Functor

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$, the functor $\mathrm{pair}\,X\,Y$ maps the left object of the walking pair category to $X$, i.e., $(\mathrm{pair}\,X\,Y)(\mathrm{left}) = X$.

CategoryTheory.Limits.pair_obj_right theorem

(X Y : C) : (pair X Y).obj ⟨right⟩ = Y

Full source

@[simp]
theorem pair_obj_right (X Y : C) : (pair X Y).obj ⟨right⟩ = Y :=
  rfl

Functor Pair Maps Right Object to Y

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$, the functor $\mathrm{pair}\,X\,Y$ maps the right object of the walking pair category to $Y$, i.e., $(\mathrm{pair}\,X\,Y)(\mathrm{right}) = Y$.

CategoryTheory.Limits.mapPair definition

: F ⟶ G

Full source

/-- The natural transformation between two functors out of the
 walking pair, specified by its components. -/
def mapPair : F ⟶ G where
  app
    | ⟨left⟩ => f
    | ⟨right⟩ => g
  naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by aesop_cat

Natural transformation between functors out of the walking pair

Informal description

The natural transformation `mapPair f g` between two functors `F` and `G` out of the walking pair category is defined by its components on the objects of the walking pair. Specifically: - On the left object, it is given by the morphism `f : F.obj left → G.obj left`. - On the right object, it is given by the morphism `g : F.obj right → G.obj right`. This natural transformation satisfies the naturality condition for all morphisms in the walking pair category.

CategoryTheory.Limits.mapPair_left theorem

: (mapPair f g).app ⟨left⟩ = f

Full source

@[simp]
theorem mapPair_left : (mapPair f g).app ⟨left⟩ = f :=
  rfl

Natural transformation component at left object equals $f$

Informal description

For any natural transformation `mapPair f g` between functors $F$ and $G$ from the walking pair category to a category $\mathcal{C}$, the component of the natural transformation at the left object is equal to $f$, i.e., $(\mathrm{mapPair}\,f\,g)_{\langle \mathrm{left} \rangle} = f$.

CategoryTheory.Limits.mapPair_right theorem

: (mapPair f g).app ⟨right⟩ = g

Full source

@[simp]
theorem mapPair_right : (mapPair f g).app ⟨right⟩ = g :=
  rfl

Component of Natural Transformation at Right Object in Walking Pair Category

Informal description

For any natural transformation `mapPair f g` between functors `F` and `G` from the walking pair category, the component of the natural transformation at the right object is equal to the morphism `g : F.obj right → G.obj right`.

CategoryTheory.Limits.mapPairIso definition

(f : F.obj ⟨left⟩ ≅ G.obj ⟨left⟩) (g : F.obj ⟨right⟩ ≅ G.obj ⟨right⟩) : F ≅ G

Full source

/-- The natural isomorphism between two functors out of the walking pair, specified by its
components. -/
@[simps!]
def mapPairIso (f : F.obj ⟨left⟩ ≅ G.obj ⟨left⟩) (g : F.obj ⟨right⟩ ≅ G.obj ⟨right⟩) : F ≅ G :=
  NatIso.ofComponents (fun j ↦ match j with
    | ⟨left⟩ => f
    | ⟨right⟩ => g)
    (fun ⟨⟨u⟩⟩ => by aesop_cat)

Natural isomorphism between functors on the walking pair category

Informal description

Given two functors $ F $ and $ G $ from the walking pair category to a category $ \mathcal{C} $, and given isomorphisms $ f : F(\text{left}) \cong G(\text{left}) $ and $ g : F(\text{right}) \cong G(\text{right}) $, there exists a natural isomorphism $ F \cong G $ whose components at the left and right objects are $ f $ and $ g $ respectively.

CategoryTheory.Limits.diagramIsoPair definition

(F : Discrete WalkingPair ⥤ C) : F ≅ pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)

Full source

/-- Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair` -/
@[simps!]
def diagramIsoPair (F : DiscreteDiscrete WalkingPair ⥤ C) :
    F ≅ pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩) :=
  mapPairIso (Iso.refl _) (Iso.refl _)

Natural isomorphism between a functor and its pair representation

Informal description

For any functor $ F $ from the discrete walking pair category to a category $ \mathcal{C} $, there is a natural isomorphism between $ F $ and the functor $\mathrm{pair}\,(F(\mathrm{left}))\,(F(\mathrm{right}))$, where $\mathrm{left}$ and $\mathrm{right}$ are the two objects of the walking pair category. This isomorphism is constructed using identity isomorphisms at both objects.

CategoryTheory.Limits.pairComp definition

(X Y : C) (F : C ⥤ D) : pair X Y ⋙ F ≅ pair (F.obj X) (F.obj Y)

Full source

/-- The natural isomorphism between `pair X Y ⋙ F` and `pair (F.obj X) (F.obj Y)`. -/
def pairComp (X Y : C) (F : C ⥤ D) : pairpair X Y ⋙ Fpair X Y ⋙ F ≅ pair (F.obj X) (F.obj Y) :=
  diagramIsoPair _

Natural isomorphism between composition of pair functor and pair of functor images

Informal description

For any objects $ X $ and $ Y $ in a category $ \mathcal{C} $ and any functor $ F : \mathcal{C} \to \mathcal{D} $, there is a natural isomorphism between the functor $ \mathrm{pair}\,X\,Y $ composed with $ F $ and the functor $ \mathrm{pair}\,(F(X))\,(F(Y)) $. This isomorphism is constructed using the identity isomorphisms at $ F(X) $ and $ F(Y) $.

CategoryTheory.Limits.BinaryFan abbrev

(X Y : C)

Full source

/-- A binary fan is just a cone on a diagram indexing a product. -/
abbrev BinaryFan (X Y : C) :=
  Cone (pair X Y)

Binary Fan Construction in Category Theory

Informal description

A binary fan for objects $X$ and $Y$ in a category $\mathcal{C}$ is a cone over the diagram consisting of just $X$ and $Y$. Specifically, it consists of: - A cone point $P$ in $\mathcal{C}$ - Two morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ (called the projections)

CategoryTheory.Limits.BinaryFan.fst abbrev

{X Y : C} (s : BinaryFan X Y)

Full source

/-- The first projection of a binary fan. -/
abbrev BinaryFan.fst {X Y : C} (s : BinaryFan X Y) :=
  s.π.app ⟨WalkingPair.left⟩

First Projection of a Binary Fan

Informal description

Given a binary fan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the first projection $\pi_1$ is a morphism from the cone point of $s$ to $X$.

CategoryTheory.Limits.BinaryFan.snd abbrev

{X Y : C} (s : BinaryFan X Y)

Full source

/-- The second projection of a binary fan. -/
abbrev BinaryFan.snd {X Y : C} (s : BinaryFan X Y) :=
  s.π.app ⟨WalkingPair.right⟩

Second Projection of a Binary Fan

Informal description

Given a binary fan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the second projection morphism $s.\mathrm{snd}$ is a morphism from the cone point $P$ of $s$ to $Y$.

CategoryTheory.Limits.BinaryFan.π_app_left theorem

{X Y : C} (s : BinaryFan X Y) : s.π.app ⟨WalkingPair.left⟩ = s.fst

Full source

@[simp]
theorem BinaryFan.π_app_left {X Y : C} (s : BinaryFan X Y) : s.π.app ⟨WalkingPair.left⟩ = s.fst :=
  rfl

Natural transformation component at left object equals first projection in binary fan

Informal description

For any binary fan $s$ over objects $X$ and $Y$ in a category $\mathcal{C}$, the natural transformation component $\pi$ evaluated at the left object of the walking pair equals the first projection morphism $s.\mathrm{fst}$ of the binary fan.

CategoryTheory.Limits.BinaryFan.π_app_right theorem

{X Y : C} (s : BinaryFan X Y) : s.π.app ⟨WalkingPair.right⟩ = s.snd

Full source

@[simp]
theorem BinaryFan.π_app_right {X Y : C} (s : BinaryFan X Y) : s.π.app ⟨WalkingPair.right⟩ = s.snd :=
  rfl

Natural Transformation Component at Right Object Equals Second Projection in Binary Fan

Informal description

For any binary fan $s$ over objects $X$ and $Y$ in a category $\mathcal{C}$, the natural transformation component $\pi$ evaluated at the right object of the walking pair equals the second projection morphism $s.\mathrm{snd}$ of the binary fan.

CategoryTheory.Limits.BinaryFan.ext definition

 {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) :
  c ≅ c'

Full source

/-- Constructs an isomorphism of `BinaryFan`s out of an isomorphism of the tips that commutes with
the projections. -/
def BinaryFan.ext {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt)
    (h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) : c ≅ c' :=
  Cones.ext e (fun j => by rcases j with ⟨⟨⟩⟩ <;> assumption)

Isomorphism of binary fans via cone point isomorphism

Informal description

Given two binary fans $c$ and $c'$ over objects $A$ and $B$ in a category $\mathcal{C}$, an isomorphism $e$ between their cone points, and two commuting conditions: 1. $c.\mathrm{fst} = e.\mathrm{hom} \circ c'.\mathrm{fst}$ 2. $c.\mathrm{snd} = e.\mathrm{hom} \circ c'.\mathrm{snd}$ then there exists an isomorphism between the binary fans $c$ and $c'$ whose underlying morphism is $e.\mathrm{hom}$.

CategoryTheory.Limits.BinaryFan.ext_hom_hom theorem

 {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) :
  (ext e h₁ h₂).hom.hom = e.hom

Full source

@[simp]
lemma BinaryFan.ext_hom_hom {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt)
    (h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) :
    (ext e h₁ h₂).hom.hom = e.hom := rfl

Underlying Morphism of Binary Fan Isomorphism Equals Cone Point Isomorphism

Informal description

Given two binary fans $c$ and $c'$ over objects $A$ and $B$ in a category $\mathcal{C}$, an isomorphism $e$ between their cone points, and two commuting conditions: 1. $c.\mathrm{fst} = e.\mathrm{hom} \circ c'.\mathrm{fst}$ 2. $c.\mathrm{snd} = e.\mathrm{hom} \circ c'.\mathrm{snd}$ then the underlying morphism of the isomorphism between the binary fans $c$ and $c'$ (constructed via `ext`) is equal to $e.\mathrm{hom}$.

CategoryTheory.Limits.BinaryFan.IsLimit.mk definition

 {X Y : C} (s : BinaryFan X Y) (lift : ∀ {T : C} (_ : T ⟶ X) (_ : T ⟶ Y), T ⟶ s.pt)
  (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f)
  (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g)
  (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt) (_ : m ≫ s.fst = f) (_ : m ≫ s.snd = g), m = lift f g) :
  IsLimit s

Full source

/-- A convenient way to show that a binary fan is a limit. -/
def BinaryFan.IsLimit.mk {X Y : C} (s : BinaryFan X Y)
    (lift : ∀ {T : C} (_ : T ⟶ X) (_ : T ⟶ Y), T ⟶ s.pt)
    (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f)
    (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g)
    (uniq :
      ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt) (_ : m ≫ s.fst = f) (_ : m ≫ s.snd = g),
        m = lift f g) :
    IsLimit s :=
  Limits.IsLimit.mk (fun t => lift (BinaryFan.fst t) (BinaryFan.snd t))
    (by
      rintro t (rfl | rfl)
      · exact hl₁ _ _
      · exact hl₂ _ _)
    fun _ _ h => uniq _ _ _ (h ⟨WalkingPair.left⟩) (h ⟨WalkingPair.right⟩)

Construction of a binary fan as a limit cone

Informal description

Given a binary fan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the function `BinaryFan.IsLimit.mk` constructs a proof that $s$ is a limit cone by providing: 1. A lifting function that for any object $T$ and morphisms $f \colon T \to X$, $g \colon T \to Y$ produces a morphism $\mathrm{lift}\,f\,g \colon T \to s.\mathrm{pt}$. 2. Proofs that the lifting function satisfies: - $\mathrm{lift}\,f\,g \circ s.\mathrm{fst} = f$ - $\mathrm{lift}\,f\,g \circ s.\mathrm{snd} = g$ 3. A uniqueness condition stating that any morphism $m \colon T \to s.\mathrm{pt}$ satisfying $m \circ s.\mathrm{fst} = f$ and $m \circ s.\mathrm{snd} = g$ must equal $\mathrm{lift}\,f\,g$. This provides a convenient way to verify that a binary fan is indeed a limit cone.

CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext theorem

 {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) {f g : W ⟶ s.pt} (h₁ : f ≫ s.fst = g ≫ s.fst)
  (h₂ : f ≫ s.snd = g ≫ s.snd) : f = g

Full source

theorem BinaryFan.IsLimit.hom_ext {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) {f g : W ⟶ s.pt}
    (h₁ : f ≫ s.fst = g ≫ s.fst) (h₂ : f ≫ s.snd = g ≫ s.snd) : f = g :=
  h.hom_ext fun j => Discrete.recOn j fun j => WalkingPair.casesOn j h₁ h₂

Uniqueness of Morphisms into Binary Product via Commuting Projections

Informal description

Let $\mathcal{C}$ be a category, $X$ and $Y$ objects in $\mathcal{C}$, and $s$ a binary fan for $X$ and $Y$ that is a limit cone. For any object $W$ in $\mathcal{C}$ and morphisms $f, g : W \to s.pt$, if both $f \circ \pi_1 = g \circ \pi_1$ and $f \circ \pi_2 = g \circ \pi_2$ hold (where $\pi_1$ and $\pi_2$ are the projections of the binary fan), then $f = g$.

CategoryTheory.Limits.BinaryCofan abbrev

(X Y : C)

Full source

/-- A binary cofan is just a cocone on a diagram indexing a coproduct. -/
abbrev BinaryCofan (X Y : C) := Cocone (pair X Y)

Binary Cofan in a Category

Informal description

A binary cofan for objects $X$ and $Y$ in a category $\mathcal{C}$ is a cocone over the diagram consisting of $X$ and $Y$ (represented by the functor $\mathrm{pair}\,X\,Y \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to \mathcal{C}$). Specifically, it consists of: - An object $P$ in $\mathcal{C}$ (the cocone point) - Morphisms $\iota_X \colon X \to P$ and $\iota_Y \colon Y \to P$ (the coprojections)

CategoryTheory.Limits.BinaryCofan.inl abbrev

{X Y : C} (s : BinaryCofan X Y)

Full source

/-- The first inclusion of a binary cofan. -/
abbrev BinaryCofan.inl {X Y : C} (s : BinaryCofan X Y) := s.ι.app ⟨WalkingPair.left⟩

First Coprojection of Binary Cofan

Informal description

Given a binary cofan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the morphism $\iota_X \colon X \to s.pt$ is the first coprojection from $X$ to the cocone point of $s$.

CategoryTheory.Limits.BinaryCofan.inr abbrev

{X Y : C} (s : BinaryCofan X Y)

Full source

/-- The second inclusion of a binary cofan. -/
abbrev BinaryCofan.inr {X Y : C} (s : BinaryCofan X Y) := s.ι.app ⟨WalkingPair.right⟩

Second coprojection of a binary cofan

Informal description

Given a binary cofan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the morphism $\iota_Y \colon Y \to P$ is the second coprojection, where $P$ is the cocone point of $s$.

CategoryTheory.Limits.BinaryCofan.ext definition

 {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) :
  c ≅ c'

Full source

/-- Constructs an isomorphism of `BinaryCofan`s out of an isomorphism of the tips that commutes with
the injections. -/
def BinaryCofan.ext {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt)
    (h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) : c ≅ c' :=
  Cocones.ext e (fun j => by rcases j with ⟨⟨⟩⟩ <;> assumption)

Isomorphism of binary cofans induced by commuting isomorphism of tips

Informal description

Given two binary cofans $c$ and $c'$ for objects $A$ and $B$ in a category $\mathcal{C}$, and an isomorphism $e$ between their cocone points that commutes with the coprojections (i.e., $c.\text{inl} \circ e = c'.\text{inl}$ and $c.\text{inr} \circ e = c'.\text{inr}$), there exists an isomorphism between the cofans $c$ and $c'$ whose underlying morphism is $e$.

CategoryTheory.Limits.BinaryCofan.ext_hom_hom theorem

 {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) :
  (ext e h₁ h₂).hom.hom = e.hom

Full source

@[simp]
lemma BinaryCofan.ext_hom_hom {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt)
    (h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) :
    (ext e h₁ h₂).hom.hom = e.hom := rfl

Underlying Morphism of Binary Cofan Isomorphism Equals Given Isomorphism

Informal description

Given two binary cofans $c$ and $c'$ for objects $A$ and $B$ in a category $\mathcal{C}$, and an isomorphism $e \colon c.pt \cong c'.pt$ between their cocone points that satisfies the commuting conditions $c.inl \circ e.hom = c'.inl$ and $c.inr \circ e.hom = c'.inr$, the underlying morphism of the isomorphism $(ext\,e\,h_1\,h_2).hom$ between the cofans is equal to $e.hom$.

CategoryTheory.Limits.BinaryCofan.ι_app_left theorem

{X Y : C} (s : BinaryCofan X Y) : s.ι.app ⟨WalkingPair.left⟩ = s.inl

Full source

@[simp]
theorem BinaryCofan.ι_app_left {X Y : C} (s : BinaryCofan X Y) :
    s.ι.app ⟨WalkingPair.left⟩ = s.inl := rfl

Coprojection Component at Left Object in Binary Cofan

Informal description

For any binary cofan $s$ of objects $X$ and $Y$ in a category $\mathcal{C}$, the component of the cocone morphism $\iota$ at the left object of the walking pair category is equal to the first coprojection $\iota_X \colon X \to s.pt$.

CategoryTheory.Limits.BinaryCofan.ι_app_right theorem

{X Y : C} (s : BinaryCofan X Y) : s.ι.app ⟨WalkingPair.right⟩ = s.inr

Full source

@[simp]
theorem BinaryCofan.ι_app_right {X Y : C} (s : BinaryCofan X Y) :
    s.ι.app ⟨WalkingPair.right⟩ = s.inr := rfl

Natural Transformation Component Equals Second Coprojection in Binary Cofan

Informal description

For any binary cofan $s$ of objects $X$ and $Y$ in a category $\mathcal{C}$, the natural transformation $\iota$ evaluated at the right object of the walking pair category equals the second coprojection morphism $s.\mathrm{inr} : Y \to s.\mathrm{pt}$.

CategoryTheory.Limits.BinaryCofan.IsColimit.mk definition

 {X Y : C} (s : BinaryCofan X Y) (desc : ∀ {T : C} (_ : X ⟶ T) (_ : Y ⟶ T), s.pt ⟶ T)
  (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f)
  (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g)
  (uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T) (_ : s.inl ≫ m = f) (_ : s.inr ≫ m = g), m = desc f g) :
  IsColimit s

Full source

/-- A convenient way to show that a binary cofan is a colimit. -/
def BinaryCofan.IsColimit.mk {X Y : C} (s : BinaryCofan X Y)
    (desc : ∀ {T : C} (_ : X ⟶ T) (_ : Y ⟶ T), s.pt ⟶ T)
    (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f)
    (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g)
    (uniq :
      ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T) (_ : s.inl ≫ m = f) (_ : s.inr ≫ m = g),
        m = desc f g) :
    IsColimit s :=
  Limits.IsColimit.mk (fun t => desc (BinaryCofan.inl t) (BinaryCofan.inr t))
    (by
      rintro t (rfl | rfl)
      · exact hd₁ _ _
      · exact hd₂ _ _)
    fun _ _ h => uniq _ _ _ (h ⟨WalkingPair.left⟩) (h ⟨WalkingPair.right⟩)

Construction of a binary cofan colimit

Informal description

Given a binary cofan $ s $ for objects $ X $ and $ Y $ in a category $ \mathcal{C} $, to show that $ s $ is a colimit cocone, it suffices to provide: 1. A *descending morphism* construction: For any object $ T $ and morphisms $ f \colon X \to T $ and $ g \colon Y \to T $, a morphism $ \mathrm{desc}\,f\,g \colon s.\mathrm{pt} \to T $. 2. Proof that the descending morphism satisfies: - $ \iota_X \circ \mathrm{desc}\,f\,g = f $ (left coprojection condition) - $ \iota_Y \circ \mathrm{desc}\,f\,g = g $ (right coprojection condition) 3. Uniqueness: Any morphism $ m \colon s.\mathrm{pt} \to T $ satisfying $ \iota_X \circ m = f $ and $ \iota_Y \circ m = g $ must equal $ \mathrm{desc}\,f\,g $.

CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext theorem

 {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) {f g : s.pt ⟶ W} (h₁ : s.inl ≫ f = s.inl ≫ g)
  (h₂ : s.inr ≫ f = s.inr ≫ g) : f = g

Full source

theorem BinaryCofan.IsColimit.hom_ext {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s)
    {f g : s.pt ⟶ W} (h₁ : s.inl ≫ f = s.inl ≫ g) (h₂ : s.inr ≫ f = s.inr ≫ g) : f = g :=
  h.hom_ext fun j => Discrete.recOn j fun j => WalkingPair.casesOn j h₁ h₂

Uniqueness of Morphisms from Binary Coproduct via Commuting Coprojections

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y \in \mathcal{C}$. Given a binary cofan $s$ for $X$ and $Y$ with cocone point $P$, and a proof $h$ that $s$ is a colimit cocone, then for any object $W \in \mathcal{C}$ and any two morphisms $f, g : P \to W$, if both coprojections $\iota_X : X \to P$ and $\iota_Y : Y \to P$ satisfy $\iota_X \circ f = \iota_X \circ g$ and $\iota_Y \circ f = \iota_Y \circ g$, then $f = g$.

CategoryTheory.Limits.BinaryFan.mk definition

{P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : BinaryFan X Y

Full source

/-- A binary fan with vertex `P` consists of the two projections `π₁ : P ⟶ X` and `π₂ : P ⟶ Y`. -/
@[simps pt]
def BinaryFan.mk {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : BinaryFan X Y where
  pt := P
  π := { app := fun | { as := j } => match j with | left => π₁ | right => π₂ }

Binary fan construction

Informal description

Given a category $\mathcal{C}$ and objects $X, Y \in \mathcal{C}$, a binary fan for $X$ and $Y$ consists of: - An object $P \in \mathcal{C}$ (called the vertex) - Two morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ (called the projections) The constructor `BinaryFan.mk` takes these projections and constructs the corresponding binary fan.

CategoryTheory.Limits.BinaryCofan.mk definition

{P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : BinaryCofan X Y

Full source

/-- A binary cofan with vertex `P` consists of the two inclusions `ι₁ : X ⟶ P` and `ι₂ : Y ⟶ P`. -/
@[simps pt]
def BinaryCofan.mk {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : BinaryCofan X Y where
  pt := P
  ι := { app := fun | { as := j } => match j with | left => ι₁ | right => ι₂ }

Binary cofan construction from coprojections

Informal description

Given two morphisms $\iota_1 \colon X \to P$ and $\iota_2 \colon Y \to P$ in a category $\mathcal{C}$, the binary cofan $\mathrm{BinaryCofan.mk}\,\iota_1\,\iota_2$ consists of: - An object $P$ (the vertex of the cofan) - The two morphisms $\iota_1$ and $\iota_2$ (the coprojections from $X$ and $Y$ respectively)

CategoryTheory.Limits.BinaryFan.mk_fst theorem

{P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (BinaryFan.mk π₁ π₂).fst = π₁

Full source

@[simp]
theorem BinaryFan.mk_fst {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (BinaryFan.mk π₁ π₂).fst = π₁ :=
  rfl

First Projection of Constructed Binary Fan Equals Given Morphism

Informal description

Given a category $\mathcal{C}$, objects $X, Y \in \mathcal{C}$, and morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ from some object $P \in \mathcal{C}$, the first projection of the binary fan constructed from $\pi_1$ and $\pi_2$ equals $\pi_1$. That is, $(\mathrm{BinaryFan.mk}\,\pi_1\,\pi_2).\mathrm{fst} = \pi_1$.

CategoryTheory.Limits.BinaryFan.mk_snd theorem

{P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (BinaryFan.mk π₁ π₂).snd = π₂

Full source

@[simp]
theorem BinaryFan.mk_snd {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (BinaryFan.mk π₁ π₂).snd = π₂ :=
  rfl

Second Projection of Constructed Binary Fan Equals Input Morphism

Informal description

For any object $P$ in a category $\mathcal{C}$ and morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$, the second projection of the binary fan constructed from $\pi_1$ and $\pi_2$ equals $\pi_2$. That is, $(\mathrm{BinaryFan.mk}\,\pi_1\,\pi_2).\mathrm{snd} = \pi_2$.

CategoryTheory.Limits.BinaryCofan.mk_inl theorem

{P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (BinaryCofan.mk ι₁ ι₂).inl = ι₁

Full source

@[simp]
theorem BinaryCofan.mk_inl {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (BinaryCofan.mk ι₁ ι₂).inl = ι₁ :=
  rfl

First coprojection of constructed binary cofan equals input morphism

Informal description

Given two morphisms $\iota_1 \colon X \to P$ and $\iota_2 \colon Y \to P$ in a category $\mathcal{C}$, the first coprojection of the binary cofan constructed from $\iota_1$ and $\iota_2$ equals $\iota_1$. That is, $(\mathrm{BinaryCofan.mk}\,\iota_1\,\iota_2).\mathrm{inl} = \iota_1$.

CategoryTheory.Limits.BinaryCofan.mk_inr theorem

{P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (BinaryCofan.mk ι₁ ι₂).inr = ι₂

Full source

@[simp]
theorem BinaryCofan.mk_inr {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (BinaryCofan.mk ι₁ ι₂).inr = ι₂ :=
  rfl

Second Coprojection of Constructed Binary Cofan Equals Input Morphism

Informal description

Given two morphisms $\iota_1 \colon X \to P$ and $\iota_2 \colon Y \to P$ in a category $\mathcal{C}$, the second coprojection of the binary cofan constructed from $\iota_1$ and $\iota_2$ equals $\iota_2$. That is, $(\mathrm{BinaryCofan.mk}\,\iota_1\,\iota_2).\mathrm{inr} = \iota_2$.

CategoryTheory.Limits.isoBinaryFanMk definition

{X Y : C} (c : BinaryFan X Y) : c ≅ BinaryFan.mk c.fst c.snd

Full source

/-- Every `BinaryFan` is isomorphic to an application of `BinaryFan.mk`. -/
def isoBinaryFanMk {X Y : C} (c : BinaryFan X Y) : c ≅ BinaryFan.mk c.fst c.snd :=
    Cones.ext (Iso.refl _) fun ⟨l⟩ => by cases l; repeat simp

Isomorphism between a binary fan and its reconstruction from projections

Informal description

For any binary fan $c$ of objects $X$ and $Y$ in a category $\mathcal{C}$, there is an isomorphism between $c$ and the binary fan constructed from its own projections $\pi_1$ and $\pi_2$.

CategoryTheory.Limits.isoBinaryCofanMk definition

{X Y : C} (c : BinaryCofan X Y) : c ≅ BinaryCofan.mk c.inl c.inr

Full source

/-- Every `BinaryFan` is isomorphic to an application of `BinaryFan.mk`. -/
def isoBinaryCofanMk {X Y : C} (c : BinaryCofan X Y) : c ≅ BinaryCofan.mk c.inl c.inr :=
    Cocones.ext (Iso.refl _) fun ⟨l⟩ => by cases l; repeat simp

Isomorphism between a binary cofan and its canonical construction

Informal description

For any binary cofan $c$ of objects $X$ and $Y$ in a category $\mathcal{C}$, there is an isomorphism between $c$ and the binary cofan constructed from its coprojections $\mathrm{BinaryCofan.mk}\,c.\mathrm{inl}\,c.\mathrm{inr}$.

CategoryTheory.Limits.BinaryFan.isLimitMk definition

 {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : ∀ s : BinaryFan X Y, s.pt ⟶ W)
  (fac_left : ∀ s : BinaryFan X Y, lift s ≫ fst = s.fst) (fac_right : ∀ s : BinaryFan X Y, lift s ≫ snd = s.snd)
  (uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W) (_ : m ≫ fst = s.fst) (_ : m ≫ snd = s.snd), m = lift s) :
  IsLimit (BinaryFan.mk fst snd)

Full source

/-- This is a more convenient formulation to show that a `BinaryFan` constructed using
`BinaryFan.mk` is a limit cone.
-/
def BinaryFan.isLimitMk {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : ∀ s : BinaryFan X Y, s.pt ⟶ W)
    (fac_left : ∀ s : BinaryFan X Y, lift s ≫ fst = s.fst)
    (fac_right : ∀ s : BinaryFan X Y, lift s ≫ snd = s.snd)
    (uniq :
      ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W) (_ : m ≫ fst = s.fst) (_ : m ≫ snd = s.snd),
        m = lift s) :
    IsLimit (BinaryFan.mk fst snd) :=
  { lift := lift
    fac := fun s j => by
      rcases j with ⟨⟨⟩⟩
      exacts [fac_left s, fac_right s]
    uniq := fun s m w => uniq s m (w ⟨WalkingPair.left⟩) (w ⟨WalkingPair.right⟩) }

Criterion for binary fan to be a limit cone

Informal description

Given a category $\mathcal{C}$ and objects $X, Y \in \mathcal{C}$, suppose we have: - An object $W \in \mathcal{C}$ with morphisms $fst \colon W \to X$ and $snd \colon W \to Y$ - A lifting function $lift$ that for any binary fan $s$ of $X$ and $Y$ produces a morphism $s.pt \to W$ - Proofs that $lift$ satisfies the left and right factor conditions: $lift(s) \circ fst = s.fst$ and $lift(s) \circ snd = s.snd$ for all $s$ - A uniqueness condition stating that any morphism $m \colon s.pt \to W$ satisfying $m \circ fst = s.fst$ and $m \circ snd = s.snd$ must equal $lift(s)$ Then the binary fan constructed from $fst$ and $snd$ is a limit cone.

CategoryTheory.Limits.BinaryCofan.isColimitMk definition

 {W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : ∀ s : BinaryCofan X Y, W ⟶ s.pt)
  (fac_left : ∀ s : BinaryCofan X Y, inl ≫ desc s = s.inl) (fac_right : ∀ s : BinaryCofan X Y, inr ≫ desc s = s.inr)
  (uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt) (_ : inl ≫ m = s.inl) (_ : inr ≫ m = s.inr), m = desc s) :
  IsColimit (BinaryCofan.mk inl inr)

Full source

/-- This is a more convenient formulation to show that a `BinaryCofan` constructed using
`BinaryCofan.mk` is a colimit cocone.
-/
def BinaryCofan.isColimitMk {W : C} {inl : X ⟶ W} {inr : Y ⟶ W}
    (desc : ∀ s : BinaryCofan X Y, W ⟶ s.pt)
    (fac_left : ∀ s : BinaryCofan X Y, inl ≫ desc s = s.inl)
    (fac_right : ∀ s : BinaryCofan X Y, inr ≫ desc s = s.inr)
    (uniq :
      ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt) (_ : inl ≫ m = s.inl) (_ : inr ≫ m = s.inr),
        m = desc s) :
    IsColimit (BinaryCofan.mk inl inr) :=
  { desc := desc
    fac := fun s j => by
      rcases j with ⟨⟨⟩⟩
      exacts [fac_left s, fac_right s]
    uniq := fun s m w => uniq s m (w ⟨WalkingPair.left⟩) (w ⟨WalkingPair.right⟩) }

Colimit condition for binary cofan

Informal description

Given a binary cofan $(W, \iota_X \colon X \to W, \iota_Y \colon Y \to W)$ in a category $\mathcal{C}$, the cofan is a colimit cocone if there exists a unique morphism $\mathrm{desc}(s) \colon W \to s.pt$ for every binary cofan $s$ of $X$ and $Y$, satisfying: 1. $\iota_X \circ \mathrm{desc}(s) = s.\iota_X$ (left factorization) 2. $\iota_Y \circ \mathrm{desc}(s) = s.\iota_Y$ (right factorization) 3. For any morphism $m \colon W \to s.pt$ satisfying $\iota_X \circ m = s.\iota_X$ and $\iota_Y \circ m = s.\iota_Y$, we have $m = \mathrm{desc}(s)$ (uniqueness).

CategoryTheory.Limits.BinaryFan.IsLimit.lift' definition

 {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) :
  { l : W ⟶ s.pt // l ≫ s.fst = f ∧ l ≫ s.snd = g }

Full source

/-- If `s` is a limit binary fan over `X` and `Y`, then every pair of morphisms `f : W ⟶ X` and
`g : W ⟶ Y` induces a morphism `l : W ⟶ s.pt` satisfying `l ≫ s.fst = f` and `l ≫ s.snd = g`.
-/
@[simps]
def BinaryFan.IsLimit.lift' {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X)
    (g : W ⟶ Y) : { l : W ⟶ s.pt // l ≫ s.fst = f ∧ l ≫ s.snd = g } :=
  ⟨h.lift <| BinaryFan.mk f g, h.fac _ _, h.fac _ _⟩

Universal property of binary product cone

Informal description

Given a binary fan $s$ for objects $X$ and $Y$ in a category $\mathcal{C}$ that is a limit cone, and given morphisms $f \colon W \to X$ and $g \colon W \to Y$, there exists a unique morphism $l \colon W \to s.\mathrm{pt}$ such that $l \circ \pi_1 = f$ and $l \circ \pi_2 = g$, where $\pi_1$ and $\pi_2$ are the projections of the binary fan $s$.

CategoryTheory.Limits.BinaryCofan.IsColimit.desc' definition

 {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) :
  { l : s.pt ⟶ W // s.inl ≫ l = f ∧ s.inr ≫ l = g }

Full source

/-- If `s` is a colimit binary cofan over `X` and `Y`,, then every pair of morphisms `f : X ⟶ W` and
`g : Y ⟶ W` induces a morphism `l : s.pt ⟶ W` satisfying `s.inl ≫ l = f` and `s.inr ≫ l = g`.
-/
@[simps]
def BinaryCofan.IsColimit.desc' {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W)
    (g : Y ⟶ W) : { l : s.pt ⟶ W // s.inl ≫ l = f ∧ s.inr ≫ l = g } :=
  ⟨h.desc <| BinaryCofan.mk f g, h.fac _ _, h.fac _ _⟩

Universal property of a colimit binary cofan

Informal description

Given a colimit binary cofan $ s $ for objects $ X $ and $ Y $ in a category $ \mathcal{C} $, and morphisms $ f \colon X \to W $ and $ g \colon Y \to W $, there exists a unique morphism $ l \colon s.pt \to W $ such that the compositions $ \iota_X \circ l = f $ and $ \iota_Y \circ l = g $, where $ \iota_X $ and $ \iota_Y $ are the coprojections of the cofan $ s $.

CategoryTheory.Limits.BinaryFan.isLimitFlip definition

{X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) : IsLimit (BinaryFan.mk c.snd c.fst)

Full source

/-- Binary products are symmetric. -/
def BinaryFan.isLimitFlip {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) :
    IsLimit (BinaryFan.mk c.snd c.fst) :=
  BinaryFan.isLimitMk (fun s => hc.lift (BinaryFan.mk s.snd s.fst)) (fun _ => hc.fac _ _)
    (fun _ => hc.fac _ _) fun s _ e₁ e₂ =>
    BinaryFan.IsLimit.hom_ext hc
      (e₂.trans (hc.fac (BinaryFan.mk s.snd s.fst) ⟨WalkingPair.left⟩).symm)
      (e₁.trans (hc.fac (BinaryFan.mk s.snd s.fst) ⟨WalkingPair.right⟩).symm)

Symmetry of binary product limits

Informal description

Given a binary fan $c$ for objects $X$ and $Y$ in a category $\mathcal{C}$, if $c$ is a limit cone, then the binary fan obtained by swapping its projections (i.e., using $c.\mathrm{snd}$ as the first projection and $c.\mathrm{fst}$ as the second projection) is also a limit cone.

CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst theorem

{X Y : C} (h : IsTerminal Y) (c : BinaryFan X Y) : Nonempty (IsLimit c) ↔ IsIso c.fst

Full source

theorem BinaryFan.isLimit_iff_isIso_fst {X Y : C} (h : IsTerminal Y) (c : BinaryFan X Y) :
    NonemptyNonempty (IsLimit c) ↔ IsIso c.fst := by
  constructor
  · rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
    exact
      ⟨⟨l,
          BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
            (h.hom_ext _ _),
          hl⟩⟩
  · intro
    exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩

Characterization of Binary Product via Isomorphism of First Projection to Terminal Object

Informal description

Let $\mathcal{C}$ be a category, $Y$ a terminal object in $\mathcal{C}$, and $c$ a binary fan for objects $X$ and $Y$. Then the following are equivalent: 1. The binary fan $c$ is a limit cone (up to isomorphism). 2. The first projection morphism $c.\mathrm{fst} : c.\mathrm{pt} \to X$ is an isomorphism.

CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd theorem

{X Y : C} (h : IsTerminal X) (c : BinaryFan X Y) : Nonempty (IsLimit c) ↔ IsIso c.snd

Full source

theorem BinaryFan.isLimit_iff_isIso_snd {X Y : C} (h : IsTerminal X) (c : BinaryFan X Y) :
    NonemptyNonempty (IsLimit c) ↔ IsIso c.snd := by
  refine Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))
  exact
    ⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
      ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩

Characterization of Binary Product via Isomorphism of Second Projection to Terminal Object

Informal description

Let $\mathcal{C}$ be a category with $X$ a terminal object, and let $c$ be a binary fan for objects $X$ and $Y$ in $\mathcal{C}$. Then the following are equivalent: 1. The binary fan $c$ is a limit cone (up to isomorphism). 2. The second projection morphism $c.\mathrm{snd} : c.\mathrm{pt} \to Y$ is an isomorphism.

CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso definition

{X Y X' : C} (c : BinaryFan X Y) (f : X ⟶ X') [IsIso f] (h : IsLimit c) : IsLimit (BinaryFan.mk (c.fst ≫ f) c.snd)

Full source

/-- If `X' ≅ X`, then `X × Y` also is the product of `X'` and `Y`. -/
noncomputable def BinaryFan.isLimitCompLeftIso {X Y X' : C} (c : BinaryFan X Y) (f : X ⟶ X')
    [IsIso f] (h : IsLimit c) : IsLimit (BinaryFan.mk (c.fst ≫ f) c.snd) := by
  fapply BinaryFan.isLimitMk
  · exact fun s => h.lift (BinaryFan.mk (s.fst ≫ inv f) s.snd)
  · intro s -- Porting note: simp timed out here
    simp only [Category.comp_id,BinaryFan.π_app_left,IsIso.inv_hom_id,
      BinaryFan.mk_fst,IsLimit.fac_assoc,eq_self_iff_true,Category.assoc]
  · intro s -- Porting note: simp timed out here
    simp only [BinaryFan.π_app_right,BinaryFan.mk_snd,eq_self_iff_true,IsLimit.fac]
  · intro s m e₁ e₂
     -- Porting note: simpa timed out here also
    apply BinaryFan.IsLimit.hom_ext h
    · simpa only
      [BinaryFan.π_app_left,BinaryFan.mk_fst,Category.assoc,IsLimit.fac,IsIso.eq_comp_inv]
    · simpa only [BinaryFan.π_app_right,BinaryFan.mk_snd,IsLimit.fac]

Limit cone preservation under isomorphism of first component

Informal description

Given a category $\mathcal{C}$ and objects $X, Y, X' \in \mathcal{C}$, let $c$ be a binary fan for $X$ and $Y$ with projections $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$. If $f \colon X \to X'$ is an isomorphism and $c$ is a limit cone, then the binary fan formed by the compositions $\pi_1 \circ f \colon P \to X'$ and $\pi_2 \colon P \to Y$ is also a limit cone.

CategoryTheory.Limits.BinaryFan.isLimitCompRightIso definition

{X Y Y' : C} (c : BinaryFan X Y) (f : Y ⟶ Y') [IsIso f] (h : IsLimit c) : IsLimit (BinaryFan.mk c.fst (c.snd ≫ f))

Full source

/-- If `Y' ≅ Y`, then `X x Y` also is the product of `X` and `Y'`. -/
noncomputable def BinaryFan.isLimitCompRightIso {X Y Y' : C} (c : BinaryFan X Y) (f : Y ⟶ Y')
    [IsIso f] (h : IsLimit c) : IsLimit (BinaryFan.mk c.fst (c.snd ≫ f)) :=
  BinaryFan.isLimitFlip <| BinaryFan.isLimitCompLeftIso _ f (BinaryFan.isLimitFlip h)

Limit cone preservation under isomorphism of second component

Informal description

Given a category $\mathcal{C}$ and objects $X, Y, Y' \in \mathcal{C}$, let $c$ be a binary fan for $X$ and $Y$ with projections $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$. If $f \colon Y \to Y'$ is an isomorphism and $c$ is a limit cone, then the binary fan formed by the projections $\pi_1 \colon P \to X$ and $\pi_2 \circ f \colon P \to Y'$ is also a limit cone.

CategoryTheory.Limits.BinaryCofan.isColimitFlip definition

{X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) : IsColimit (BinaryCofan.mk c.inr c.inl)

Full source

/-- Binary coproducts are symmetric. -/
def BinaryCofan.isColimitFlip {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) :
    IsColimit (BinaryCofan.mk c.inr c.inl) :=
  BinaryCofan.isColimitMk (fun s => hc.desc (BinaryCofan.mk s.inr s.inl)) (fun _ => hc.fac _ _)
    (fun _ => hc.fac _ _) fun s _ e₁ e₂ =>
    BinaryCofan.IsColimit.hom_ext hc
      (e₂.trans (hc.fac (BinaryCofan.mk s.inr s.inl) ⟨WalkingPair.left⟩).symm)
      (e₁.trans (hc.fac (BinaryCofan.mk s.inr s.inl) ⟨WalkingPair.right⟩).symm)

Symmetry of binary coproducts

Informal description

Given a binary cofan $ c $ for objects $ X $ and $ Y $ in a category $ \mathcal{C} $, if $ c $ is a colimit cocone, then the cofan obtained by swapping the coprojections $ c.\iota_X $ and $ c.\iota_Y $ is also a colimit cocone. In other words, binary coproducts are symmetric.

CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl theorem

{X Y : C} (h : IsInitial Y) (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ IsIso c.inl

Full source

theorem BinaryCofan.isColimit_iff_isIso_inl {X Y : C} (h : IsInitial Y) (c : BinaryCofan X Y) :
    NonemptyNonempty (IsColimit c) ↔ IsIso c.inl := by
  constructor
  · rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
    refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
    rw [Category.comp_id]
    have e : (inl c ≫ l) ≫ inl c = 𝟙𝟙 X ≫ inl c := congrArg (·≫inl c) hl
    rwa [Category.assoc,Category.id_comp] at e
  · intro
    exact
      ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
          (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
          (IsIso.eq_inv_comp _).mpr e⟩

Characterization of Binary Cofan Colimit via Isomorphism of First Coprojection when Second Object is Initial

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y$ be objects in $\mathcal{C}$. If $Y$ is an initial object, then for any binary cofan $c$ of $X$ and $Y$, the following are equivalent: 1. There exists a colimit structure on $c$. 2. The coprojection $\iota_X : X \to c.pt$ is an isomorphism.

CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr theorem

{X Y : C} (h : IsInitial X) (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ IsIso c.inr

Full source

theorem BinaryCofan.isColimit_iff_isIso_inr {X Y : C} (h : IsInitial X) (c : BinaryCofan X Y) :
    NonemptyNonempty (IsColimit c) ↔ IsIso c.inr := by
  refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
  exact
    ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

Characterization of Binary Cofan Colimit via Isomorphism of Second Coprojection when First Object is Initial

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y$ be objects in $\mathcal{C}$. If $X$ is an initial object, then for any binary cofan $c$ of $X$ and $Y$, the following are equivalent: 1. There exists a colimit structure on $c$. 2. The coprojection $\iota_Y : Y \to c.pt$ is an isomorphism.

CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso definition

 {X Y X' : C} (c : BinaryCofan X Y) (f : X' ⟶ X) [IsIso f] (h : IsColimit c) :
  IsColimit (BinaryCofan.mk (f ≫ c.inl) c.inr)

Full source

/-- If `X' ≅ X`, then `X ⨿ Y` also is the coproduct of `X'` and `Y`. -/
noncomputable def BinaryCofan.isColimitCompLeftIso {X Y X' : C} (c : BinaryCofan X Y) (f : X' ⟶ X)
    [IsIso f] (h : IsColimit c) : IsColimit (BinaryCofan.mk (f ≫ c.inl) c.inr) := by
  fapply BinaryCofan.isColimitMk
  · exact fun s => h.desc (BinaryCofan.mk (invinv f ≫ s.inl) s.inr)
  · intro s
    -- Porting note: simp timed out here too
    simp only [IsColimit.fac,BinaryCofan.ι_app_left,eq_self_iff_true,
      Category.assoc,BinaryCofan.mk_inl,IsIso.hom_inv_id_assoc]
  · intro s
    -- Porting note: simp timed out here too
    simp only [IsColimit.fac,BinaryCofan.ι_app_right,eq_self_iff_true,BinaryCofan.mk_inr]
  · intro s m e₁ e₂
    apply BinaryCofan.IsColimit.hom_ext h
    · rw [← cancel_epi f]
    -- Porting note: simp timed out here too
      simpa only [IsColimit.fac,BinaryCofan.ι_app_left,eq_self_iff_true,
      Category.assoc,BinaryCofan.mk_inl,IsIso.hom_inv_id_assoc] using e₁
    -- Porting note: simp timed out here too
    · simpa only [IsColimit.fac,BinaryCofan.ι_app_right,eq_self_iff_true,BinaryCofan.mk_inr]

Colimit preservation under isomorphism of first coprojection

Informal description

Given a binary cofan $ c $ for objects $ X $ and $ Y $ in a category $ \mathcal{C} $, and an isomorphism $ f : X' \to X $, if $ c $ is a colimit cocone, then the modified binary cofan $ \mathrm{BinaryCofan.mk}\,(f \circ c.\iota_X)\,c.\iota_Y $ is also a colimit cocone. In other words, if $ c $ is a colimit for the original pair $ X $ and $ Y $, then replacing the first coprojection $ \iota_X $ with $ f \circ \iota_X $ (where $ f $ is an isomorphism) still yields a colimit cocone.

CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso definition

 {X Y Y' : C} (c : BinaryCofan X Y) (f : Y' ⟶ Y) [IsIso f] (h : IsColimit c) :
  IsColimit (BinaryCofan.mk c.inl (f ≫ c.inr))

Full source

/-- If `Y' ≅ Y`, then `X ⨿ Y` also is the coproduct of `X` and `Y'`. -/
noncomputable def BinaryCofan.isColimitCompRightIso {X Y Y' : C} (c : BinaryCofan X Y) (f : Y' ⟶ Y)
    [IsIso f] (h : IsColimit c) : IsColimit (BinaryCofan.mk c.inl (f ≫ c.inr)) :=
  BinaryCofan.isColimitFlip <| BinaryCofan.isColimitCompLeftIso _ f (BinaryCofan.isColimitFlip h)

Colimit preservation under isomorphism of second coprojection

Informal description

Given a binary cofan $ c $ for objects $ X $ and $ Y $ in a category $ \mathcal{C} $, and an isomorphism $ f : Y' \to Y $, if $ c $ is a colimit cocone, then the modified binary cofan $ \mathrm{BinaryCofan.mk}\,c.\iota_X\,(f \circ c.\iota_Y) $ is also a colimit cocone. In other words, if $ c $ is a colimit for the original pair $ X $ and $ Y $, then replacing the second coprojection $ \iota_Y $ with $ f \circ \iota_Y $ (where $ f $ is an isomorphism) still yields a colimit cocone.

CategoryTheory.Limits.HasBinaryProduct abbrev

(X Y : C)

Full source

/-- An abbreviation for `HasLimit (pair X Y)`. -/
abbrev HasBinaryProduct (X Y : C) :=
  HasLimit (pair X Y)

Existence of Binary Product in a Category

Informal description

For objects $X$ and $Y$ in a category $\mathcal{C}$, the abbreviation $\mathrm{HasBinaryProduct}\,X\,Y$ asserts the existence of a limit for the functor $\mathrm{pair}\,X\,Y \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to \mathcal{C}$. This means there exists a binary product of $X$ and $Y$ in $\mathcal{C}$.

CategoryTheory.Limits.HasBinaryCoproduct abbrev

(X Y : C)

Full source

/-- An abbreviation for `HasColimit (pair X Y)`. -/
abbrev HasBinaryCoproduct (X Y : C) :=
  HasColimit (pair X Y)

Existence of Binary Coproducts in a Category

Informal description

A category $\mathcal{C}$ is said to have binary coproducts for objects $X$ and $Y$ if there exists a colimit for the functor $\mathrm{pair}\,X\,Y \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to \mathcal{C}$, where $\mathrm{WalkingPair}$ is the indexing category with two objects (representing the left and right components of the coproduct).

CategoryTheory.Limits.prod abbrev

(X Y : C) [HasBinaryProduct X Y]

Full source

/-- If we have a product of `X` and `Y`, we can access it using `prod X Y` or
    `X ⨯ Y`. -/
noncomputable abbrev prod (X Y : C) [HasBinaryProduct X Y] :=
  limit (pair X Y)

Binary product in a category

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary products, the product of $X$ and $Y$ is denoted by $\mathrm{prod}\,X\,Y$ or $X \times Y$. This is the limit of the functor $\mathrm{pair}\,X\,Y \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to \mathcal{C}$, where $\mathrm{WalkingPair}$ is the indexing category with two objects representing the left and right components of the product.

CategoryTheory.Limits.coprod abbrev

(X Y : C) [HasBinaryCoproduct X Y]

Full source

/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y` or
    `X ⨿ Y`. -/
noncomputable abbrev coprod (X Y : C) [HasBinaryCoproduct X Y] :=
  colimit (pair X Y)

Binary coproduct in a category

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary coproducts, the coproduct of $X$ and $Y$ is denoted by $\mathrm{coprod}\,X\,Y$ or $X \sqcup Y$.

CategoryTheory.Limits.term_⨯_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for the product -/
notation:20 X " ⨯ " Y:20 => prod X Y

Categorical product notation

Informal description

The notation $ X \times Y $ denotes the categorical product of objects $ X $ and $ Y $ in a category $ \mathcal{C} $.

CategoryTheory.Limits.term_⨿_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for the coproduct -/
notation:20 X " ⨿ " Y:20 => coprod X Y

Coproduct notation

Informal description

The notation $ X \amalg Y $ is defined as the coproduct of $ X $ and $ Y $.

CategoryTheory.Limits.prod.fst abbrev

{X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ X

Full source

/-- The projection map to the first component of the product. -/
noncomputable abbrev prod.fst {X Y : C} [HasBinaryProduct X Y] : X ⨯ YX ⨯ Y ⟶ X :=
  limit.π (pair X Y) ⟨WalkingPair.left⟩

First Projection Morphism from Binary Product

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary products, there exists a projection morphism $\pi_1: X \times Y \to X$ from the product object to the first component $X$.

CategoryTheory.Limits.prod.snd abbrev

{X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ Y

Full source

/-- The projection map to the second component of the product. -/
noncomputable abbrev prod.snd {X Y : C} [HasBinaryProduct X Y] : X ⨯ YX ⨯ Y ⟶ Y :=
  limit.π (pair X Y) ⟨WalkingPair.right⟩

Second projection morphism from binary product

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary products, the second projection morphism $\mathrm{snd} \colon X \times Y \to Y$ is the canonical morphism from the product object to $Y$.

CategoryTheory.Limits.coprod.inl abbrev

{X Y : C} [HasBinaryCoproduct X Y] : X ⟶ X ⨿ Y

Full source

/-- The inclusion map from the first component of the coproduct. -/
noncomputable abbrev coprod.inl {X Y : C} [HasBinaryCoproduct X Y] : X ⟶ X ⨿ Y :=
  colimit.ι (pair X Y) ⟨WalkingPair.left⟩

Left Inclusion Map into Coproduct

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary coproducts, the inclusion map $\mathrm{inl} \colon X \to X \sqcup Y$ is the canonical morphism from $X$ to the coproduct $X \sqcup Y$.

CategoryTheory.Limits.coprod.inr abbrev

{X Y : C} [HasBinaryCoproduct X Y] : Y ⟶ X ⨿ Y

Full source

/-- The inclusion map from the second component of the coproduct. -/
noncomputable abbrev coprod.inr {X Y : C} [HasBinaryCoproduct X Y] : Y ⟶ X ⨿ Y :=
  colimit.ι (pair X Y) ⟨WalkingPair.right⟩

Right Inclusion into Binary Coproduct

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$ with binary coproducts, the morphism $\mathrm{coprod.inr} : Y \to X \sqcup Y$ is the canonical inclusion of $Y$ into the coproduct $X \sqcup Y$.

CategoryTheory.Limits.prodIsProd definition

(X Y : C) [HasBinaryProduct X Y] : IsLimit (BinaryFan.mk (prod.fst : X ⨯ Y ⟶ X) prod.snd)

Full source

/-- The binary fan constructed from the projection maps is a limit. -/
noncomputable def prodIsProd (X Y : C) [HasBinaryProduct X Y] :
    IsLimit (BinaryFan.mk (prod.fst : X ⨯ YX ⨯ Y ⟶ X) prod.snd) :=
  (limit.isLimit _).ofIsoLimit (Cones.ext (Iso.refl _) (fun ⟨u⟩ => by
    cases u
    · dsimp; simp only [Category.id_comp]; rfl
    · dsimp; simp only [Category.id_comp]; rfl
  ))

Product object is a limit cone

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary products, the binary fan formed by the projection maps $\pi_1: X \times Y \to X$ and $\pi_2: X \times Y \to Y$ is a limit cone. This means the product object $X \times Y$ together with these projections satisfies the universal property of a product.

CategoryTheory.Limits.coprodIsCoprod definition

(X Y : C) [HasBinaryCoproduct X Y] : IsColimit (BinaryCofan.mk (coprod.inl : X ⟶ X ⨿ Y) coprod.inr)

Full source

/-- The binary cofan constructed from the coprojection maps is a colimit. -/
noncomputable def coprodIsCoprod (X Y : C) [HasBinaryCoproduct X Y] :
    IsColimit (BinaryCofan.mk (coprod.inl : X ⟶ X ⨿ Y) coprod.inr) :=
  (colimit.isColimit _).ofIsoColimit (Cocones.ext (Iso.refl _) (fun ⟨u⟩ => by
    cases u
    · dsimp; simp only [Category.comp_id]
    · dsimp; simp only [Category.comp_id]
  ))

Universal property of binary coproduct cocone

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$ with binary coproducts, the binary cofan formed by the coproduct inclusions $\mathrm{coprod.inl} \colon X \to X \sqcup Y$ and $\mathrm{coprod.inr} \colon Y \to X \sqcup Y$ is a colimit cocone. This means it satisfies the universal property of coproducts: for any other cocone over the pair $(X, Y)$, there exists a unique morphism from the coproduct cocone to that cocone.

CategoryTheory.Limits.prod.hom_ext theorem

 {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} (h₁ : f ≫ prod.fst = g ≫ prod.fst)
  (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g

Full source

@[ext 1100]
theorem prod.hom_ext {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y}
    (h₁ : f ≫ prod.fst = g ≫ prod.fst) (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
  BinaryFan.IsLimit.hom_ext (limit.isLimit _) h₁ h₂

Uniqueness of Morphisms into Binary Product via Commuting Projections

Informal description

Let $\mathcal{C}$ be a category with binary products, and let $X$ and $Y$ be objects in $\mathcal{C}$. For any object $W$ in $\mathcal{C}$ and morphisms $f, g : W \to X \times Y$, if both compositions $f \circ \pi_1 = g \circ \pi_1$ and $f \circ \pi_2 = g \circ \pi_2$ hold (where $\pi_1 : X \times Y \to X$ and $\pi_2 : X \times Y \to Y$ are the projection morphisms), then $f = g$.

CategoryTheory.Limits.coprod.hom_ext theorem

 {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} (h₁ : coprod.inl ≫ f = coprod.inl ≫ g)
  (h₂ : coprod.inr ≫ f = coprod.inr ≫ g) : f = g

Full source

@[ext 1100]
theorem coprod.hom_ext {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ YX ⨿ Y ⟶ W}
    (h₁ : coprod.inlcoprod.inl ≫ f = coprod.inlcoprod.inl ≫ g) (h₂ : coprod.inrcoprod.inr ≫ f = coprod.inrcoprod.inr ≫ g) : f = g :=
  BinaryCofan.IsColimit.hom_ext (colimit.isColimit _) h₁ h₂

Uniqueness of Morphisms from Binary Coproduct via Commuting Coprojections

Informal description

Let $\mathcal{C}$ be a category with binary coproducts, and let $X, Y \in \mathcal{C}$. For any object $W \in \mathcal{C}$ and any two morphisms $f, g : X \sqcup Y \to W$, if the compositions of the left inclusion $\iota_X : X \to X \sqcup Y$ with $f$ and $g$ are equal, and similarly for the right inclusion $\iota_Y : Y \to X \sqcup Y$, then $f = g$. In other words, if $f \circ \iota_X = g \circ \iota_X$ and $f \circ \iota_Y = g \circ \iota_Y$, then $f = g$.

CategoryTheory.Limits.prod.lift abbrev

{W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y

Full source

/-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
    induces a morphism `prod.lift f g : W ⟶ X ⨯ Y`. -/
noncomputable abbrev prod.lift {W X Y : C} [HasBinaryProduct X Y]
    (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y :=
  limit.lift _ (BinaryFan.mk f g)

Universal property of binary product: $\mathrm{prod.lift}\,f\,g$

Informal description

Given objects $W, X, Y$ in a category $\mathcal{C}$ with binary products, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, there exists a unique morphism $\mathrm{prod.lift}\,f\,g \colon W \to X \times Y$ induced by the universal property of the product $X \times Y$.

CategoryTheory.Limits.diag abbrev

(X : C) [HasBinaryProduct X X] : X ⟶ X ⨯ X

Full source

/-- diagonal arrow of the binary product in the category `fam I` -/
noncomputable abbrev diag (X : C) [HasBinaryProduct X X] : X ⟶ X ⨯ X :=
  prod.lift (𝟙 _) (𝟙 _)

Diagonal Morphism of Binary Product

Informal description

For an object $X$ in a category $\mathcal{C}$ that has binary products, the diagonal morphism $\mathrm{diag}_X \colon X \to X \times X$ is the unique morphism induced by the universal property of the product, corresponding to the pair of identity morphisms $(\mathrm{id}_X, \mathrm{id}_X)$.

CategoryTheory.Limits.coprod.desc abbrev

{W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W

Full source

/-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
    `g : Y ⟶ W` induces a morphism `coprod.desc f g : X ⨿ Y ⟶ W`. -/
noncomputable abbrev coprod.desc {W X Y : C} [HasBinaryCoproduct X Y]
    (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ YX ⨿ Y ⟶ W :=
  colimit.desc _ (BinaryCofan.mk f g)

Universal Property of Binary Coproducts

Informal description

Given objects $X$, $Y$, and $W$ in a category $\mathcal{C}$ that has binary coproducts, and morphisms $f \colon X \to W$ and $g \colon Y \to W$, there exists a unique morphism $\mathrm{coprod.desc}\,f\,g \colon X \sqcup Y \to W$ induced by the universal property of the coproduct.

CategoryTheory.Limits.codiag abbrev

(X : C) [HasBinaryCoproduct X X] : X ⨿ X ⟶ X

Full source

/-- codiagonal arrow of the binary coproduct -/
noncomputable abbrev codiag (X : C) [HasBinaryCoproduct X X] : X ⨿ XX ⨿ X ⟶ X :=
  coprod.desc (𝟙 _) (𝟙 _)

Codiagonal Morphism of Binary Coproduct

Informal description

For an object $X$ in a category $\mathcal{C}$ that has binary coproducts, the codiagonal morphism $\mathrm{codiag}_X \colon X \sqcup X \to X$ is the unique morphism induced by the universal property of the coproduct, corresponding to the pair of identity morphisms $(\mathrm{id}_X, \mathrm{id}_X)$.

CategoryTheory.Limits.prod.lift_fst theorem

{W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : prod.lift f g ≫ prod.fst = f

Full source

@[reassoc]
theorem prod.lift_fst {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
    prod.liftprod.lift f g ≫ prod.fst = f :=
  limit.lift_π _ _

Commutativity of Product Lift with First Projection

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $W, X, Y \in \mathcal{C}$ and morphisms $f \colon W \to X$ and $g \colon W \to Y$, the composition of the product lift morphism $\mathrm{prod.lift}\,f\,g \colon W \to X \times Y$ with the first projection $\pi_1 \colon X \times Y \to X$ equals $f$, i.e., \[ \mathrm{prod.lift}\,f\,g \circ \pi_1 = f. \]

CategoryTheory.Limits.prod.lift_snd theorem

{W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : prod.lift f g ≫ prod.snd = g

Full source

@[reassoc]
theorem prod.lift_snd {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
    prod.liftprod.lift f g ≫ prod.snd = g :=
  limit.lift_π _ _

Commutativity of product lift with second projection: $\mathrm{lift}\,f\,g \circ \pi_2 = g$

Informal description

For any objects $W, X, Y$ in a category $\mathcal{C}$ with binary products, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, the composition of the product lift morphism $\mathrm{prod.lift}\,f\,g \colon W \to X \times Y$ with the second projection $\mathrm{snd} \colon X \times Y \to Y$ equals $g$, i.e., \[ \mathrm{prod.lift}\,f\,g \circ \mathrm{snd} = g. \]

CategoryTheory.Limits.coprod.inl_desc theorem

{W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : coprod.inl ≫ coprod.desc f g = f

Full source

@[reassoc]
theorem coprod.inl_desc {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
    coprod.inlcoprod.inl ≫ coprod.desc f g = f :=
  colimit.ι_desc _ _

Commutativity of Left Coprojection with Coproduct Universal Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts, and let $X$, $Y$, and $W$ be objects in $\mathcal{C}$. For any morphisms $f \colon X \to W$ and $g \colon Y \to W$, the composition of the left coprojection $\mathrm{inl} \colon X \to X \sqcup Y$ with the induced morphism $\mathrm{desc}\,f\,g \colon X \sqcup Y \to W$ equals $f$, i.e., \[ \mathrm{inl} \circ \mathrm{desc}\,f\,g = f. \]

CategoryTheory.Limits.coprod.inr_desc theorem

{W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : coprod.inr ≫ coprod.desc f g = g

Full source

@[reassoc]
theorem coprod.inr_desc {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
    coprod.inrcoprod.inr ≫ coprod.desc f g = g :=
  colimit.ι_desc _ _

Commutativity of Right Coprojection with Coproduct Descending Morphism

Informal description

In a category $\mathcal{C}$ with binary coproducts, given objects $X$, $Y$, and $W$ and morphisms $f \colon X \to W$ and $g \colon Y \to W$, the composition of the right coprojection $\iota_r \colon Y \to X \sqcup Y$ with the universal morphism $\mathrm{desc}(f,g) \colon X \sqcup Y \to W$ equals $g$.

CategoryTheory.Limits.prod.mono_lift_of_mono_left instance

{W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (prod.lift f g)

Full source

instance prod.mono_lift_of_mono_left {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y)
    [Mono f] : Mono (prod.lift f g) :=
  mono_of_mono_fac <| prod.lift_fst _ _

Lift of a Mono Morphism to a Product is Mono

Informal description

In a category $\mathcal{C}$ with binary products, given objects $W, X, Y$ and morphisms $f \colon W \to X$ and $g \colon W \to Y$, if $f$ is a monomorphism, then the induced morphism $\mathrm{prod.lift}\,f\,g \colon W \to X \times Y$ is also a monomorphism.

CategoryTheory.Limits.prod.mono_lift_of_mono_right instance

{W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (prod.lift f g)

Full source

instance prod.mono_lift_of_mono_right {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y)
    [Mono g] : Mono (prod.lift f g) :=
  mono_of_mono_fac <| prod.lift_snd _ _

Monomorphism Property of Product Lift with Monomorphic Right Component

Informal description

In a category $\mathcal{C}$ with binary products, given objects $W, X, Y$ and morphisms $f \colon W \to X$ and $g \colon W \to Y$, if $g$ is a monomorphism, then the induced morphism $\mathrm{prod.lift}\,f\,g \colon W \to X \times Y$ is also a monomorphism.

CategoryTheory.Limits.coprod.epi_desc_of_epi_left instance

{W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] : Epi (coprod.desc f g)

Full source

instance coprod.epi_desc_of_epi_left {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
    [Epi f] : Epi (coprod.desc f g) :=
  epi_of_epi_fac <| coprod.inl_desc _ _

Epimorphism Property Preserved by Coproduct Universal Morphism via Left Component

Informal description

Let $\mathcal{C}$ be a category with binary coproducts, and let $X$, $Y$, and $W$ be objects in $\mathcal{C}$. Given morphisms $f \colon X \to W$ and $g \colon Y \to W$, if $f$ is an epimorphism, then the induced morphism $\mathrm{coprod.desc}\,f\,g \colon X \sqcup Y \to W$ is also an epimorphism.

CategoryTheory.Limits.coprod.epi_desc_of_epi_right instance

{W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] : Epi (coprod.desc f g)

Full source

instance coprod.epi_desc_of_epi_right {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
    [Epi g] : Epi (coprod.desc f g) :=
  epi_of_epi_fac <| coprod.inr_desc _ _

Epimorphism Property via Right Coprojection in Binary Coproducts

Informal description

In a category $\mathcal{C}$ with binary coproducts, given objects $W, X, Y$ and morphisms $f \colon X \to W$ and $g \colon Y \to W$, if $g$ is an epimorphism, then the induced morphism $\mathrm{coprod.desc}\,f\,g \colon X \sqcup Y \to W$ is also an epimorphism.

CategoryTheory.Limits.prod.lift' definition

 {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ X ⨯ Y // l ≫ prod.fst = f ∧ l ≫ prod.snd = g }

Full source

/-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
    induces a morphism `l : W ⟶ X ⨯ Y` satisfying `l ≫ Prod.fst = f` and `l ≫ Prod.snd = g`. -/
noncomputable def prod.lift' {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
    { l : W ⟶ X ⨯ Y // l ≫ prod.fst = f ∧ l ≫ prod.snd = g } :=
  ⟨prod.lift f g, prod.lift_fst _ _, prod.lift_snd _ _⟩

Universal property of binary product: existence of induced morphism

Informal description

Given objects $W, X, Y$ in a category $\mathcal{C}$ with binary products, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, there exists a unique morphism $l \colon W \to X \times Y$ such that $l$ composed with the first projection equals $f$ and $l$ composed with the second projection equals $g$. This morphism is precisely the one induced by the universal property of the product $X \times Y$.

CategoryTheory.Limits.coprod.desc' definition

 {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
  { l : X ⨿ Y ⟶ W // coprod.inl ≫ l = f ∧ coprod.inr ≫ l = g }

Full source

/-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
    `g : Y ⟶ W` induces a morphism `l : X ⨿ Y ⟶ W` satisfying `coprod.inl ≫ l = f` and
    `coprod.inr ≫ l = g`. -/
noncomputable def coprod.desc' {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
    { l : X ⨿ Y ⟶ W // coprod.inl ≫ l = f ∧ coprod.inr ≫ l = g } :=
  ⟨coprod.desc f g, coprod.inl_desc _ _, coprod.inr_desc _ _⟩

Universal property of binary coproducts (bundled version)

Informal description

Given objects $X$, $Y$, and $W$ in a category $\mathcal{C}$ that has binary coproducts, and morphisms $f \colon X \to W$ and $g \colon Y \to W$, there exists a unique morphism $l \colon X \sqcup Y \to W$ such that the composition of the left inclusion $\mathrm{coprod.inl}$ with $l$ equals $f$, and the composition of the right inclusion $\mathrm{coprod.inr}$ with $l$ equals $g$.

CategoryTheory.Limits.prod.map definition

{W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨯ X ⟶ Y ⨯ Z

Full source

/-- If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of morphisms `f : W ⟶ Y` and
    `g : X ⟶ Z` induces a morphism `prod.map f g : W ⨯ X ⟶ Y ⨯ Z`. -/
noncomputable def prod.map {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z]
    (f : W ⟶ Y) (g : X ⟶ Z) : W ⨯ XW ⨯ X ⟶ Y ⨯ Z :=
  limMap (mapPair f g)

Induced morphism on binary products via component-wise maps

Informal description

Given objects $ W, X, Y, Z $ in a category $ \mathcal{C} $ where the binary products $ W \times X $ and $ Y \times Z $ exist, and morphisms $ f \colon W \to Y $ and $ g \colon X \to Z $, the morphism $ \mathrm{prod.map}\,f\,g \colon W \times X \to Y \times Z $ is the unique morphism induced by the universal property of the product $ Y \times Z $. This morphism is constructed as the limit map of the natural transformation $ \mathrm{mapPair}\,f\,g $ between the functors $ \mathrm{pair}\,W\,X $ and $ \mathrm{pair}\,Y\,Z $.

CategoryTheory.Limits.coprod.map definition

{W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ X ⟶ Y ⨿ Z

Full source

/-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of morphisms `f : W ⟶ Y` and
    `g : W ⟶ Z` induces a morphism `coprod.map f g : W ⨿ X ⟶ Y ⨿ Z`. -/
noncomputable def coprod.map {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z]
    (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ XW ⨿ X ⟶ Y ⨿ Z :=
  colimMap (mapPair f g)

Coproduct map induced by a pair of morphisms

Informal description

Given objects $ W, X, Y, Z $ in a category $ \mathcal{C} $ that has binary coproducts $ W \sqcup X $ and $ Y \sqcup Z $, and given morphisms $ f \colon W \to Y $ and $ g \colon X \to Z $, the coproduct map $ \mathrm{coprod.map}\,f\,g \colon W \sqcup X \to Y \sqcup Z $ is the morphism induced by the universal property of the coproduct $ W \sqcup X $ applied to the cocone obtained by composing $ f $ and $ g $ with the coproduct inclusions of $ Y \sqcup Z $.

CategoryTheory.Limits.prod.comp_lift theorem

 {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
  f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h)

Full source

@[reassoc, simp]
theorem prod.comp_lift {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
    f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h) := by ext <;> simp

Composition with Product Lift Equals Lift of Compositions

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $V, W, X, Y$ in $\mathcal{C}$ and morphisms $f \colon V \to W$, $g \colon W \to X$, and $h \colon W \to Y$, the composition of $f$ with the product morphism $\mathrm{lift}(g, h) \colon W \to X \times Y$ is equal to the product morphism $\mathrm{lift}(f \circ g, f \circ h) \colon V \to X \times Y$. In other words, the following diagram commutes: \[ f \circ \mathrm{lift}(g, h) = \mathrm{lift}(f \circ g, f \circ h). \]

CategoryTheory.Limits.prod.comp_diag theorem

{X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) : f ≫ diag Y = prod.lift f f

Full source

theorem prod.comp_diag {X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) :
    f ≫ diag Y = prod.lift f f := by simp

Composition with Diagonal Equals Lift of Identical Morphisms

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X$ and $Y$ in $\mathcal{C}$ where the product $Y \times Y$ exists, and for any morphism $f \colon X \to Y$, the composition of $f$ with the diagonal morphism $\mathrm{diag}_Y \colon Y \to Y \times Y$ is equal to the product morphism $\mathrm{lift}(f, f) \colon X \to Y \times Y$. In other words, the following diagram commutes: \[ f \circ \mathrm{diag}_Y = \mathrm{lift}(f, f). \]

CategoryTheory.Limits.prod.map_fst theorem

 {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  prod.map f g ≫ prod.fst = prod.fst ≫ f

Full source

@[reassoc (attr := simp)]
theorem prod.map_fst {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : prod.mapprod.map f g ≫ prod.fst = prod.fstprod.fst ≫ f :=
  limMap_π _ _

Commutativity of Product Map with First Projection

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $W, X, Y, Z$ in $\mathcal{C}$ where $W \times X$ and $Y \times Z$ exist, and for any morphisms $f \colon W \to Y$ and $g \colon X \to Z$, the following diagram commutes: \[ \mathrm{prod.map}\,f\,g \circ \pi_1 = \pi_1 \circ f \] where: - $\pi_1 \colon W \times X \to W$ and $\pi_1 \colon Y \times Z \to Y$ are the first projection morphisms, - $\mathrm{prod.map}\,f\,g \colon W \times X \to Y \times Z$ is the product map induced by $f$ and $g$.

CategoryTheory.Limits.prod.map_snd theorem

 {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  prod.map f g ≫ prod.snd = prod.snd ≫ g

Full source

@[reassoc (attr := simp)]
theorem prod.map_snd {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : prod.mapprod.map f g ≫ prod.snd = prod.sndprod.snd ≫ g :=
  limMap_π _ _

Commutativity of Product Map with Second Projection

Informal description

Let $\mathcal{C}$ be a category with binary products. Given objects $W, X, Y, Z \in \mathcal{C}$ where $W \times X$ and $Y \times Z$ exist, and morphisms $f: W \to Y$ and $g: X \to Z$, the following diagram commutes: \[ \text{prod.map}\, f\, g \circ \pi_2 = \pi_2 \circ g \] where: - $\text{prod.map}\, f\, g: W \times X \to Y \times Z$ is the product map induced by $f$ and $g$, - $\pi_2: X \times Y \to Y$ is the second projection morphism.

CategoryTheory.Limits.prod.map_id_id theorem

{X Y : C} [HasBinaryProduct X Y] : prod.map (𝟙 X) (𝟙 Y) = 𝟙 _

Full source

@[simp]
theorem prod.map_id_id {X Y : C} [HasBinaryProduct X Y] : prod.map (𝟙 X) (𝟙 Y) = 𝟙 _ := by
  ext <;> simp

Identity Product Map is Identity Morphism

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ that has binary products, the product map $\mathrm{prod.map}\,(𝟙_X)\,(𝟙_Y) \colon X \times Y \to X \times Y$ induced by the identity morphisms on $X$ and $Y$ is equal to the identity morphism on $X \times Y$.

CategoryTheory.Limits.prod.lift_fst_snd theorem

{X Y : C} [HasBinaryProduct X Y] : prod.lift prod.fst prod.snd = 𝟙 (X ⨯ Y)

Full source

@[simp]
theorem prod.lift_fst_snd {X Y : C} [HasBinaryProduct X Y] :
    prod.lift prod.fst prod.snd = 𝟙 (X ⨯ Y) := by ext <;> simp

Identity Morphism via Product Lift of Projections

Informal description

In a category $\mathcal{C}$ with binary products, the morphism $\mathrm{prod.lift}\, \pi_1\, \pi_2 \colon X \times Y \to X \times Y$ induced by the universal property of the product is equal to the identity morphism on $X \times Y$, where $\pi_1 \colon X \times Y \to X$ and $\pi_2 \colon X \times Y \to Y$ are the projection morphisms.

CategoryTheory.Limits.prod.lift_map theorem

 {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
  prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k)

Full source

@[reassoc (attr := simp)]
theorem prod.lift_map {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W)
    (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
    prod.liftprod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k) := by ext <;> simp

Commutativity of Product Lift and Map

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $V, W, X, Y, Z$ in $\mathcal{C}$ where the binary products $W \times X$ and $Y \times Z$ exist, and for any morphisms $f \colon V \to W$, $g \colon V \to X$, $h \colon W \to Y$, $k \colon X \to Z$, the following diagram commutes: \[ \mathrm{prod.lift}\, f\, g \circ \mathrm{prod.map}\, h\, k = \mathrm{prod.lift}\, (f \circ h)\, (g \circ k) \]

CategoryTheory.Limits.prod.lift_fst_comp_snd_comp theorem

 {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
  prod.lift (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g'

Full source

@[simp]
theorem prod.lift_fst_comp_snd_comp {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z]
    (g : W ⟶ X) (g' : Y ⟶ Z) : prod.lift (prod.fstprod.fst ≫ g) (prod.sndprod.snd ≫ g') = prod.map g g' := by
  rw [← prod.lift_map]
  simp

Equality of Product Lift and Map via Composed Projections

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $W, X, Y, Z$ in $\mathcal{C}$ where the binary products $W \times Y$ and $X \times Z$ exist, and for any morphisms $g \colon W \to X$ and $g' \colon Y \to Z$, the morphism $\mathrm{prod.lift}\, (\pi_1 \circ g)\, (\pi_2 \circ g') \colon W \times Y \to X \times Z$ is equal to the product map $\mathrm{prod.map}\, g\, g'$, where $\pi_1 \colon W \times Y \to W$ and $\pi_2 \colon W \times Y \to Y$ are the projection morphisms.

CategoryTheory.Limits.prod.map_map theorem

 {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂)
  (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : prod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k)

Full source

@[reassoc (attr := simp)]
theorem prod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂]
    [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
    prod.mapprod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k) := by ext <;> simp

Composition of Product Maps Equals Product of Compositions

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $A_1, A_2, A_3, B_1, B_2, B_3$ in $\mathcal{C}$ where the binary products $A_i \times B_i$ exist for $i = 1, 2, 3$, and for any morphisms $f \colon A_1 \to A_2$, $g \colon B_1 \to B_2$, $h \colon A_2 \to A_3$, $k \colon B_2 \to B_3$, the following equality holds: \[ \text{prod.map}\, f\, g \circ \text{prod.map}\, h\, k = \text{prod.map}\, (f \circ h)\, (g \circ k) \]

CategoryTheory.Limits.prod.map_swap theorem

 {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] :
  prod.map (𝟙 X) f ≫ prod.map g (𝟙 B) = prod.map g (𝟙 A) ≫ prod.map (𝟙 Y) f

Full source

@[reassoc]
theorem prod.map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
    [HasLimitsOfShape (Discrete WalkingPair) C] :
    prod.mapprod.map (𝟙 X) f ≫ prod.map g (𝟙 B) = prod.mapprod.map g (𝟙 A) ≫ prod.map (𝟙 Y) f := by simp

Commutation of Product Maps with Identity Components

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $A, B, X, Y$ in $\mathcal{C}$ and morphisms $f \colon A \to B$, $g \colon X \to Y$, the following diagram commutes: \[ X \times A \xrightarrow{\mathrm{prod.map}\, \mathrm{id}_X\, f} X \times B \xrightarrow{\mathrm{prod.map}\, g\, \mathrm{id}_B} Y \times B \] \[ X \times A \xrightarrow{\mathrm{prod.map}\, g\, \mathrm{id}_A} Y \times A \xrightarrow{\mathrm{prod.map}\, \mathrm{id}_Y\, f} Y \times B \] That is, $\mathrm{prod.map}\, \mathrm{id}_X\, f \circ \mathrm{prod.map}\, g\, \mathrm{id}_B = \mathrm{prod.map}\, g\, \mathrm{id}_A \circ \mathrm{prod.map}\, \mathrm{id}_Y\, f$.

CategoryTheory.Limits.prod.map_comp_id theorem

 {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W] [HasBinaryProduct Z W] [HasBinaryProduct Y W] :
  prod.map (f ≫ g) (𝟙 W) = prod.map f (𝟙 W) ≫ prod.map g (𝟙 W)

Full source

@[reassoc]
theorem prod.map_comp_id {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W]
    [HasBinaryProduct Z W] [HasBinaryProduct Y W] :
    prod.map (f ≫ g) (𝟙 W) = prod.mapprod.map f (𝟙 W) ≫ prod.map g (𝟙 W) := by simp

Composition of Product Maps with Identity Equals Product of Compositions

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X, Y, Z, W$ in $\mathcal{C}$ where the binary products $X \times W$, $Y \times W$, and $Z \times W$ exist, and for any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the following equality holds: \[ \text{prod.map}\, (f \circ g)\, \text{id}_W = \text{prod.map}\, f\, \text{id}_W \circ \text{prod.map}\, g\, \text{id}_W \]

CategoryTheory.Limits.prod.map_id_comp theorem

 {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X] [HasBinaryProduct W Y] [HasBinaryProduct W Z] :
  prod.map (𝟙 W) (f ≫ g) = prod.map (𝟙 W) f ≫ prod.map (𝟙 W) g

Full source

@[reassoc]
theorem prod.map_id_comp {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X]
    [HasBinaryProduct W Y] [HasBinaryProduct W Z] :
    prod.map (𝟙 W) (f ≫ g) = prod.mapprod.map (𝟙 W) f ≫ prod.map (𝟙 W) g := by simp

Composition of Product Maps with Fixed First Component

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X, Y, Z, W$ in $\mathcal{C}$ where the binary products $W \times X$, $W \times Y$, and $W \times Z$ exist, and for any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the following equality holds: \[ \text{prod.map}\, (\text{id}_W)\, (f \circ g) = \text{prod.map}\, (\text{id}_W)\, f \circ \text{prod.map}\, (\text{id}_W)\, g \]

CategoryTheory.Limits.prod.mapIso definition

{W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨯ X ≅ Y ⨯ Z

Full source

/-- If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
    `g : X ≅ Z` induces an isomorphism `prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z`. -/
@[simps]
def prod.mapIso {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y)
    (g : X ≅ Z) : W ⨯ XW ⨯ X ≅ Y ⨯ Z where
  hom := prod.map f.hom g.hom
  inv := prod.map f.inv g.inv

Isomorphism between binary products induced by component-wise isomorphisms

Informal description

Given objects $ W, X, Y, Z $ in a category $ \mathcal{C} $ where the binary products $ W \times X $ and $ Y \times Z $ exist, and isomorphisms $ f \colon W \cong Y $ and $ g \colon X \cong Z $, the isomorphism $ \mathrm{prod.mapIso}\,f\,g \colon W \times X \cong Y \times Z $ is constructed by applying the product functor component-wise to the morphisms $ f $ and $ g $. Specifically, the forward morphism is $ \mathrm{prod.map}\,f.\mathrm{hom}\,g.\mathrm{hom} $ and the inverse morphism is $ \mathrm{prod.map}\,f.\mathrm{inv}\,g.\mathrm{inv} $.

CategoryTheory.Limits.isIso_prod instance

 {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f] [IsIso g] :
  IsIso (prod.map f g)

Full source

instance isIso_prod {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) [IsIso f] [IsIso g] : IsIso (prod.map f g) :=
  (prod.mapIso (asIso f) (asIso g)).isIso_hom

Isomorphism of Binary Products Induced by Component-wise Isomorphisms

Informal description

For objects $W, X, Y, Z$ in a category $\mathcal{C}$ with binary products $W \times X$ and $Y \times Z$, if $f \colon W \to Y$ and $g \colon X \to Z$ are isomorphisms, then the induced morphism $\mathrm{prod.map}\,f\,g \colon W \times X \to Y \times Z$ is also an isomorphism.

CategoryTheory.Limits.prod.map_mono instance

 {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryProduct W X]
  [HasBinaryProduct Y Z] : Mono (prod.map f g)

Full source

instance prod.map_mono {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
    [Mono g] [HasBinaryProduct W X] [HasBinaryProduct Y Z] : Mono (prod.map f g) :=
  ⟨fun i₁ i₂ h => by
    ext
    · rw [← cancel_mono f]
      simpa using congr_arg (fun f => f ≫ prod.fst) h
    · rw [← cancel_mono g]
      simpa using congr_arg (fun f => f ≫ prod.snd) h⟩

Product Map Preserves Monomorphisms

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $W, X, Y, Z$ in $\mathcal{C}$ and monomorphisms $f \colon W \to Y$ and $g \colon X \to Z$, the induced morphism $\mathrm{prod.map}\,f\,g \colon W \times X \to Y \times Z$ is also a monomorphism.

CategoryTheory.Limits.prod.diag_map theorem

{X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] : diag X ≫ prod.map f f = f ≫ diag Y

Full source

@[reassoc]
theorem prod.diag_map {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] :
    diagdiag X ≫ prod.map f f = f ≫ diag Y := by simp

Commutativity of Diagonal Morphism with Product Map: $\mathrm{diag}_X \circ (f \times f) = f \circ \mathrm{diag}_Y$

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X$ and $Y$ in $\mathcal{C}$ and any morphism $f \colon X \to Y$, the following diagram commutes: \[ \mathrm{diag}_X \circ \mathrm{prod.map}\,f\,f = f \circ \mathrm{diag}_Y \] where $\mathrm{diag}_X \colon X \to X \times X$ and $\mathrm{diag}_Y \colon Y \to Y \times Y$ are the diagonal morphisms, and $\mathrm{prod.map}\,f\,f \colon X \times X \to Y \times Y$ is the morphism induced by $f$ on each component of the product.

CategoryTheory.Limits.prod.diag_map_fst_snd theorem

 {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] :
  diag (X ⨯ Y) ≫ prod.map prod.fst prod.snd = 𝟙 (X ⨯ Y)

Full source

@[reassoc]
theorem prod.diag_map_fst_snd {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] :
    diagdiag (X ⨯ Y) ≫ prod.map prod.fst prod.snd = 𝟙 (X ⨯ Y) := by simp

Identity via Diagonal and Product Map of Projections

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ with binary products, the composition of the diagonal morphism $\mathrm{diag}_{X \times Y} \colon X \times Y \to (X \times Y) \times (X \times Y)$ with the product map $\mathrm{prod.map}\, \pi_1\, \pi_2 \colon (X \times Y) \times (X \times Y) \to X \times Y$ (where $\pi_1 \colon X \times Y \to X$ and $\pi_2 \colon X \times Y \to Y$ are the projection morphisms) equals the identity morphism on $X \times Y$. In symbols: \[ \mathrm{diag}_{X \times Y} \circ \mathrm{prod.map}\, \pi_1\, \pi_2 = \mathrm{id}_{X \times Y} \]

CategoryTheory.Limits.prod.diag_map_fst_snd_comp theorem

 [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') :
  diag (X ⨯ X') ≫ prod.map (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g'

Full source

@[reassoc]
theorem prod.diag_map_fst_snd_comp [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C}
    (g : X ⟶ Y) (g' : X' ⟶ Y') :
    diagdiag (X ⨯ X') ≫ prod.map (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g' := by simp

Commutativity of Diagonal with Product Map via Composed Projections

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X, X', Y, Y'$ in $\mathcal{C}$ and morphisms $g \colon X \to Y$ and $g' \colon X' \to Y'$, the composition of the diagonal morphism $\mathrm{diag}_{X \times X'} \colon X \times X' \to (X \times X') \times (X \times X')$ with the product map $\mathrm{prod.map}\, (\pi_1 \circ g)\, (\pi_2 \circ g') \colon (X \times X') \times (X \times X') \to Y \times Y'$ equals the product map $\mathrm{prod.map}\, g\, g' \colon X \times X' \to Y \times Y'$. In symbols: \[ \mathrm{diag}_{X \times X'} \circ \mathrm{prod.map}\, (\pi_1 \circ g)\, (\pi_2 \circ g') = \mathrm{prod.map}\, g\, g' \] where $\pi_1 \colon X \times X' \to X$ and $\pi_2 \colon X \times X' \to X'$ are the projection morphisms.

CategoryTheory.Limits.instIsSplitMonoDiag instance

{X : C} [HasBinaryProduct X X] : IsSplitMono (diag X)

Full source

instance {X : C} [HasBinaryProduct X X] : IsSplitMono (diag X) :=
  IsSplitMono.mk' { retraction := prod.fst }

The Diagonal Morphism is a Split Monomorphism

Informal description

For any object $X$ in a category $\mathcal{C}$ that has binary products, the diagonal morphism $\mathrm{diag}_X \colon X \to X \times X$ is a split monomorphism. That is, there exists a morphism $X \times X \to X$ such that its composition with $\mathrm{diag}_X$ is the identity morphism on $X$.

CategoryTheory.Limits.coprod.desc_comp theorem

 {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) :
  coprod.desc g h ≫ f = coprod.desc (g ≫ f) (h ≫ f)

Full source

@[reassoc, simp]
theorem coprod.desc_comp {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V)
    (h : Y ⟶ V) : coprod.desccoprod.desc g h ≫ f = coprod.desc (g ≫ f) (h ≫ f) := by
  ext <;> simp

Composition with Coproduct Universal Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $X, Y, V, W \in \mathcal{C}$ and morphisms $f \colon V \to W$, $g \colon X \to V$, and $h \colon Y \to V$, the composition of the coproduct universal morphism $\mathrm{coprod.desc}\,g\,h \colon X \sqcup Y \to V$ with $f$ is equal to the coproduct universal morphism $\mathrm{coprod.desc}\,(g \circ f)\,(h \circ f) \colon X \sqcup Y \to W$. In symbols: \[ \mathrm{coprod.desc}\,g\,h \circ f = \mathrm{coprod.desc}\,(g \circ f)\,(h \circ f). \]

CategoryTheory.Limits.coprod.diag_comp theorem

{X Y : C} [HasBinaryCoproduct X X] (f : X ⟶ Y) : codiag X ≫ f = coprod.desc f f

Full source

theorem coprod.diag_comp {X Y : C} [HasBinaryCoproduct X X] (f : X ⟶ Y) :
    codiagcodiag X ≫ f = coprod.desc f f := by simp

Composition of Codiagonal Morphism with a Morphism Equals Coproduct Universal Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $X, Y \in \mathcal{C}$ and morphism $f \colon X \to Y$, the composition of the codiagonal morphism $\mathrm{codiag}_X \colon X \sqcup X \to X$ with $f$ is equal to the coproduct universal morphism $\mathrm{coprod.desc}\,f\,f \colon X \sqcup X \to Y$. In symbols: \[ \mathrm{codiag}_X \circ f = \mathrm{coprod.desc}\,f\,f. \]

CategoryTheory.Limits.coprod.inl_map theorem

 {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  coprod.inl ≫ coprod.map f g = f ≫ coprod.inl

Full source

@[reassoc (attr := simp)]
theorem coprod.inl_map {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : coprod.inlcoprod.inl ≫ coprod.map f g = f ≫ coprod.inl :=
  ι_colimMap _ _

Commutativity of Left Inclusion with Coproduct Map

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $W, X, Y, Z \in \mathcal{C}$ and morphisms $f \colon W \to Y$ and $g \colon X \to Z$, the composition of the left inclusion $\mathrm{inl} \colon W \to W \sqcup X$ with the coproduct map $\mathrm{coprod.map}\,f\,g \colon W \sqcup X \to Y \sqcup Z$ is equal to the composition of $f$ with the left inclusion $\mathrm{inl} \colon Y \to Y \sqcup Z$. In symbols: \[ \mathrm{inl} \circ \mathrm{coprod.map}\,f\,g = f \circ \mathrm{inl}. \]

CategoryTheory.Limits.coprod.inr_map theorem

 {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  coprod.inr ≫ coprod.map f g = g ≫ coprod.inr

Full source

@[reassoc (attr := simp)]
theorem coprod.inr_map {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : coprod.inrcoprod.inr ≫ coprod.map f g = g ≫ coprod.inr :=
  ι_colimMap _ _

Naturality of Right Coproduct Inclusion with Respect to Coproduct Map

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. Given objects $W, X, Y, Z \in \mathcal{C}$ and morphisms $f \colon W \to Y$, $g \colon X \to Z$, the composition of the right coproduct inclusion $\mathrm{inr} \colon X \to W \sqcup X$ with the coproduct map $\mathrm{coprod.map}\,f\,g \colon W \sqcup X \to Y \sqcup Z$ equals the composition of $g$ with the right coproduct inclusion $\mathrm{inr} \colon Z \to Y \sqcup Z$. In symbols: \[ \mathrm{inr} \circ \mathrm{coprod.map}\,f\,g = g \circ \mathrm{inr} \]

CategoryTheory.Limits.coprod.map_id_id theorem

{X Y : C} [HasBinaryCoproduct X Y] : coprod.map (𝟙 X) (𝟙 Y) = 𝟙 _

Full source

@[simp]
theorem coprod.map_id_id {X Y : C} [HasBinaryCoproduct X Y] : coprod.map (𝟙 X) (𝟙 Y) = 𝟙 _ := by
  ext <;> simp

Identity Coproduct Map is the Identity Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts, and let $X, Y \in \mathcal{C}$. The coproduct map $\mathrm{coprod.map}\,(\mathrm{id}_X)\,(\mathrm{id}_Y) \colon X \sqcup Y \to X \sqcup Y$ is equal to the identity morphism $\mathrm{id}_{X \sqcup Y}$.

CategoryTheory.Limits.coprod.desc_inl_inr theorem

{X Y : C} [HasBinaryCoproduct X Y] : coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y)

Full source

@[simp]
theorem coprod.desc_inl_inr {X Y : C} [HasBinaryCoproduct X Y] :
    coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y) := by ext <;> simp

Identity Morphism via Coproduct Universal Property

Informal description

In a category $\mathcal{C}$ with binary coproducts, for any objects $X$ and $Y$, the morphism $\mathrm{coprod.desc}(\iota_X, \iota_Y) \colon X \sqcup Y \to X \sqcup Y$ induced by the coproduct inclusions $\iota_X \colon X \to X \sqcup Y$ and $\iota_Y \colon Y \to X \sqcup Y$ is equal to the identity morphism on $X \sqcup Y$.

CategoryTheory.Limits.coprod.map_desc theorem

 {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) :
  coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g)

Full source

@[reassoc, simp]
theorem coprod.map_desc {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V]
    (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) :
    coprod.mapcoprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g) := by
  ext <;> simp

Commutativity of Coproduct Map with Descending Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. Given objects $S, T, U, V, W \in \mathcal{C}$ and morphisms $f \colon U \to S$, $g \colon W \to S$, $h \colon T \to U$, and $k \colon V \to W$, the following diagram commutes: \[ \mathrm{coprod.map}\,h\,k \circ \mathrm{coprod.desc}\,f\,g = \mathrm{coprod.desc}\,(h \circ f)\,(k \circ g) \] where: - $\mathrm{coprod.map}\,h\,k \colon T \sqcup V \to U \sqcup W$ is the coproduct map induced by $h$ and $k$, - $\mathrm{coprod.desc}\,f\,g \colon U \sqcup W \to S$ is the universal morphism induced by $f$ and $g$, - $\mathrm{coprod.desc}\,(h \circ f)\,(k \circ g) \colon T \sqcup V \to S$ is the universal morphism induced by $h \circ f$ and $k \circ g$.

CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr theorem

 {W X Y Z : C} [HasBinaryCoproduct W Y] [HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
  coprod.desc (g ≫ coprod.inl) (g' ≫ coprod.inr) = coprod.map g g'

Full source

@[simp]
theorem coprod.desc_comp_inl_comp_inr {W X Y Z : C} [HasBinaryCoproduct W Y]
    [HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
    coprod.desc (g ≫ coprod.inl) (g' ≫ coprod.inr) = coprod.map g g' := by
  rw [← coprod.map_desc]; simp

Universal Property of Coproduct Map via Descending Morphisms

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. Given objects $W, X, Y, Z \in \mathcal{C}$ and morphisms $g \colon W \to X$ and $g' \colon Y \to Z$, the universal morphism $\mathrm{coprod.desc}(g \circ \iota_X, g' \circ \iota_Z) \colon W \sqcup Y \to X \sqcup Z$ is equal to the coproduct map $\mathrm{coprod.map}\,g\,g' \colon W \sqcup Y \to X \sqcup Z$, where $\iota_X \colon X \to X \sqcup Z$ and $\iota_Z \colon Z \to X \sqcup Z$ are the coproduct inclusion maps.

CategoryTheory.Limits.coprod.map_map theorem

 {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂)
  (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : coprod.map f g ≫ coprod.map h k = coprod.map (f ≫ h) (g ≫ k)

Full source

@[reassoc (attr := simp)]
theorem coprod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂]
    [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
    coprod.mapcoprod.map f g ≫ coprod.map h k = coprod.map (f ≫ h) (g ≫ k) := by
  ext <;> simp

Composition of Coproduct Maps Equals Coproduct Map of Compositions

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. Given objects $A_1, A_2, A_3, B_1, B_2, B_3 \in \mathcal{C}$ and morphisms $f \colon A_1 \to A_2$, $g \colon B_1 \to B_2$, $h \colon A_2 \to A_3$, $k \colon B_2 \to B_3$, the composition of the coproduct maps $\mathrm{coprod.map}\,f\,g \colon A_1 \sqcup B_1 \to A_2 \sqcup B_2$ and $\mathrm{coprod.map}\,h\,k \colon A_2 \sqcup B_2 \to A_3 \sqcup B_3$ is equal to the coproduct map of the compositions $\mathrm{coprod.map}\,(f \circ h)\,(g \circ k) \colon A_1 \sqcup B_1 \to A_3 \sqcup B_3$. In symbols: \[ \mathrm{coprod.map}\,f\,g \circ \mathrm{coprod.map}\,h\,k = \mathrm{coprod.map}\,(f \circ h)\,(g \circ k). \]

CategoryTheory.Limits.coprod.map_swap theorem

 {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasColimitsOfShape (Discrete WalkingPair) C] :
  coprod.map (𝟙 X) f ≫ coprod.map g (𝟙 B) = coprod.map g (𝟙 A) ≫ coprod.map (𝟙 Y) f

Full source

@[reassoc]
theorem coprod.map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
    [HasColimitsOfShape (Discrete WalkingPair) C] :
    coprod.mapcoprod.map (𝟙 X) f ≫ coprod.map g (𝟙 B) = coprod.mapcoprod.map g (𝟙 A) ≫ coprod.map (𝟙 Y) f := by simp

Commutation of Coproduct Maps with Identity Morphisms

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $A, B, X, Y \in \mathcal{C}$ and morphisms $f \colon A \to B$ and $g \colon X \to Y$, the following diagram commutes: \[ (X \sqcup A) \xrightarrow{\mathrm{coprod.map}\,(\mathrm{id}_X)\,f} (X \sqcup B) \xrightarrow{\mathrm{coprod.map}\,g\,\mathrm{id}_B} (Y \sqcup B) \] \[ (X \sqcup A) \xrightarrow{\mathrm{coprod.map}\,g\,\mathrm{id}_A} (Y \sqcup A) \xrightarrow{\mathrm{coprod.map}\,(\mathrm{id}_Y)\,f} (Y \sqcup B) \] In other words, the composition of coproduct maps satisfies: \[ \mathrm{coprod.map}\,(\mathrm{id}_X)\,f \circ \mathrm{coprod.map}\,g\,\mathrm{id}_B = \mathrm{coprod.map}\,g\,\mathrm{id}_A \circ \mathrm{coprod.map}\,(\mathrm{id}_Y)\,f. \]

CategoryTheory.Limits.coprod.map_comp_id theorem

 {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct Z W] [HasBinaryCoproduct Y W] [HasBinaryCoproduct X W] :
  coprod.map (f ≫ g) (𝟙 W) = coprod.map f (𝟙 W) ≫ coprod.map g (𝟙 W)

Full source

@[reassoc]
theorem coprod.map_comp_id {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct Z W]
    [HasBinaryCoproduct Y W] [HasBinaryCoproduct X W] :
    coprod.map (f ≫ g) (𝟙 W) = coprod.mapcoprod.map f (𝟙 W) ≫ coprod.map g (𝟙 W) := by simp

Composition of Coproduct Maps with Identity Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. Given objects $X, Y, Z, W \in \mathcal{C}$ and morphisms $f \colon X \to Y$, $g \colon Y \to Z$, the coproduct map of the composition $f \circ g$ with the identity morphism $\mathrm{id}_W$ satisfies: \[ \mathrm{coprod.map}\,(f \circ g)\,\mathrm{id}_W = \mathrm{coprod.map}\,f\,\mathrm{id}_W \circ \mathrm{coprod.map}\,g\,\mathrm{id}_W. \]

CategoryTheory.Limits.coprod.map_id_comp theorem

 {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct W X] [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] :
  coprod.map (𝟙 W) (f ≫ g) = coprod.map (𝟙 W) f ≫ coprod.map (𝟙 W) g

Full source

@[reassoc]
theorem coprod.map_id_comp {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct W X]
    [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] :
    coprod.map (𝟙 W) (f ≫ g) = coprod.mapcoprod.map (𝟙 W) f ≫ coprod.map (𝟙 W) g := by simp

Composition of Coproduct Maps with Identity on Fixed Component

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $X, Y, Z, W \in \mathcal{C}$ and morphisms $f \colon X \to Y$, $g \colon Y \to Z$, the coproduct map of the identity morphism on $W$ and the composition $f \circ g$ is equal to the composition of the coproduct maps of the identity on $W$ with $f$ and $g$ respectively. In symbols: \[ \mathrm{coprod.map}\,(\mathrm{id}_W)\,(f \circ g) = \mathrm{coprod.map}\,(\mathrm{id}_W)\,f \circ \mathrm{coprod.map}\,(\mathrm{id}_W)\,g. \]

CategoryTheory.Limits.coprod.mapIso definition

{W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z

Full source

/-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
   `g : W ≅ Z` induces an isomorphism `coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z`. -/
@[simps]
def coprod.mapIso {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y)
    (g : X ≅ Z) : W ⨿ XW ⨿ X ≅ Y ⨿ Z where
  hom := coprod.map f.hom g.hom
  inv := coprod.map f.inv g.inv

Coproduct isomorphism induced by a pair of isomorphisms

Informal description

Given objects $ W, X, Y, Z $ in a category $ \mathcal{C} $ that has binary coproducts $ W \sqcup X $ and $ Y \sqcup Z $, and given isomorphisms $ f \colon W \cong Y $ and $ g \colon X \cong Z $, the coproduct isomorphism $ \mathrm{coprod.mapIso}\,f\,g \colon W \sqcup X \cong Y \sqcup Z $ is defined by the coproduct map of the morphisms $ f $ and $ g $ in both directions, ensuring that the composition yields the identity morphism.

CategoryTheory.Limits.isIso_coprod instance

 {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f] [IsIso g] :
  IsIso (coprod.map f g)

Full source

instance isIso_coprod {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) [IsIso f] [IsIso g] : IsIso (coprod.map f g) :=
  (coprod.mapIso (asIso f) (asIso g)).isIso_hom

Isomorphism of Coproducts from Component Isomorphisms

Informal description

Given objects $W, X, Y, Z$ in a category $\mathcal{C}$ with binary coproducts $W \sqcup X$ and $Y \sqcup Z$, and morphisms $f \colon W \to Y$ and $g \colon X \to Z$ that are isomorphisms, the coproduct map $\mathrm{coprod.map}\,f\,g \colon W \sqcup X \to Y \sqcup Z$ is also an isomorphism.

CategoryTheory.Limits.coprod.map_epi instance

 {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryCoproduct W X]
  [HasBinaryCoproduct Y Z] : Epi (coprod.map f g)

Full source

instance coprod.map_epi {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
    [Epi g] [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] : Epi (coprod.map f g) :=
  ⟨fun i₁ i₂ h => by
    ext
    · rw [← cancel_epi f]
      simpa using congr_arg (fun f => coprod.inl ≫ f) h
    · rw [← cancel_epi g]
      simpa using congr_arg (fun f => coprod.inr ≫ f) h⟩

Coproduct of Epimorphisms is Epimorphic

Informal description

Let $\mathcal{C}$ be a category with binary coproducts, and let $W, X, Y, Z$ be objects in $\mathcal{C}$. Given epimorphisms $f \colon W \to Y$ and $g \colon X \to Z$, the induced coproduct map $f \sqcup g \colon W \sqcup X \to Y \sqcup Z$ is also an epimorphism.

CategoryTheory.Limits.coprod.map_codiag theorem

 {X Y : C} (f : X ⟶ Y) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] : coprod.map f f ≫ codiag Y = codiag X ≫ f

Full source

@[reassoc]
theorem coprod.map_codiag {X Y : C} (f : X ⟶ Y) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] :
    coprod.mapcoprod.map f f ≫ codiag Y = codiagcodiag X ≫ f := by simp

Commutativity of Coproduct Map with Codiagonal Morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $X, Y \in \mathcal{C}$ and morphism $f \colon X \to Y$, the following diagram commutes: \[ \mathrm{coprod.map}\,f\,f \circ \mathrm{codiag}_Y = \mathrm{codiag}_X \circ f \] where: - $\mathrm{coprod.map}\,f\,f \colon X \sqcup X \to Y \sqcup Y$ is the coproduct map induced by $f$ on both components, - $\mathrm{codiag}_X \colon X \sqcup X \to X$ and $\mathrm{codiag}_Y \colon Y \sqcup Y \to Y$ are the codiagonal morphisms.

CategoryTheory.Limits.coprod.map_inl_inr_codiag theorem

 {X Y : C} [HasBinaryCoproduct X Y] [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] :
  coprod.map coprod.inl coprod.inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)

Full source

@[reassoc]
theorem coprod.map_inl_inr_codiag {X Y : C} [HasBinaryCoproduct X Y]
    [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] :
    coprod.mapcoprod.map coprod.inl coprod.inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y) := by simp

Identity via coproduct map and codiagonal morphism

Informal description

Let $\mathcal{C}$ be a category with binary coproducts. For any objects $X$ and $Y$ in $\mathcal{C}$, the composition of the coproduct map $\mathrm{coprod.map}\,\iota_X\,\iota_Y \colon X \sqcup Y \to (X \sqcup Y) \sqcup (X \sqcup Y)$ (where $\iota_X \colon X \to X \sqcup Y$ and $\iota_Y \colon Y \to X \sqcup Y$ are the coproduct inclusions) with the codiagonal morphism $\mathrm{codiag}_{X \sqcup Y} \colon (X \sqcup Y) \sqcup (X \sqcup Y) \to X \sqcup Y$ equals the identity morphism on $X \sqcup Y$.

CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag theorem

 [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') :
  coprod.map (g ≫ coprod.inl) (g' ≫ coprod.inr) ≫ codiag (Y ⨿ Y') = coprod.map g g'

Full source

@[reassoc]
theorem coprod.map_comp_inl_inr_codiag [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C}
    (g : X ⟶ Y) (g' : X' ⟶ Y') :
    coprod.mapcoprod.map (g ≫ coprod.inl) (g' ≫ coprod.inr) ≫ codiag (Y ⨿ Y') = coprod.map g g' := by simp

Commutativity of coproduct map composition with codiagonal morphism

Informal description

Let $\mathcal{C}$ be a category with colimits of shape $\mathrm{Discrete}\,\mathrm{WalkingPair}$. For any objects $X, X', Y, Y' \in \mathcal{C}$ and morphisms $g \colon X \to Y$, $g' \colon X' \to Y'$, the composition of the coproduct map $\mathrm{coprod.map}(g \circ \iota_Y, g' \circ \iota_{Y'})$ with the codiagonal morphism $\mathrm{codiag}_{Y \sqcup Y'}$ equals the coproduct map $\mathrm{coprod.map}\,g\,g'$, where $\iota_Y \colon Y \to Y \sqcup Y'$ and $\iota_{Y'} \colon Y' \to Y \sqcup Y'$ are the coproduct inclusion maps.

CategoryTheory.Limits.HasBinaryProducts abbrev

Full source

/-- `HasBinaryProducts` represents a choice of product for every pair of objects. -/
@[stacks 001T]
abbrev HasBinaryProducts :=
  HasLimitsOfShape (Discrete WalkingPair) C

Existence of Binary Products in a Category

Informal description

A category $\mathcal{C}$ has binary products if for every pair of objects $X, Y$ in $\mathcal{C}$, there exists a product object $X \times Y$ together with projection morphisms $\pi_1 : X \times Y \to X$ and $\pi_2 : X \times Y \to Y$ satisfying the universal property of products.

CategoryTheory.Limits.HasBinaryCoproducts abbrev

Full source

/-- `HasBinaryCoproducts` represents a choice of coproduct for every pair of objects. -/
@[stacks 04AP]
abbrev HasBinaryCoproducts :=
  HasColimitsOfShape (Discrete WalkingPair) C

Existence of Binary Coproducts in a Category

Informal description

A category $\mathcal{C}$ has binary coproducts if for every pair of objects $X, Y$ in $\mathcal{C}$, there exists a colimit for the diagram indexed by the discrete category with two objects (representing $X$ and $Y$). This means there exists an object $X \sqcup Y$ equipped with inclusion morphisms $X \to X \sqcup Y$ and $Y \to X \sqcup Y$ satisfying the universal property of coproducts.

CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair theorem

[∀ {X Y : C}, HasLimit (pair X Y)] : HasBinaryProducts C

Full source

/-- If `C` has all limits of diagrams `pair X Y`, then it has all binary products -/
theorem hasBinaryProducts_of_hasLimit_pair [∀ {X Y : C}, HasLimit (pair X Y)] :
    HasBinaryProducts C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoPair F).symm }

Existence of Binary Products from Limits of Pair Diagrams

Informal description

If a category $\mathcal{C}$ has all limits of diagrams of the form $\mathrm{pair}\,X\,Y$ for every pair of objects $X, Y$ in $\mathcal{C}$, then $\mathcal{C}$ has all binary products.

CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair theorem

[∀ {X Y : C}, HasColimit (pair X Y)] : HasBinaryCoproducts C

Full source

/-- If `C` has all colimits of diagrams `pair X Y`, then it has all binary coproducts -/
theorem hasBinaryCoproducts_of_hasColimit_pair [∀ {X Y : C}, HasColimit (pair X Y)] :
    HasBinaryCoproducts C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoPair F) }

Existence of Binary Coproducts from Pairwise Colimits

Informal description

If a category $\mathcal{C}$ has all colimits of diagrams of the form $\mathrm{pair}\,X\,Y$ for every pair of objects $X, Y \in \mathcal{C}$, then $\mathcal{C}$ has all binary coproducts.

CategoryTheory.Limits.prod.braiding definition

(P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ Q ≅ Q ⨯ P

Full source

/-- The braiding isomorphism which swaps a binary product. -/
@[simps]
def prod.braiding (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ QP ⨯ Q ≅ Q ⨯ P where
  hom := prod.lift prod.snd prod.fst
  inv := prod.lift prod.snd prod.fst

Braiding isomorphism for binary products

Informal description

Given objects $P$ and $Q$ in a category $\mathcal{C}$ that has binary products, the braiding isomorphism $\mathrm{prod.braiding}\,P\,Q : P \times Q \cong Q \times P$ is defined by the morphisms $\mathrm{prod.lift}\,\pi_2\,\pi_1$ in both directions, where $\pi_1$ and $\pi_2$ are the first and second projection morphisms from the respective products.

CategoryTheory.Limits.braid_natural theorem

 [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
  prod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f

Full source

/-- The braiding isomorphism can be passed through a map by swapping the order. -/
@[reassoc]
theorem braid_natural [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
    prod.mapprod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f := by simp

Naturality of the Braiding Isomorphism with Respect to Product Maps

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $W, X, Y, Z$ in $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon Z \to W$, the following diagram commutes: \[ \mathrm{prod.map}\,f\,g \circ \mathrm{prod.braiding}\,X\,Z = \mathrm{prod.braiding}\,Y\,W \circ \mathrm{prod.map}\,g\,f \] where: - $\mathrm{prod.map}\,f\,g \colon X \times Z \to Y \times W$ is the product map induced by $f$ and $g$, - $\mathrm{prod.braiding}\,X\,Z \colon X \times Z \to Z \times X$ is the braiding isomorphism, - $\mathrm{prod.braiding}\,Y\,W \colon Y \times W \to W \times Y$ is the braiding isomorphism.

CategoryTheory.Limits.prod.symmetry' theorem

 (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
  prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q)

Full source

@[reassoc]
theorem prod.symmetry' (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
    prod.liftprod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
  (prod.braiding _ _).hom_inv_id

Identity of Double Braiding in Binary Products

Informal description

For any objects $P$ and $Q$ in a category $\mathcal{C}$ that has binary products, the composition of the morphism $\mathrm{prod.lift}\,\pi_2\,\pi_1$ with itself is equal to the identity morphism on $P \times Q$, i.e., \[ (\mathrm{lift}\, \pi_2\, \pi_1) \circ (\mathrm{lift}\, \pi_2\, \pi_1) = \mathrm{id}_{P \times Q} \] where $\pi_1: P \times Q \to P$ and $\pi_2: P \times Q \to Q$ are the projection morphisms.

CategoryTheory.Limits.prod.symmetry theorem

(P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : (prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _

Full source

/-- The braiding isomorphism is symmetric. -/
@[reassoc]
theorem prod.symmetry (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
    (prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
  (prod.braiding _ _).hom_inv_id

Symmetry of the Braiding Isomorphism for Binary Products

Informal description

For any objects $P$ and $Q$ in a category $\mathcal{C}$ with binary products, the composition of the braiding isomorphism $\mathrm{prod.braiding}\,P\,Q \colon P \times Q \to Q \times P$ with its inverse $\mathrm{prod.braiding}\,Q\,P \colon Q \times P \to P \times Q$ is equal to the identity morphism on $P \times Q$, i.e., \[ \mathrm{prod.braiding}\,P\,Q \circ \mathrm{prod.braiding}\,Q\,P = \mathrm{id}_{P \times Q}. \]

CategoryTheory.Limits.prod.associator definition

[HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R

Full source

/-- The associator isomorphism for binary products. -/
@[simps]
def prod.associator [HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R(P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R where
  hom := prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)
  inv := prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd)

Associator isomorphism for binary products

Informal description

The associator isomorphism for binary products in a category $\mathcal{C}$ with binary products is a natural isomorphism $(P \times Q) \times R \cong P \times (Q \times R)$ for any objects $P, Q, R$ in $\mathcal{C}$. The forward morphism is given by the composite of projection morphisms, and the inverse morphism is constructed similarly to satisfy the isomorphism conditions.

CategoryTheory.Limits.prod.pentagon theorem

 [HasBinaryProducts C] (W X Y Z : C) :
  prod.map (prod.associator W X Y).hom (𝟙 Z) ≫
      (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) (prod.associator X Y Z).hom =
    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom

Full source

@[reassoc]
theorem prod.pentagon [HasBinaryProducts C] (W X Y Z : C) :
    prod.mapprod.map (prod.associator W X Y).hom (𝟙 Z) ≫
        (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) (prod.associator X Y Z).hom =
      (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom := by
  simp

Pentagon Identity for Binary Product Associators

Informal description

In a category $\mathcal{C}$ with binary products, for any objects $W, X, Y, Z$, the following pentagon diagram commutes: \[ \begin{tikzcd} & (W \times X) \times Y \times Z \arrow[dr, "{\mathrm{prod.map}(\alpha_{W,X,Y}, \mathrm{id}_Z)}"] & \\ (W \times (X \times Y)) \times Z \arrow[ur, "{\alpha_{W,X \times Y,Z}}"] \arrow[dr, "{\mathrm{prod.map}(\mathrm{id}_W, \alpha_{X,Y,Z})}"] & & W \times X \times (Y \times Z) \\ & W \times (X \times (Y \times Z)) \arrow[ur, "{\alpha_{W,X,Y \times Z}}"] & \end{tikzcd} \] where $\alpha_{A,B,C} \colon (A \times B) \times C \to A \times (B \times C)$ denotes the associator isomorphism.

CategoryTheory.Limits.prod.associator_naturality theorem

 [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
  prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
    (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃)

Full source

@[reassoc]
theorem prod.associator_naturality [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁)
    (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    prod.mapprod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
      (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) := by
  simp

Naturality of the Associator Isomorphism for Binary Products

Informal description

Let $\mathcal{C}$ be a category with binary products. For any objects $X_1, X_2, X_3, Y_1, Y_2, Y_3$ in $\mathcal{C}$ and morphisms $f_1 \colon X_1 \to Y_1$, $f_2 \colon X_2 \to Y_2$, $f_3 \colon X_3 \to Y_3$, the following diagram commutes: \[ \begin{tikzcd} (X_1 \times X_2) \times X_3 \arrow[r, "{\alpha_{X_1,X_2,X_3}}"] \arrow[d, "{\mathrm{map}(\mathrm{map}(f_1, f_2), f_3)}"'] & X_1 \times (X_2 \times X_3) \arrow[d, "{\mathrm{map}(f_1, \mathrm{map}(f_2, f_3))}"] \\ (Y_1 \times Y_2) \times Y_3 \arrow[r, "{\alpha_{Y_1,Y_2,Y_3}}"'] & Y_1 \times (Y_2 \times Y_3) \end{tikzcd} \] where $\alpha_{A,B,C} \colon (A \times B) \times C \to A \times (B \times C)$ denotes the associator isomorphism for binary products.

CategoryTheory.Limits.prod.leftUnitor definition

(P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P

Full source

/-- The left unitor isomorphism for binary products with the terminal object. -/
@[simps]
def prod.leftUnitor (P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P(⊤_ C) ⨯ P ≅ P where
  hom := prod.snd
  inv := prod.lift (terminal.from P) (𝟙 _)
  hom_inv_id := by apply prod.hom_ext <;> simp [eq_iff_true_of_subsingleton]
  inv_hom_id := by simp

Left unitor isomorphism for binary products with terminal object

Informal description

For any object $P$ in a category $\mathcal{C}$ that has binary products and a terminal object $\top_{\mathcal{C}}$, there is a natural isomorphism between the product $\top_{\mathcal{C}} \times P$ and $P$. The isomorphism is given by: - The forward morphism is the second projection $\mathrm{snd} \colon \top_{\mathcal{C}} \times P \to P$. - The inverse morphism is the unique morphism $\mathrm{prod.lift}\,(\mathrm{terminal.from}\,P)\,\mathrm{id}_P \colon P \to \top_{\mathcal{C}} \times P$ induced by the universal property of the product. This isomorphism satisfies the usual coherence conditions for a unitor in a monoidal category.

CategoryTheory.Limits.prod.rightUnitor definition

(P : C) [HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ C ≅ P

Full source

/-- The right unitor isomorphism for binary products with the terminal object. -/
@[simps]
def prod.rightUnitor (P : C) [HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ CP ⨯ ⊤_ C ≅ P where
  hom := prod.fst
  inv := prod.lift (𝟙 _) (terminal.from P)
  hom_inv_id := by apply prod.hom_ext <;> simp [eq_iff_true_of_subsingleton]
  inv_hom_id := by simp

Right unitor isomorphism for binary products with terminal object

Informal description

The right unitor isomorphism for binary products with the terminal object is an isomorphism between the product $P \times \top_{\mathcal{C}}$ and $P$ in a category $\mathcal{C}$ that has binary products and a terminal object $\top_{\mathcal{C}}$. The forward morphism is the first projection $\pi_1: P \times \top_{\mathcal{C}} \to P$, and the inverse morphism is induced by the identity on $P$ and the universal morphism from $P$ to $\top_{\mathcal{C}}$.

CategoryTheory.Limits.prod.leftUnitor_hom_naturality theorem

[HasBinaryProducts C] (f : X ⟶ Y) : prod.map (𝟙 _) f ≫ (prod.leftUnitor Y).hom = (prod.leftUnitor X).hom ≫ f

Full source

@[reassoc]
theorem prod.leftUnitor_hom_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    prod.mapprod.map (𝟙 _) f ≫ (prod.leftUnitor Y).hom = (prod.leftUnitor X).hom ≫ f :=
  prod.map_snd _ _

Naturality of the Left Unitor Isomorphism with Respect to Morphisms

Informal description

Let $\mathcal{C}$ be a category with binary products. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, the following diagram commutes: \[ \text{prod.map}\, \text{id}_{\top_{\mathcal{C}}}\, f \circ \text{leftUnitor}_Y = \text{leftUnitor}_X \circ f \] where: - $\text{prod.map}\, \text{id}_{\top_{\mathcal{C}}}\, f \colon \top_{\mathcal{C}} \times X \to \top_{\mathcal{C}} \times Y$ is the product map induced by the identity on $\top_{\mathcal{C}}$ and $f$, - $\text{leftUnitor}_X \colon \top_{\mathcal{C}} \times X \to X$ is the left unitor isomorphism at $X$, - $\text{leftUnitor}_Y \colon \top_{\mathcal{C}} \times Y \to Y$ is the left unitor isomorphism at $Y$.

CategoryTheory.Limits.prod.leftUnitor_inv_naturality theorem

[HasBinaryProducts C] (f : X ⟶ Y) : (prod.leftUnitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.leftUnitor Y).inv

Full source

@[reassoc]
theorem prod.leftUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    (prod.leftUnitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.leftUnitor Y).inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

Naturality of the Inverse Left Unitor Isomorphism for Binary Products with Terminal Object

Informal description

Let $\mathcal{C}$ be a category with binary products. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, the following diagram commutes: \[ \lambda_X^{-1} \circ \mathrm{prod.map}\, \mathrm{id}_{\top_{\mathcal{C}}}\, f = f \circ \lambda_Y^{-1} \] where: - $\lambda_X \colon \top_{\mathcal{C}} \times X \to X$ and $\lambda_Y \colon \top_{\mathcal{C}} \times Y \to Y$ are the left unitor isomorphisms, - $\mathrm{prod.map}\, \mathrm{id}_{\top_{\mathcal{C}}}\, f \colon \top_{\mathcal{C}} \times X \to \top_{\mathcal{C}} \times Y$ is the product map induced by the identity on $\top_{\mathcal{C}}$ and $f$.

CategoryTheory.Limits.prod.rightUnitor_hom_naturality theorem

[HasBinaryProducts C] (f : X ⟶ Y) : prod.map f (𝟙 _) ≫ (prod.rightUnitor Y).hom = (prod.rightUnitor X).hom ≫ f

Full source

@[reassoc]
theorem prod.rightUnitor_hom_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    prod.mapprod.map f (𝟙 _) ≫ (prod.rightUnitor Y).hom = (prod.rightUnitor X).hom ≫ f :=
  prod.map_fst _ _

Naturality of the Right Unitor Isomorphism for Binary Products with Terminal Object

Informal description

Let $\mathcal{C}$ be a category with binary products. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, the following diagram commutes: \[ \mathrm{prod.map}\,f\,\mathrm{id} \circ \rho_Y = \rho_X \circ f \] where: - $\rho_X \colon X \times \top_{\mathcal{C}} \to X$ and $\rho_Y \colon Y \times \top_{\mathcal{C}} \to Y$ are the right unitor isomorphisms, - $\mathrm{prod.map}\,f\,\mathrm{id} \colon X \times \top_{\mathcal{C}} \to Y \times \top_{\mathcal{C}}$ is the product map induced by $f$ and the identity morphism on $\top_{\mathcal{C}}$.

CategoryTheory.Limits.prod_rightUnitor_inv_naturality theorem

[HasBinaryProducts C] (f : X ⟶ Y) : (prod.rightUnitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.rightUnitor Y).inv

Full source

@[reassoc]
theorem prod_rightUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    (prod.rightUnitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.rightUnitor Y).inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]

Naturality of the Inverse Right Unitor Isomorphism for Binary Products with Terminal Object

Informal description

Let $\mathcal{C}$ be a category with binary products. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, the following diagram commutes: \[ \rho_X^{-1} \circ \mathrm{prod.map}\,f\,\mathrm{id} = f \circ \rho_Y^{-1} \] where: - $\rho_X^{-1} \colon X \to X \times \top_{\mathcal{C}}$ and $\rho_Y^{-1} \colon Y \to Y \times \top_{\mathcal{C}}$ are the inverse morphisms of the right unitor isomorphisms, - $\mathrm{prod.map}\,f\,\mathrm{id} \colon X \times \top_{\mathcal{C}} \to Y \times \top_{\mathcal{C}}$ is the product map induced by $f$ and the identity morphism on $\top_{\mathcal{C}}$.

CategoryTheory.Limits.prod.triangle theorem

 [HasBinaryProducts C] (X Y : C) :
  (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) (prod.leftUnitor Y).hom = prod.map (prod.rightUnitor X).hom (𝟙 Y)

Full source

theorem prod.triangle [HasBinaryProducts C] (X Y : C) :
    (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) (prod.leftUnitor Y).hom =
      prod.map (prod.rightUnitor X).hom (𝟙 Y) := by
  ext <;> simp

Triangle Identity for Binary Products with Terminal Object

Informal description

In a category $\mathcal{C}$ with binary products and a terminal object $\top_{\mathcal{C}}$, the following diagram commutes for any objects $X$ and $Y$: \[ \alpha_{X,\top_{\mathcal{C}},Y} \circ \mathrm{id}_X \times \lambda_Y = \rho_X \times \mathrm{id}_Y \] where: - $\alpha_{X,\top_{\mathcal{C}},Y} \colon (X \times \top_{\mathcal{C}}) \times Y \to X \times (\top_{\mathcal{C}} \times Y)$ is the associator isomorphism, - $\lambda_Y \colon \top_{\mathcal{C}} \times Y \to Y$ is the left unitor isomorphism, - $\rho_X \colon X \times \top_{\mathcal{C}} \to X$ is the right unitor isomorphism.

CategoryTheory.Limits.coprod.braiding definition

(P Q : C) : P ⨿ Q ≅ Q ⨿ P

Full source

/-- The braiding isomorphism which swaps a binary coproduct. -/
@[simps]
def coprod.braiding (P Q : C) : P ⨿ QP ⨿ Q ≅ Q ⨿ P where
  hom := coprod.desc coprod.inr coprod.inl
  inv := coprod.desc coprod.inr coprod.inl

Braiding isomorphism for binary coproducts

Informal description

Given two objects $P$ and $Q$ in a category $\mathcal{C}$ with binary coproducts, the braiding isomorphism $\mathrm{coprod.braiding}\,P\,Q \colon P \sqcup Q \to Q \sqcup P$ is defined by the universal property of coproducts, where the morphism is induced by swapping the inclusion maps $\mathrm{inr} \colon Q \to Q \sqcup P$ and $\mathrm{inl} \colon P \to Q \sqcup P$. The inverse morphism is similarly defined by swapping the inclusions again, ensuring that the composition yields the identity morphism.

CategoryTheory.Limits.coprod.symmetry' theorem

(P Q : C) : coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q)

Full source

@[reassoc]
theorem coprod.symmetry' (P Q : C) :
    coprod.desccoprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
  (coprod.braiding _ _).hom_inv_id

Identity via Double Swap of Coproduct Components

Informal description

For any objects $P$ and $Q$ in a category $\mathcal{C}$ with binary coproducts, the composition of the coproduct universal morphisms $\mathrm{coprod.desc}\,(\mathrm{coprod.inr})\,(\mathrm{coprod.inl})$ with itself equals the identity morphism on $P \sqcup Q$. In other words, the morphism $P \sqcup Q \to Q \sqcup P \to P \sqcup Q$ obtained by first swapping the components and then swapping back is the identity morphism.

CategoryTheory.Limits.coprod.symmetry theorem

(P Q : C) : (coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _

Full source

/-- The braiding isomorphism is symmetric. -/
theorem coprod.symmetry (P Q : C) : (coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
  coprod.symmetry' _ _

Symmetry of Coproduct Braiding Isomorphism

Informal description

For any objects $P$ and $Q$ in a category $\mathcal{C}$ with binary coproducts, the composition of the braiding isomorphism $P \sqcup Q \to Q \sqcup P$ with its inverse $Q \sqcup P \to P \sqcup Q$ equals the identity morphism on $P \sqcup Q$.

CategoryTheory.Limits.coprod.associator definition

(P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R

Full source

/-- The associator isomorphism for binary coproducts. -/
@[simps]
def coprod.associator (P Q R : C) : (P ⨿ Q) ⨿ R(P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R where
  hom := coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr)
  inv := coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr)

Associator isomorphism for binary coproducts

Informal description

The associator isomorphism for binary coproducts in a category $\mathcal{C}$ is a natural isomorphism between the objects $(P \sqcup Q) \sqcup R$ and $P \sqcup (Q \sqcup R)$. The homomorphism part is constructed using the universal property of coproducts, mapping: - The left inclusion of $(P \sqcup Q) \sqcup R$ to the left inclusion of $P \sqcup (Q \sqcup R)$ composed with the left inclusion. - The right inclusion of $(P \sqcup Q) \sqcup R$ to the right inclusion of $P \sqcup (Q \sqcup R)$ composed with the right inclusion. The inverse is similarly constructed by mapping: - The left inclusion of $P \sqcup (Q \sqcup R)$ to the left inclusion composed with the left inclusion. - The right inclusion of $P \sqcup (Q \sqcup R)$ to the right inclusion composed with the left inclusion and the right inclusion.

CategoryTheory.Limits.coprod.pentagon theorem

 (W X Y Z : C) :
  coprod.map (coprod.associator W X Y).hom (𝟙 Z) ≫
      (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) (coprod.associator X Y Z).hom =
    (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom

Full source

theorem coprod.pentagon (W X Y Z : C) :
    coprod.mapcoprod.map (coprod.associator W X Y).hom (𝟙 Z) ≫
        (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) (coprod.associator X Y Z).hom =
      (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom := by
  simp

Pentagon Identity for Coproduct Associators

Informal description

For any objects $W, X, Y, Z$ in a category $\mathcal{C}$ with binary coproducts, the following pentagon diagram commutes: \[ \begin{CD} (W \sqcup X) \sqcup Y \sqcup Z @>{\text{coprod.map}(\alpha_{WXY}, \text{id}_Z)}>> W \sqcup (X \sqcup Y) \sqcup Z \\ @V{\alpha_{(W \sqcup X)YZ}}VV @VV{\alpha_{W(X \sqcup Y)Z}}V \\ (W \sqcup X) \sqcup (Y \sqcup Z) @. W \sqcup (X \sqcup Y \sqcup Z) \\ @V{\alpha_{WX(Y \sqcup Z)}}VV @VV{\text{coprod.map}(\text{id}_W, \alpha_{XYZ})}V \\ W \sqcup X \sqcup (Y \sqcup Z) @= W \sqcup X \sqcup (Y \sqcup Z) \end{CD} \] where $\alpha_{ABC}$ denotes the associator isomorphism $(A \sqcup B) \sqcup C \cong A \sqcup (B \sqcup C)$.

CategoryTheory.Limits.coprod.associator_naturality theorem

 {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
  coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
    (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃)

Full source

theorem coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
    (f₃ : X₃ ⟶ Y₃) :
    coprod.mapcoprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
      (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) := by
  simp

Naturality of the Associator Isomorphism for Binary Coproducts

Informal description

For any objects $X_1, X_2, X_3, Y_1, Y_2, Y_3$ in a category $\mathcal{C}$ with binary coproducts, and morphisms $f_1 \colon X_1 \to Y_1$, $f_2 \colon X_2 \to Y_2$, $f_3 \colon X_3 \to Y_3$, the following diagram commutes: \[ \mathrm{coprod.map}\,(\mathrm{coprod.map}\,f_1\,f_2)\,f_3 \circ \mathrm{associator}_{Y_1,Y_2,Y_3} = \mathrm{associator}_{X_1,X_2,X_3} \circ \mathrm{coprod.map}\,f_1\,(\mathrm{coprod.map}\,f_2\,f_3) \] where $\mathrm{associator}_{A,B,C} \colon (A \sqcup B) \sqcup C \to A \sqcup (B \sqcup C)$ is the associator isomorphism for coproducts.

CategoryTheory.Limits.coprod.leftUnitor definition

(P : C) : (⊥_ C) ⨿ P ≅ P

Full source

/-- The left unitor isomorphism for binary coproducts with the initial object. -/
@[simps]
def coprod.leftUnitor (P : C) : (⊥_ C) ⨿ P(⊥_ C) ⨿ P ≅ P where
  hom := coprod.desc (initial.to P) (𝟙 _)
  inv := coprod.inr
  hom_inv_id := by apply coprod.hom_ext <;> simp [eq_iff_true_of_subsingleton]
  inv_hom_id := by simp

Left unitor isomorphism for binary coproducts with initial object

Informal description

The left unitor isomorphism for binary coproducts in a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ is an isomorphism between $\bot_{\mathcal{C}} \sqcup P$ and $P$, for any object $P$ in $\mathcal{C}$. The forward morphism is induced by the universal property of the coproduct, combining the unique morphism from $\bot_{\mathcal{C}}$ to $P$ and the identity morphism on $P$. The inverse morphism is the right inclusion of $P$ into the coproduct.

CategoryTheory.Limits.coprod.rightUnitor definition

(P : C) : P ⨿ ⊥_ C ≅ P

Full source

/-- The right unitor isomorphism for binary coproducts with the initial object. -/
@[simps]
def coprod.rightUnitor (P : C) : P ⨿ ⊥_ CP ⨿ ⊥_ C ≅ P where
  hom := coprod.desc (𝟙 _) (initial.to P)
  inv := coprod.inl
  hom_inv_id := by apply coprod.hom_ext <;> simp [eq_iff_true_of_subsingleton]
  inv_hom_id := by simp

Right unitor isomorphism for binary coproducts

Informal description

The right unitor isomorphism for binary coproducts states that for any object $P$ in a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, the coproduct $P \sqcup \bot_{\mathcal{C}}$ is isomorphic to $P$. The isomorphism consists of: - A morphism from $P \sqcup \bot_{\mathcal{C}}$ to $P$ given by the coproduct universal property applied to the identity morphism on $P$ and the unique morphism from $\bot_{\mathcal{C}}$ to $P$. - An inverse morphism from $P$ to $P \sqcup \bot_{\mathcal{C}}$ given by the left inclusion map. This isomorphism satisfies the standard coherence conditions for unitors in a monoidal category structure.

CategoryTheory.Limits.coprod.triangle theorem

 (X Y : C) :
  (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) (coprod.leftUnitor Y).hom =
    coprod.map (coprod.rightUnitor X).hom (𝟙 Y)

Full source

theorem coprod.triangle (X Y : C) :
    (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) (coprod.leftUnitor Y).hom =
      coprod.map (coprod.rightUnitor X).hom (𝟙 Y) := by
  ext <;> simp

Triangle Identity for Coproduct Unitors and Associator

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, the following diagram commutes: \[ (X \sqcup \bot_{\mathcal{C}}) \sqcup Y \xrightarrow{\text{associator hom}} X \sqcup (\bot_{\mathcal{C}} \sqcup Y) \xrightarrow{\text{id}_X \sqcup \text{left unitor hom}} X \sqcup Y \] equals \[ (X \sqcup \bot_{\mathcal{C}}) \sqcup Y \xrightarrow{\text{right unitor hom} \sqcup \text{id}_Y} X \sqcup Y \]

CategoryTheory.Limits.prod.functor definition

: C ⥤ C ⥤ C

Full source

/-- The binary product functor. -/
@[simps]
def prod.functor : C ⥤ C ⥤ C where
  obj X :=
    { obj := fun Y => X ⨯ Y
      map := fun {_ _} => prod.map (𝟙 X) }
  map f :=
    { app := fun T => prod.map f (𝟙 T) }

Binary product functor

Informal description

The binary product functor is a functor from a category $\mathcal{C}$ to the functor category $\mathcal{C} \Rightarrow \mathcal{C}$. For each object $X$ in $\mathcal{C}$, it assigns the functor that maps an object $Y$ to the product $X \times Y$ and a morphism $g \colon Y \to Z$ to the morphism $\text{id}_X \times g \colon X \times Y \to X \times Z$. For a morphism $f \colon X \to W$ in $\mathcal{C}$, the functor maps an object $T$ to the morphism $f \times \text{id}_T \colon X \times T \to W \times T$.

CategoryTheory.Limits.prod.functorLeftComp definition

(X Y : C) : prod.functor.obj (X ⨯ Y) ≅ prod.functor.obj Y ⋙ prod.functor.obj X

Full source

/-- The product functor can be decomposed. -/
def prod.functorLeftComp (X Y : C) :
    prod.functorprod.functor.obj (X ⨯ Y) ≅ prod.functor.obj Y ⋙ prod.functor.obj X :=
  NatIso.ofComponents (prod.associator _ _)

Natural isomorphism for reassociation of binary product functors

Informal description

For any objects $ X $ and $ Y $ in a category $ \mathcal{C} $ with binary products, there is a natural isomorphism between the functor $ \mathrm{prod.functor.obj}(X \times Y) $ and the composition of functors $ \mathrm{prod.functor.obj}\,Y \circ \mathrm{prod.functor.obj}\,X $. This isomorphism is given by the associator for binary products, $ \mathrm{prod.associator}\,X\,Y $, which provides a natural way to reassociate the product $ (X \times Y) \times Z $ to $ X \times (Y \times Z) $ for any object $ Z $ in $ \mathcal{C} $.

CategoryTheory.Limits.coprod.functor definition

: C ⥤ C ⥤ C

Full source

/-- The binary coproduct functor. -/
@[simps]
def coprod.functor : C ⥤ C ⥤ C where
  obj X :=
    { obj := fun Y => X ⨿ Y
      map := fun {_ _} => coprod.map (𝟙 X) }
  map f := { app := fun T => coprod.map f (𝟙 T) }

Binary coproduct functor

Informal description

The binary coproduct functor is a functor from a category $\mathcal{C}$ to the functor category $\mathcal{C} \to \mathcal{C}$. For each object $X$ in $\mathcal{C}$, it assigns the functor that maps an object $Y$ to the coproduct $X \sqcup Y$, and maps a morphism $g \colon Y \to Z$ to the morphism $\text{id}_X \sqcup g \colon X \sqcup Y \to X \sqcup Z$. For a morphism $f \colon X \to W$ in $\mathcal{C}$, the functor maps it to the natural transformation whose component at $Y$ is $f \sqcup \text{id}_Y \colon X \sqcup Y \to W \sqcup Y$.

CategoryTheory.Limits.coprod.functorLeftComp definition

(X Y : C) : coprod.functor.obj (X ⨿ Y) ≅ coprod.functor.obj Y ⋙ coprod.functor.obj X

Full source

/-- The coproduct functor can be decomposed. -/
def coprod.functorLeftComp (X Y : C) :
    coprod.functorcoprod.functor.obj (X ⨿ Y) ≅ coprod.functor.obj Y ⋙ coprod.functor.obj X :=
  NatIso.ofComponents (coprod.associator _ _)

Associativity isomorphism for binary coproduct functors

Informal description

For any objects $ X $ and $ Y $ in a category $ \mathcal{C} $, there is a natural isomorphism between the functor $ \mathrm{coprod.functor.obj}\,(X \sqcup Y) $ and the composition of functors $ \mathrm{coprod.functor.obj}\,Y \circ \mathrm{coprod.functor.obj}\,X $. This isomorphism is given by the associator isomorphism for binary coproducts, which maps $ (X \sqcup Y) \sqcup Z $ to $ X \sqcup (Y \sqcup Z) $ for any object $ Z $ in $ \mathcal{C} $.

CategoryTheory.Limits.prodComparison definition

 (F : C ⥤ D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] : F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B

Full source

/-- The product comparison morphism.

In `CategoryTheory/Limits/Preserves` we show this is always an iso iff F preserves binary products.
-/
def prodComparison (F : C ⥤ D) (A B : C) [HasBinaryProduct A B]
    [HasBinaryProduct (F.obj A) (F.obj B)] : F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B :=
  prod.lift (F.map prod.fst) (F.map prod.snd)

Product comparison morphism

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories, and objects $ A $ and $ B $ in $ \mathcal{C} $ that have a binary product $ A \times B $, the product comparison morphism $ \text{prodComparison}\,F\,A\,B $ is the canonical morphism from $ F(A \times B) $ to the product $ F(A) \times F(B) $ in $ \mathcal{D} $, induced by the universal property of the product $ F(A) \times F(B) $. Specifically, it is the unique morphism such that the following diagram commutes: \[ F(A \times B) \xrightarrow{\text{prodComparison}\,F\,A\,B} F(A) \times F(B) \] where the morphism is constructed using the projections $ F(\pi_1) \colon F(A \times B) \to F(A) $ and $ F(\pi_2) \colon F(A \times B) \to F(B) $.

CategoryTheory.Limits.prodComparison_fst theorem

: prodComparison F A B ≫ prod.fst = F.map prod.fst

Full source

@[reassoc (attr := simp)]
theorem prodComparison_fst : prodComparisonprodComparison F A B ≫ prod.fst = F.map prod.fst :=
  prod.lift_fst _ _

Commutativity of Product Comparison with First Projection

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary products, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For objects $A$ and $B$ in $\mathcal{C}$, the composition of the product comparison morphism $\mathrm{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B)$ with the first projection $\pi_1 \colon F(A) \times F(B) \to F(A)$ equals the image under $F$ of the first projection $\pi_1 \colon A \times B \to A$, i.e., \[ \mathrm{prodComparison}\,F\,A\,B \circ \pi_1 = F(\pi_1). \]

CategoryTheory.Limits.prodComparison_snd theorem

: prodComparison F A B ≫ prod.snd = F.map prod.snd

Full source

@[reassoc (attr := simp)]
theorem prodComparison_snd : prodComparisonprodComparison F A B ≫ prod.snd = F.map prod.snd :=
  prod.lift_snd _ _

Commutativity of product comparison with second projection: $\mathrm{prodComparison}\,F\,A\,B \circ \pi_2 = F(\pi_2)$

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories, and objects $A$ and $B$ in $\mathcal{C}$ that have a binary product $A \times B$, the composition of the product comparison morphism $\mathrm{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B)$ with the second projection $\pi_2 \colon F(A) \times F(B) \to F(B)$ equals the image under $F$ of the second projection $\pi_2 \colon A \times B \to B$, i.e., \[ \mathrm{prodComparison}\,F\,A\,B \circ \pi_2 = F(\pi_2). \]

CategoryTheory.Limits.prodComparison_natural theorem

 (f : A ⟶ A') (g : B ⟶ B') :
  F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Full source

/-- Naturality of the `prodComparison` morphism in both arguments. -/
@[reassoc]
theorem prodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
    F.map (prod.map f g) ≫ prodComparison F A' B' =
      prodComparisonprodComparison F A B ≫ prod.map (F.map f) (F.map g) := by
  rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]

Naturality of the Product Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary products, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any morphisms $f \colon A \to A'$ and $g \colon B \to B'$ in $\mathcal{C}$, the following diagram commutes: \[ F(A \times B) \xrightarrow{\mathrm{prodComparison}\,F\,A\,B} F(A) \times F(B) \] \[ F(f \times g) \downarrow \quad \quad \quad \downarrow F(f) \times F(g) \] \[ F(A' \times B') \xrightarrow{\mathrm{prodComparison}\,F\,A'\,B'} F(A') \times F(B') \] That is, the product comparison morphism is natural in both arguments: \[ F(f \times g) \circ \mathrm{prodComparison}\,F\,A'\,B' = \mathrm{prodComparison}\,F\,A\,B \circ (F(f) \times F(g)). \]

CategoryTheory.Limits.prodComparisonNatTrans definition

 [HasBinaryProducts C] [HasBinaryProducts D] (F : C ⥤ D) (A : C) :
  prod.functor.obj A ⋙ F ⟶ F ⋙ prod.functor.obj (F.obj A)

Full source

/-- The product comparison morphism from `F(A ⨯ -)` to `FA ⨯ F-`, whose components are given by
`prodComparison`.
-/
@[simps]
def prodComparisonNatTrans [HasBinaryProducts C] [HasBinaryProducts D] (F : C ⥤ D) (A : C) :
    prod.functorprod.functor.obj A ⋙ Fprod.functor.obj A ⋙ F ⟶ F ⋙ prod.functor.obj (F.obj A) where
  app B := prodComparison F A B
  naturality f := by simp [prodComparison_natural]

Natural transformation of product comparison morphisms

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories with binary products, and an object $ A $ in $ \mathcal{C} $, the natural transformation $ \text{prodComparisonNatTrans}\,F\,A $ is defined between the functors $ \text{prod.functor.obj}\,A \circ F $ and $ F \circ \text{prod.functor.obj}\,(F.obj\,A) $. For each object $ B $ in $ \mathcal{C} $, the component of this natural transformation at $ B $ is the product comparison morphism $ \text{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B) $. The naturality condition states that for any morphism $ f \colon B \to B' $ in $ \mathcal{C} $, the following diagram commutes: \[ F(A \times B) \xrightarrow{\text{prodComparison}\,F\,A\,B} F(A) \times F(B) \] \[ F(\text{id}_A \times f) \downarrow \quad \quad \quad \downarrow F(\text{id}_A) \times F(f) \] \[ F(A \times B') \xrightarrow{\text{prodComparison}\,F\,A\,B'} F(A) \times F(B') \]

CategoryTheory.Limits.inv_prodComparison_map_fst theorem

[IsIso (prodComparison F A B)] : inv (prodComparison F A B) ≫ F.map prod.fst = prod.fst

Full source

@[reassoc]
theorem inv_prodComparison_map_fst [IsIso (prodComparison F A B)] :
    invinv (prodComparison F A B) ≫ F.map prod.fst = prod.fst := by simp [IsIso.inv_comp_eq]

Inverse Product Comparison Preserves First Projection

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary products, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For objects $A$ and $B$ in $\mathcal{C}$, if the product comparison morphism $\mathrm{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B)$ is an isomorphism, then the composition of its inverse with $F(\pi_1)$ equals the first projection $\pi_1 \colon F(A) \times F(B) \to F(A)$, i.e., \[ (\mathrm{prodComparison}\,F\,A\,B)^{-1} \circ F(\pi_1) = \pi_1. \]

CategoryTheory.Limits.inv_prodComparison_map_snd theorem

[IsIso (prodComparison F A B)] : inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd

Full source

@[reassoc]
theorem inv_prodComparison_map_snd [IsIso (prodComparison F A B)] :
    invinv (prodComparison F A B) ≫ F.map prod.snd = prod.snd := by simp [IsIso.inv_comp_eq]

Inverse Product Comparison Preserves Second Projection: $(\mathrm{prodComparison}\,F\,A\,B)^{-1} \circ F(\pi_2) = \pi_2$

Informal description

For a functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories, and objects $A$ and $B$ in $\mathcal{C}$ with binary products, if the product comparison morphism $\mathrm{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B)$ is an isomorphism, then the composition of its inverse with $F(\pi_2)$ equals the second projection $\pi_2 \colon F(A) \times F(B) \to F(B)$, i.e., \[ (\mathrm{prodComparison}\,F\,A\,B)^{-1} \circ F(\pi_2) = \pi_2. \]

CategoryTheory.Limits.prodComparison_inv_natural theorem

 (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)] [IsIso (prodComparison F A' B')] :
  inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')

Full source

/-- If the product comparison morphism is an iso, its inverse is natural. -/
@[reassoc]
theorem prodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)]
    [IsIso (prodComparison F A' B')] :
    invinv (prodComparison F A B) ≫ F.map (prod.map f g) =
      prod.mapprod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B') := by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Naturality of Inverse Product Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary products, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any morphisms $f \colon A \to A'$ and $g \colon B \to B'$ in $\mathcal{C}$, if the product comparison morphisms $\mathrm{prodComparison}\,F\,A\,B$ and $\mathrm{prodComparison}\,F\,A'\,B'$ are isomorphisms, then the following diagram commutes: \[ F(A \times B) \xrightarrow{\mathrm{inv}(\mathrm{prodComparison}\,F\,A\,B)} F(A) \times F(B) \] \[ F(f \times g) \downarrow \quad \quad \quad \downarrow F(f) \times F(g) \] \[ F(A' \times B') \xrightarrow{\mathrm{inv}(\mathrm{prodComparison}\,F\,A'\,B')} F(A') \times F(B') \] That is, the inverse of the product comparison morphism is natural in both arguments: \[ \mathrm{inv}(\mathrm{prodComparison}\,F\,A\,B) \circ F(f \times g) = (F(f) \times F(g)) \circ \mathrm{inv}(\mathrm{prodComparison}\,F\,A'\,B'). \]

CategoryTheory.Limits.prodComparisonNatIso definition

 [HasBinaryProducts C] [HasBinaryProducts D] (A : C) [∀ B, IsIso (prodComparison F A B)] :
  prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A)

Full source

/-- The natural isomorphism `F(A ⨯ -) ≅ FA ⨯ F-`, provided each `prodComparison F A B` is an
isomorphism (as `B` changes).
-/
@[simps]
def prodComparisonNatIso [HasBinaryProducts C] [HasBinaryProducts D] (A : C)
    [∀ B, IsIso (prodComparison F A B)] :
    prod.functorprod.functor.obj A ⋙ Fprod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A) := by
  refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }
  apply NatIso.isIso_of_isIso_app

Natural isomorphism for product-preserving functors

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories with binary products, and an object $ A $ in $ \mathcal{C} $, if for every object $ B $ in $ \mathcal{C} $ the product comparison morphism $ \text{prodComparison}\,F\,A\,B \colon F(A \times B) \to F(A) \times F(B) $ is an isomorphism, then there is a natural isomorphism between the functors $ \text{prod.functor.obj}\,A \circ F $ and $ F \circ \text{prod.functor.obj}\,(F.obj\,A) $. This natural isomorphism expresses that $ F $ preserves products in the sense that $ F(A \times -) $ is naturally isomorphic to $ F(A) \times F(-) $.

CategoryTheory.Limits.prodComparison_comp theorem

: prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Full source

theorem prodComparison_comp :
    prodComparison (F ⋙ G) A B =
      G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B) := by
  unfold prodComparison
  ext <;> simp [← G.map_comp]

Composition Law for Product Comparison Morphisms

Informal description

For functors $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$ between categories with binary products, and objects $A$ and $B$ in $\mathcal{C}$, the product comparison morphism for the composed functor $F \circ G$ satisfies: \[ \mathrm{prodComparison}\,(F \circ G)\,A\,B = G(\mathrm{prodComparison}\,F\,A\,B) \circ \mathrm{prodComparison}\,G\,(F(A))\,(F(B)). \]

CategoryTheory.Limits.coprodComparison definition

 (F : C ⥤ D) (A B : C) [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] :
  F.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B)

Full source

/-- The coproduct comparison morphism.

In `Mathlib/CategoryTheory/Limits/Preserves/` we show
this is always an iso iff F preserves binary coproducts.
-/
def coprodComparison (F : C ⥤ D) (A B : C) [HasBinaryCoproduct A B]
    [HasBinaryCoproduct (F.obj A) (F.obj B)] : F.obj A ⨿ F.obj BF.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B) :=
  coprod.desc (F.map coprod.inl) (F.map coprod.inr)

Coproduct comparison morphism

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories with binary coproducts, and objects $ A $ and $ B $ in $ \mathcal{C} $, the coproduct comparison morphism $ \text{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B) $ is the unique morphism induced by the universal property of the coproduct $ F(A) \sqcup F(B) $, defined by composing the images of the coproduct inclusions $ \text{inl} \colon A \to A \sqcup B $ and $ \text{inr} \colon B \to A \sqcup B $ under $ F $.

CategoryTheory.Limits.coprodComparison_inl theorem

: coprod.inl ≫ coprodComparison F A B = F.map coprod.inl

Full source

@[reassoc (attr := simp)]
theorem coprodComparison_inl : coprod.inlcoprod.inl ≫ coprodComparison F A B = F.map coprod.inl :=
  coprod.inl_desc _ _

Commutativity of Left Coprojection with Coproduct Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary coproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For objects $A$ and $B$ in $\mathcal{C}$, the composition of the left coprojection $\mathrm{inl} \colon F(A) \to F(A) \sqcup F(B)$ with the coproduct comparison morphism $\mathrm{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ equals the image under $F$ of the left coprojection $\mathrm{inl} \colon A \to A \sqcup B$, i.e., \[ \mathrm{inl} \circ \mathrm{coprodComparison}\,F\,A\,B = F(\mathrm{inl}). \]

CategoryTheory.Limits.coprodComparison_inr theorem

: coprod.inr ≫ coprodComparison F A B = F.map coprod.inr

Full source

@[reassoc (attr := simp)]
theorem coprodComparison_inr : coprod.inrcoprod.inr ≫ coprodComparison F A B = F.map coprod.inr :=
  coprod.inr_desc _ _

Commutativity of Right Coprojection with Coproduct Comparison Morphism

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories with binary coproducts, and objects $A$ and $B$ in $\mathcal{C}$, the composition of the right coprojection $\iota_r \colon F(B) \to F(A) \sqcup F(B)$ with the coproduct comparison morphism $\text{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ equals the image under $F$ of the right coprojection $\iota_r \colon B \to A \sqcup B$ in $\mathcal{C}$.

CategoryTheory.Limits.coprodComparison_natural theorem

 (f : A ⟶ A') (g : B ⟶ B') :
  coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'

Full source

/-- Naturality of the coprod_comparison morphism in both arguments. -/
@[reassoc]
theorem coprodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
    coprodComparisoncoprodComparison F A B ≫ F.map (coprod.map f g) =
      coprod.mapcoprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B' := by
  rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]

Naturality of the Coproduct Comparison Morphism with Respect to Morphisms in the Base Category

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary coproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any morphisms $f \colon A \to A'$ and $g \colon B \to B'$ in $\mathcal{C}$, the following diagram commutes: \[ \mathrm{coprodComparison}\,F\,A\,B \circ F(\mathrm{coprod.map}\,f\,g) = \mathrm{coprod.map}\,F(f)\,F(g) \circ \mathrm{coprodComparison}\,F\,A'\,B' \] where: - $\mathrm{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ is the coproduct comparison morphism, - $\mathrm{coprod.map}\,f\,g \colon A \sqcup B \to A' \sqcup B'$ is the coproduct map induced by $f$ and $g$, - $\mathrm{coprod.map}\,F(f)\,F(g) \colon F(A) \sqcup F(B) \to F(A') \sqcup F(B')$ is the coproduct map induced by $F(f)$ and $F(g)$.

CategoryTheory.Limits.coprodComparisonNatTrans definition

 [HasBinaryCoproducts C] [HasBinaryCoproducts D] (F : C ⥤ D) (A : C) :
  F ⋙ coprod.functor.obj (F.obj A) ⟶ coprod.functor.obj A ⋙ F

Full source

/-- The coproduct comparison morphism from `FA ⨿ F-` to `F(A ⨿ -)`, whose components are given by
`coprodComparison`.
-/
@[simps]
def coprodComparisonNatTrans [HasBinaryCoproducts C] [HasBinaryCoproducts D] (F : C ⥤ D) (A : C) :
    F ⋙ coprod.functor.obj (F.obj A)F ⋙ coprod.functor.obj (F.obj A) ⟶ coprod.functor.obj A ⋙ F where
  app B := coprodComparison F A B
  naturality f := by simp [coprodComparison_natural]

Coproduct Comparison Natural Transformation

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories with binary coproducts, and an object $ A $ in $ \mathcal{C} $, the coproduct comparison natural transformation $ \text{coprodComparisonNatTrans}\,F\,A $ is a natural transformation from the functor $ F \circ (\text{coprod.functor}\,(F\,A)) $ to the functor $ (\text{coprod.functor}\,A) \circ F $. Its component at each object $ B $ in $ \mathcal{C} $ is the coproduct comparison morphism $ \text{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B) $.

CategoryTheory.Limits.map_inl_inv_coprodComparison theorem

[IsIso (coprodComparison F A B)] : F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl

Full source

@[reassoc]
theorem map_inl_inv_coprodComparison [IsIso (coprodComparison F A B)] :
    F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl := by simp [IsIso.inv_comp_eq]

Inverse of Coproduct Comparison Morphism Composes with Left Inclusion to Yield Left Coprojection

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary coproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For objects $A$ and $B$ in $\mathcal{C}$, if the coproduct comparison morphism $\mathrm{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ is an isomorphism, then the composition of $F(\mathrm{inl})$ with its inverse equals the left coprojection $\mathrm{inl} \colon F(A) \to F(A) \sqcup F(B)$, i.e., \[ F(\mathrm{inl}) \circ (\mathrm{coprodComparison}\,F\,A\,B)^{-1} = \mathrm{inl}. \]

CategoryTheory.Limits.map_inr_inv_coprodComparison theorem

[IsIso (coprodComparison F A B)] : F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr

Full source

@[reassoc]
theorem map_inr_inv_coprodComparison [IsIso (coprodComparison F A B)] :
    F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr := by simp [IsIso.inv_comp_eq]

Commutativity of Right Coprojection with Inverse Coproduct Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary coproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For objects $A$ and $B$ in $\mathcal{C}$, suppose the coproduct comparison morphism $\text{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ is an isomorphism. Then, the composition of the image of the right coprojection $F(\iota_r) \colon F(B) \to F(A \sqcup B)$ with the inverse of the coproduct comparison morphism equals the right coprojection $\iota_r \colon F(B) \to F(A) \sqcup F(B)$ in $\mathcal{D}$. That is, the following diagram commutes: \[ F(\iota_r) \circ (\text{coprodComparison}\,F\,A\,B)^{-1} = \iota_r. \]

CategoryTheory.Limits.coprodComparison_inv_natural theorem

 (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)] [IsIso (coprodComparison F A' B')] :
  inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
    F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')

Full source

/-- If the coproduct comparison morphism is an iso, its inverse is natural. -/
@[reassoc]
theorem coprodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)]
    [IsIso (coprodComparison F A' B')] :
    invinv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
      F.map (coprod.map f g) ≫ inv (coprodComparison F A' B') := by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]

Naturality of the Inverse Coproduct Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with binary coproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any morphisms $f \colon A \to A'$ and $g \colon B \to B'$ in $\mathcal{C}$, if the coproduct comparison morphisms $\mathrm{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B)$ and $\mathrm{coprodComparison}\,F\,A'\,B' \colon F(A') \sqcup F(B') \to F(A' \sqcup B')$ are isomorphisms, then the following diagram commutes: \[ (\mathrm{coprodComparison}\,F\,A\,B)^{-1} \circ \mathrm{coprod.map}\,F(f)\,F(g) = F(\mathrm{coprod.map}\,f\,g) \circ (\mathrm{coprodComparison}\,F\,A'\,B')^{-1}. \]

CategoryTheory.Limits.coprodComparisonNatIso definition

 [HasBinaryCoproducts C] [HasBinaryCoproducts D] (A : C) [∀ B, IsIso (coprodComparison F A B)] :
  F ⋙ coprod.functor.obj (F.obj A) ≅ coprod.functor.obj A ⋙ F

Full source

/-- The natural isomorphism `FA ⨿ F- ≅ F(A ⨿ -)`, provided each `coprodComparison F A B` is an
isomorphism (as `B` changes).
-/
@[simps]
def coprodComparisonNatIso [HasBinaryCoproducts C] [HasBinaryCoproducts D] (A : C)
    [∀ B, IsIso (coprodComparison F A B)] :
    F ⋙ coprod.functor.obj (F.obj A)F ⋙ coprod.functor.obj (F.obj A) ≅ coprod.functor.obj A ⋙ F :=
  { @asIso _ _ _ _ _ (NatIso.isIso_of_isIso_app ..) with hom := coprodComparisonNatTrans F A }

Natural isomorphism induced by coproduct comparison isomorphisms

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ between categories with binary coproducts and an object $ A $ in $ \mathcal{C} $, if for every object $ B $ in $ \mathcal{C} $ the coproduct comparison morphism $ \text{coprodComparison}\,F\,A\,B \colon F(A) \sqcup F(B) \to F(A \sqcup B) $ is an isomorphism, then there is a natural isomorphism $ F \circ (\text{coprod.functor}\,(F\,A)) \cong (\text{coprod.functor}\,A) \circ F $. This isomorphism is constructed from the coproduct comparison natural transformation $ \text{coprodComparisonNatTrans}\,F\,A $, which is componentwise an isomorphism under the given hypothesis.

CategoryTheory.Over.coprodObj definition

[HasBinaryCoproducts C] {A : C} : Over A → Over A ⥤ Over A

Full source

/-- Auxiliary definition for `Over.coprod`. -/
@[simps]
noncomputable def Over.coprodObj [HasBinaryCoproducts C] {A : C} :
    Over A → OverOver A ⥤ Over A :=
  fun f =>
  { obj := fun g => Over.mk (coprod.desc f.hom g.hom)
    map := fun k => Over.homMk (coprod.map (𝟙 _) k.left) }

Functor sending an object in the over category to its coproduct with another object

Informal description

Given an object $f \colon Y \to A$ in the over category of $A$ in a category $\mathcal{C}$ with binary coproducts, the functor $\mathrm{coprodObj}\,f$ sends another object $g \colon Z \to A$ in the over category to the object $\mathrm{coprod.desc}\,f\,g \colon Y \sqcup Z \to A$, where $\mathrm{coprod.desc}$ is the universal morphism induced by the coproduct $Y \sqcup Z$ and the morphisms $f$ and $g$. For a morphism $k \colon g_1 \to g_2$ in the over category, the functor maps it to the morphism $\mathrm{coprod.map}\,(\mathrm{id}_Y)\,k \colon \mathrm{coprod.desc}\,f\,g_1 \to \mathrm{coprod.desc}\,f\,g_2$, where $\mathrm{coprod.map}$ is the morphism induced by the universal property of the coproduct.

CategoryTheory.Over.coprod definition

[HasBinaryCoproducts C] {A : C} : Over A ⥤ Over A ⥤ Over A

Full source

/-- A category with binary coproducts has a functorial `sup` operation on over categories. -/
@[simps]
noncomputable def Over.coprod [HasBinaryCoproducts C] {A : C} : OverOver A ⥤ Over A ⥤ Over A where
  obj f := Over.coprodObj f
  map k :=
    { app := fun g => Over.homMk (coprod.map k.left (𝟙 _)) (by
        dsimp; rw [coprod.map_desc, Category.id_comp, Over.w k])
      naturality := fun f g k => by
        ext
        dsimp; simp }
  map_id X := by
    ext
    dsimp; simp
  map_comp f g := by
    ext
    dsimp; simp

Binary coproduct functor in the over category

Informal description

Given a category $\mathcal{C}$ with binary coproducts and an object $A$ in $\mathcal{C}$, the functor $\mathrm{coprod} \colon \mathrm{Over}\,A \to \mathrm{Over}\,A \to \mathrm{Over}\,A$ sends an object $f \colon Y \to A$ in the over category of $A$ to the functor $\mathrm{coprodObj}\,f$, which maps another object $g \colon Z \to A$ to the coproduct object $\mathrm{coprod.desc}\,f\,g \colon Y \sqcup Z \to A$. For a morphism $k \colon f_1 \to f_2$ in $\mathrm{Over}\,A$, the functor $\mathrm{coprod}$ maps it to the natural transformation whose component at $g$ is the morphism $\mathrm{coprod.map}\,k.left\,\mathrm{id}_Z \colon \mathrm{coprod.desc}\,f_1\,g \to \mathrm{coprod.desc}\,f_2\,g$ in $\mathrm{Over}\,A$.

CategoryTheory.Limits.BinaryFan.op abbrev

(c : BinaryFan X Y) : BinaryCofan (op X) (op Y)

Full source

/-- A binary fan gives a binary cofan in the opposite category. -/
protected abbrev BinaryFan.op (c : BinaryFan X Y) : BinaryCofan (op X) (op Y) :=
  .mk c.fst.op c.snd.op

Opposite Construction of Binary Fan Yields Binary Cofan in Opposite Category

Informal description

Given a binary fan $c$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the opposite construction yields a binary cofan for the opposite objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$ in the opposite category $\mathcal{C}^{\mathrm{op}}$. Specifically: - The cone point $P$ of $c$ becomes the cocone point $\mathrm{op}\,P$ in $\mathcal{C}^{\mathrm{op}}$. - The projections $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ become coprojections $\mathrm{op}\,\pi_1 \colon \mathrm{op}\,X \to \mathrm{op}\,P$ and $\mathrm{op}\,\pi_2 \colon \mathrm{op}\,Y \to \mathrm{op}\,P$ in $\mathcal{C}^{\mathrm{op}}$.

CategoryTheory.Limits.BinaryCofan.op abbrev

(c : BinaryCofan X Y) : BinaryFan (op X) (op Y)

Full source

/-- A binary cofan gives a binary fan in the opposite category. -/
protected abbrev BinaryCofan.op (c : BinaryCofan X Y) : BinaryFan (op X) (op Y) :=
  .mk c.inl.op c.inr.op

Opposite of a Binary Cofan Yields a Binary Fan

Informal description

Given a binary cofan $c$ for objects $X$ and $Y$ in a category $\mathcal{C}$, the operation $\mathrm{op}$ constructs a binary fan for the opposite objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$ in the opposite category $\mathcal{C}^{\mathrm{op}}$. Specifically: - The cocone point $P$ of $c$ becomes the cone point $\mathrm{op}\,P$ in the opposite category. - The coprojections $\iota_X \colon X \to P$ and $\iota_Y \colon Y \to P$ become projections $\mathrm{op}\,\iota_X \colon \mathrm{op}\,P \to \mathrm{op}\,X$ and $\mathrm{op}\,\iota_Y \colon \mathrm{op}\,P \to \mathrm{op}\,Y$ in $\mathcal{C}^{\mathrm{op}}$.

CategoryTheory.Limits.BinaryFan.unop abbrev

(c : BinaryFan (op X) (op Y)) : BinaryCofan X Y

Full source

/-- A binary fan in the opposite category gives a binary cofan. -/
protected abbrev BinaryFan.unop (c : BinaryFan (op X) (op Y)) : BinaryCofan X Y :=
  .mk c.fst.unop c.snd.unop

Conversion of Binary Fan in Opposite Category to Binary Cofan in Original Category

Informal description

Given a binary fan $c$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ with objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$, the operation $\mathrm{BinaryFan.unop}$ constructs a binary cofan in the original category $\mathcal{C}$ with objects $X$ and $Y$.

CategoryTheory.Limits.BinaryCofan.unop abbrev

(c : BinaryCofan (op X) (op Y)) : BinaryFan X Y

Full source

/-- A binary cofan in the opposite category gives a binary fan. -/
protected abbrev BinaryCofan.unop (c : BinaryCofan (op X) (op Y)) : BinaryFan X Y :=
  .mk c.inl.unop c.inr.unop

Conversion from Opposite Binary Cofan to Binary Fan

Informal description

Given a binary cofan $c$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ with objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$, the operation returns a binary fan in the original category $\mathcal{C}$ with objects $X$ and $Y$. Specifically, the binary fan consists of: - A vertex $P$ in $\mathcal{C}$ (the cone point) - Two projections $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ obtained by unopposing the coprojections of $c$.

CategoryTheory.Limits.BinaryFan.op_mk theorem

(π₁ : P ⟶ X) (π₂ : P ⟶ Y) : BinaryFan.op (mk π₁ π₂) = .mk π₁.op π₂.op

Full source

@[simp] lemma BinaryFan.op_mk (π₁ : P ⟶ X) (π₂ : P ⟶ Y) :
    BinaryFan.op (mk π₁ π₂) = .mk π₁.op π₂.op := rfl

Opposite of Binary Fan Construction Equals Binary Cofan Construction in Opposite Category

Informal description

Given morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ in a category $\mathcal{C}$, the opposite of the binary fan constructed from $\pi_1$ and $\pi_2$ is equal to the binary cofan in the opposite category $\mathcal{C}^{\mathrm{op}}$ constructed from the opposite morphisms $\pi_1^{\mathrm{op}} \colon X^{\mathrm{op}} \to P^{\mathrm{op}}$ and $\pi_2^{\mathrm{op}} \colon Y^{\mathrm{op}} \to P^{\mathrm{op}}$. In symbols: \[ \mathrm{BinaryFan.op}\,(\mathrm{mk}\,\pi_1\,\pi_2) = \mathrm{mk}\,\pi_1^{\mathrm{op}}\,\pi_2^{\mathrm{op}} \]

CategoryTheory.Limits.BinaryFan.unop_mk theorem

(π₁ : op P ⟶ op X) (π₂ : op P ⟶ op Y) : BinaryFan.unop (mk π₁ π₂) = .mk π₁.unop π₂.unop

Full source

@[simp] lemma BinaryFan.unop_mk (π₁ : opop P ⟶ op X) (π₂ : opop P ⟶ op Y) :
    BinaryFan.unop (mk π₁ π₂) = .mk π₁.unop π₂.unop := rfl

Unopposite of Binary Fan Construction Equals Binary Cofan Construction via Unopposite Morphisms

Informal description

Given morphisms $\pi_1 \colon \mathrm{op}\,P \to \mathrm{op}\,X$ and $\pi_2 \colon \mathrm{op}\,P \to \mathrm{op}\,Y$ in the opposite category $\mathcal{C}^{\mathrm{op}}$, the unopposite of the binary fan constructed from $\pi_1$ and $\pi_2$ is equal to the binary cofan in $\mathcal{C}$ constructed from the unopposite morphisms $\pi_1.\mathrm{unop} \colon X \to P$ and $\pi_2.\mathrm{unop} \colon Y \to P$.

CategoryTheory.Limits.BinaryCofan.op_mk theorem

(ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : BinaryCofan.op (mk ι₁ ι₂) = .mk ι₁.op ι₂.op

Full source

@[simp] lemma BinaryCofan.op_mk (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) :
    BinaryCofan.op (mk ι₁ ι₂) = .mk ι₁.op ι₂.op := rfl

Opposite of Binary Cofan Construction Equals Binary Fan Construction of Opposites

Informal description

Given two morphisms $\iota_1 \colon X \to P$ and $\iota_2 \colon Y \to P$ in a category $\mathcal{C}$, the opposite of the binary cofan constructed from $\iota_1$ and $\iota_2$ is equal to the binary fan in the opposite category $\mathcal{C}^{\mathrm{op}}$ constructed from the opposite morphisms $\iota_1^{\mathrm{op}} \colon \mathrm{op}\,X \to \mathrm{op}\,P$ and $\iota_2^{\mathrm{op}} \colon \mathrm{op}\,Y \to \mathrm{op}\,P$.

CategoryTheory.Limits.BinaryCofan.unop_mk theorem

(ι₁ : op X ⟶ op P) (ι₂ : op Y ⟶ op P) : BinaryCofan.unop (mk ι₁ ι₂) = .mk ι₁.unop ι₂.unop

Full source

@[simp] lemma BinaryCofan.unop_mk (ι₁ : opop X ⟶ op P) (ι₂ : opop Y ⟶ op P) :
    BinaryCofan.unop (mk ι₁ ι₂) = .mk ι₁.unop ι₂.unop := rfl

Unopposite of Binary Cofan Construction via Coprojections Equals Binary Fan Construction via Unopposite Coprojections

Informal description

Given morphisms $\iota_1 \colon \mathrm{op}\,X \to \mathrm{op}\,P$ and $\iota_2 \colon \mathrm{op}\,Y \to \mathrm{op}\,P$ in the opposite category $\mathcal{C}^{\mathrm{op}}$, the unopposite of the binary cofan constructed from these morphisms is equal to the binary fan in $\mathcal{C}$ constructed from their unopposite morphisms $\iota_1^{\mathrm{unop}} \colon P \to X$ and $\iota_2^{\mathrm{unop}} \colon P \to Y$.

CategoryTheory.Limits.BinaryFan.IsLimit.op definition

{c : BinaryFan X Y} (hc : IsLimit c) : IsColimit c.op

Full source

/-- If a `BinaryFan` is a limit, then its opposite is a colimit. -/
protected def BinaryFan.IsLimit.op {c : BinaryFan X Y} (hc : IsLimit c) : IsColimit c.op :=
  BinaryCofan.isColimitMk (fun s ↦ (hc.lift s.unop).op)
    (fun _ ↦ Quiver.Hom.unop_inj (by simp)) (fun _ ↦ Quiver.Hom.unop_inj (by simp))
    (fun s m h₁ h₂ ↦ Quiver.Hom.unop_inj
      (BinaryFan.IsLimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

Opposite of a binary fan limit is a binary cofan colimit

Informal description

Given a binary fan $c$ for objects $X$ and $Y$ in a category $\mathcal{C}$, if $c$ is a limit cone, then its opposite construction $c^{\mathrm{op}}$ is a colimit cocone in the opposite category $\mathcal{C}^{\mathrm{op}}$. Specifically, the colimit cocone $c^{\mathrm{op}}$ consists of: - The cocone point $P^{\mathrm{op}}$ (the opposite of the cone point $P$ of $c$) - The coprojections $\pi_1^{\mathrm{op}} \colon X^{\mathrm{op}} \to P^{\mathrm{op}}$ and $\pi_2^{\mathrm{op}} \colon Y^{\mathrm{op}} \to P^{\mathrm{op}}$ (the opposites of the projections $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ in $\mathcal{C}$)

CategoryTheory.Limits.BinaryCofan.IsColimit.op definition

{c : BinaryCofan X Y} (hc : IsColimit c) : IsLimit c.op

Full source

/-- If a `BinaryCofan` is a colimit, then its opposite is a limit. -/
protected def BinaryCofan.IsColimit.op {c : BinaryCofan X Y} (hc : IsColimit c) : IsLimit c.op :=
  BinaryFan.isLimitMk (fun s ↦ (hc.desc s.unop).op)
    (fun _ ↦ Quiver.Hom.unop_inj (by simp)) (fun _ ↦ Quiver.Hom.unop_inj (by simp))
    (fun s m h₁ h₂ ↦ Quiver.Hom.unop_inj
      (BinaryCofan.IsColimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

Opposite of a colimit binary cofan is a limit binary fan

Informal description

Given a binary cofan $c$ for objects $X$ and $Y$ in a category $\mathcal{C}$, if $c$ is a colimit cocone, then its opposite $c^{\mathrm{op}}$ is a limit cone in the opposite category $\mathcal{C}^{\mathrm{op}}$. Specifically, the construction provides: 1. For any binary fan $s$ in $\mathcal{C}^{\mathrm{op}}$, a morphism from $s$ to $c^{\mathrm{op}}$ obtained by taking the opposite of the universal morphism from $s^{\mathrm{unop}}$ to $c$ in $\mathcal{C}$. 2. Proofs that this morphism satisfies the required factorization properties with respect to the projections of $s$. 3. A uniqueness condition ensuring that any morphism satisfying these properties must coincide with the constructed one.

CategoryTheory.Limits.BinaryFan.IsLimit.unop definition

{c : BinaryFan (op X) (op Y)} (hc : IsLimit c) : IsColimit c.unop

Full source

/-- If a `BinaryFan` in the opposite category is a limit, then its `unop` is a colimit. -/
protected def BinaryFan.IsLimit.unop {c : BinaryFan (op X) (op Y)} (hc : IsLimit c) :
    IsColimit c.unop :=
  BinaryCofan.isColimitMk (fun s ↦ (hc.lift s.op).unop)
    (fun _ ↦ Quiver.Hom.op_inj (by simp)) (fun _ ↦ Quiver.Hom.op_inj (by simp))
    (fun s m h₁ h₂ ↦ Quiver.Hom.op_inj
      (BinaryFan.IsLimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

Unopposite of a limit binary fan is a colimit binary cofan

Informal description

Given a binary fan $c$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ with objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$, if $c$ is a limit cone, then its unopposite $c.\mathrm{unop}$ is a colimit cocone in the original category $\mathcal{C}$.

CategoryTheory.Limits.BinaryCofan.IsColimit.unop definition

{c : BinaryCofan (op X) (op Y)} (hc : IsColimit c) : IsLimit c.unop

Full source

/-- If a `BinaryCofan` in the opposite category is a colimit, then its `unop` is a limit. -/
protected def BinaryCofan.IsColimit.unop {c : BinaryCofan (op X) (op Y)} (hc : IsColimit c) :
    IsLimit c.unop :=
  BinaryFan.isLimitMk (fun s ↦ (hc.desc s.op).unop)
    (fun _ ↦ Quiver.Hom.op_inj (by simp)) (fun _ ↦ Quiver.Hom.op_inj (by simp))
    (fun s m h₁ h₂ ↦ Quiver.Hom.op_inj
      (BinaryCofan.IsColimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

Unopposite of a colimit binary cofan is a limit binary fan

Informal description

Given a binary cofan $c$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ for objects $\mathrm{op}\,X$ and $\mathrm{op}\,Y$, if $c$ is a colimit cocone in $\mathcal{C}^{\mathrm{op}}$, then its unopposite $c.\mathrm{unop}$ is a limit cone in the original category $\mathcal{C}$ for objects $X$ and $Y$.

References