doc-next-gen

Mathlib.CategoryTheory.Products.Basic

Module docstring

{"# Cartesian products of categories

We define the category instance on C × D when C and D are categories.

We define: * sectL C Z : the functor C ⥤ C × D given by X ↦ ⟨X, Z⟩ * sectR Z D : the functor D ⥤ C × D given by Y ↦ ⟨Z, Y⟩ * fst : the functor ⟨X, Y⟩ ↦ X * snd : the functor ⟨X, Y⟩ ↦ Y * swap : the functor C × D ⥤ D × C given by ⟨X, Y⟩ ↦ ⟨Y, X⟩ (and the fact this is an equivalence)

We further define evaluation : C ⥤ (C ⥤ D) ⥤ D and evaluationUncurried : C × (C ⥤ D) ⥤ D, and products of functors and natural transformations, written F.prod G and α.prod β. "}

CategoryTheory.prod instance
: Category.{max v₁ v₂} (C × D)
Full source 
/-- `prod C D` gives the cartesian product of two categories. -/
@[simps (config := { notRecursive := [] }) Hom id_fst id_snd comp_fst comp_snd, stacks 001K]
instance prod : Category.{max v₁ v₂} (C × D) where
  Hom X Y := (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)
  id X := ⟨𝟙 X.1, 𝟙 X.2⟩
  comp f g := (f.1 ≫ g.1, f.2 ≫ g.2)
The Category Structure on Cartesian Product of Categories
Informal description
For any two categories $C$ and $D$, the cartesian product $C \times D$ forms a category where the objects are pairs $(X, Y)$ with $X \in C$ and $Y \in D$, and the morphisms are pairs $(f, g)$ where $f$ is a morphism in $C$ and $g$ is a morphism in $D$.
CategoryTheory.prod.hom_ext theorem
{X Y : C × D} {f g : X ⟶ Y} (h₁ : f.1 = g.1) (h₂ : f.2 = g.2) : f = g
Full source 
@[ext]
lemma prod.hom_ext {X Y : C × D} {f g : X ⟶ Y} (h₁ : f.1 = g.1) (h₂ : f.2 = g.2) : f = g := by
  dsimp
  ext <;> assumption
Extensionality of Morphisms in Product Categories
Informal description
Let $C$ and $D$ be categories, and let $X, Y$ be objects in the product category $C \times D$. For any two morphisms $f, g : X \to Y$ in $C \times D$, if the components of $f$ and $g$ are equal in both $C$ and $D$ (i.e., $f_1 = g_1$ in $C$ and $f_2 = g_2$ in $D$), then $f = g$.
CategoryTheory.prod_id theorem
(X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y)
Full source 
/-- Two rfl lemmas that cannot be generated by `@[simps]`. -/
@[simp]
theorem prod_id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) :=
  rfl
Identity Morphism in Product Category Decomposes as Pair of Identities
Informal description
For any objects $X$ in a category $C$ and $Y$ in a category $D$, the identity morphism on the pair $(X, Y)$ in the product category $C \times D$ is equal to the pair of identity morphisms $(\mathrm{id}_X, \mathrm{id}_Y)$.
CategoryTheory.prod_comp theorem
{P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2)
Full source 
@[simp]
theorem prod_comp {P Q R : C} {S T U : D} (f : (P, S)(P, S) ⟶ (Q, T)) (g : (Q, T)(Q, T) ⟶ (R, U)) :
    f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) :=
  rfl
Composition in Product Category Decomposes Componentwise
Informal description
For any objects $P, Q, R$ in category $C$ and $S, T, U$ in category $D$, and morphisms $f \colon (P, S) \to (Q, T)$ and $g \colon (Q, T) \to (R, U)$ in the product category $C \times D$, the composition $f \gg g$ is equal to the pair $(f_1 \gg g_1, f_2 \gg g_2)$, where $f_1$ and $g_1$ are the components of $f$ and $g$ in $C$, and $f_2$ and $g_2$ are the components in $D$.
CategoryTheory.isIso_prod_iff theorem
{P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} : IsIso f ↔ IsIso f.1 ∧ IsIso f.2
Full source 
theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S)(P, S) ⟶ (Q, T)} :
    IsIsoIsIso f ↔ IsIso f.1 ∧ IsIso f.2 := by
  constructor
  · rintro ⟨g, hfg, hgf⟩
    simp? at hfg hgf says simp only [prod_Hom, prod_comp, prod_id, Prod.mk.injEq] at hfg hgf
    rcases hfg with ⟨hfg₁, hfg₂⟩
    rcases hgf with ⟨hgf₁, hgf₂⟩
    exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
  · rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
    dsimp at hfg₁ hgf₁ hfg₂ hgf₂
    refine ⟨⟨(g₁, g₂), ?_, ?_⟩⟩
    repeat { simp; constructor; assumption; assumption }
Isomorphism in Product Category iff Components Are Isomorphisms
Informal description
A morphism $f \colon (P, S) \to (Q, T)$ in the product category $C \times D$ is an isomorphism if and only if its first component $f_1 \colon P \to Q$ is an isomorphism in $C$ and its second component $f_2 \colon S \to T$ is an isomorphism in $D$.
CategoryTheory.prod.etaIso definition
(X : C × D) : (X.1, X.2) ≅ X
Full source 
/-- The isomorphism between `(X.1, X.2)` and `X`. -/
@[simps]
def prod.etaIso (X : C × D) : (X.1, X.2)(X.1, X.2) ≅ X where
  hom := (𝟙 _, 𝟙 _)
  inv := (𝟙 _, 𝟙 _)
Isomorphism between component pair and product object
Informal description
For any object $X$ in the product category $C \times D$, there is a natural isomorphism between the pair $(X.1, X.2)$ and $X$ itself, where the morphisms in both directions are given by the identity morphisms on each component.
CategoryTheory.Iso.prod definition
{P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S) ≅ (Q, T)
Full source 
/-- Construct an isomorphism in `C × D` out of two isomorphisms in `C` and `D`. -/
@[simps]
def Iso.prod {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S)(P, S) ≅ (Q, T) where
  hom := (f.hom, g.hom)
  inv := (f.inv, g.inv)
Product of isomorphisms in a product category
Informal description
Given isomorphisms $f \colon P \cong Q$ in category $\mathcal{C}$ and $g \colon S \cong T$ in category $\mathcal{D}$, the isomorphism $\text{Iso.prod}\, f\, g$ is the product isomorphism $(P, S) \cong (Q, T)$ in the product category $\mathcal{C} \times \mathcal{D}$, where the morphism component is the pair $(f_{\text{hom}}, g_{\text{hom}})$ and the inverse component is the pair $(f_{\text{inv}}, g_{\text{inv}})$.
CategoryTheory.uniformProd instance
: Category (C × D)
Full source 
/-- `Category.uniformProd C D` is an additional instance specialised so both factors have the same
universe levels. This helps typeclass resolution.
-/
instance uniformProd : Category (C × D) :=
  CategoryTheory.prod C D
The Category Structure on Cartesian Product of Categories with Same Universe Levels
Informal description
For any two categories $C$ and $D$ with the same universe levels, the cartesian product $C \times D$ forms a category where the objects are pairs $(X, Y)$ with $X \in C$ and $Y \in D$, and the morphisms are pairs $(f, g)$ where $f$ is a morphism in $C$ and $g$ is a morphism in $D$.
CategoryTheory.Prod.sectL definition
(C : Type u₁) [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (Z : D) : C ⥤ C × D
Full source 
/-- `sectL C Z` is the functor `C ⥤ C × D` given by `X ↦ (X, Z)`. -/
@[simps]
def sectL (C : Type u₁) [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (Z : D) : C ⥤ C × D where
  obj X := (X, Z)
  map f := (f, 𝟙 Z)
Left section functor for product categories
Informal description
Given a category $\mathcal{C}$ and an object $Z$ in a category $\mathcal{D}$, the functor $\text{sectL}_{\mathcal{C}, Z}$ maps each object $X$ in $\mathcal{C}$ to the pair $(X, Z)$ in the product category $\mathcal{C} \times \mathcal{D}$, and each morphism $f \colon X \to Y$ in $\mathcal{C}$ to the pair $(f, \text{id}_Z)$ in $\mathcal{C} \times \mathcal{D}$.
CategoryTheory.Prod.sectR definition
{C : Type u₁} [Category.{v₁} C] (Z : C) (D : Type u₂) [Category.{v₂} D] : D ⥤ C × D
Full source 
/-- `sectR Z D` is the functor `D ⥤ C × D` given by `Y ↦ (Z, Y)` . -/
@[simps]
def sectR {C : Type u₁} [Category.{v₁} C] (Z : C) (D : Type u₂) [Category.{v₂} D] : D ⥤ C × D where
  obj X := (Z, X)
  map f := (𝟙 Z, f)
Right section functor of the product category
Informal description
Given a category $C$ with an object $Z \in C$ and another category $D$, the functor $\text{sectR}_Z D \colon D \to C \times D$ maps each object $X \in D$ to the pair $(Z, X)$ and each morphism $f \colon X \to Y$ in $D$ to the pair $(\text{id}_Z, f)$ in $C \times D$.
CategoryTheory.Prod.fst definition
: C × D ⥤ C
Full source 
/-- `fst` is the functor `(X, Y) ↦ X`. -/
@[simps]
def fst : C × DC × D ⥤ C where
  obj X := X.1
  map f := f.1
First projection functor
Informal description
The functor `fst` from the product category $C \times D$ to $C$ maps each object $(X, Y)$ to $X$ and each morphism $(f, g)$ to $f$.
CategoryTheory.Prod.snd definition
: C × D ⥤ D
Full source 
/-- `snd` is the functor `(X, Y) ↦ Y`. -/
@[simps]
def snd : C × DC × D ⥤ D where
  obj X := X.2
  map f := f.2
Second projection functor of product category
Informal description
The functor `snd` from the product category $C \times D$ to $D$ maps each object $(X, Y)$ to $Y$ and each morphism $(f, g)$ to $g$.
CategoryTheory.Prod.swap definition
: C × D ⥤ D × C
Full source 
/-- The functor swapping the factors of a cartesian product of categories, `C × D ⥤ D × C`. -/
@[simps]
def swap : C × DC × D ⥤ D × C where
  obj X := (X.2, X.1)
  map f := (f.2, f.1)
Swap functor for product categories
Informal description
The functor that swaps the components of objects and morphisms in the cartesian product category $C \times D$, mapping $(X, Y)$ to $(Y, X)$ and $(f, g)$ to $(g, f)$. This defines a functor from $C \times D$ to $D \times C$.
CategoryTheory.Prod.symmetry definition
: swap C D ⋙ swap D C ≅ 𝟭 (C × D)
Full source 
/-- Swapping the factors of a cartesian product of categories twice is naturally isomorphic
to the identity functor.
-/
@[simps]
def symmetry : swapswap C D ⋙ swap D Cswap C D ⋙ swap D C ≅ 𝟭 (C × D) where
  hom := { app := fun X => 𝟙 X }
  inv := { app := fun X => 𝟙 X }
Symmetry isomorphism for product categories
Informal description
The composition of the swap functor from $C \times D$ to $D \times C$ with the swap functor from $D \times C$ back to $C \times D$ is naturally isomorphic to the identity functor on $C \times D$. Specifically, for any object $X$ in $C \times D$, the isomorphism is given by the identity morphism $\text{id}_X$.
CategoryTheory.Prod.braiding definition
: C × D ≌ D × C
Full source 
/-- The equivalence, given by swapping factors, between `C × D` and `D × C`.
-/
@[simps]
def braiding : C × DC × D ≌ D × C where
  functor := swap C D
  inverse := swap D C
  unitIso := Iso.refl _
  counitIso := Iso.refl _
Equivalence between $C \times D$ and $D \times C$ via swapping
Informal description
The equivalence of categories between the cartesian product categories $C \times D$ and $D \times C$, given by swapping the components of objects and morphisms. This equivalence consists of: - The swap functor $F \colon C \times D \to D \times C$ mapping $(X, Y) \mapsto (Y, X)$ and $(f, g) \mapsto (g, f)$, - Its inverse functor $G \colon D \times C \to C \times D$ similarly swapping components, - The identity natural isomorphisms $\eta \colon \text{id}_{C \times D} \cong G \circ F$ and $\epsilon \colon F \circ G \cong \text{id}_{D \times C}$.
CategoryTheory.Prod.swapIsEquivalence instance
: (swap C D).IsEquivalence
Full source 
instance swapIsEquivalence : (swap C D).IsEquivalence :=
  (by infer_instance : (braiding C D).functor.IsEquivalence)
The Swap Functor is an Equivalence of Categories
Informal description
The swap functor $\text{swap} \colon C \times D \to D \times C$, which maps objects $(X, Y)$ to $(Y, X)$ and morphisms $(f, g)$ to $(g, f)$, is an equivalence of categories.
CategoryTheory.Prod.fac theorem
{x y : C × D} (f : x ⟶ y) : f = ((𝟙 x.1, f.2) : _ ⟶ ⟨x.1, y.2⟩) ≫ (f.1, 𝟙 y.2)
Full source 
/-- Any morphism in a product factors as a morphsim whose left component is an identity
followed by a morphism whose right component is an identity. -/
@[reassoc]
lemma fac {x y : C × D} (f : x ⟶ y) :
    f = ((𝟙 x.1, f.2) : _ ⟶ ⟨x.1, y.2⟩) ≫ (f.1, 𝟙 y.2) := by aesop
Factorization of Morphisms in Product Category via Identity Components
Informal description
For any morphism $f \colon (X, Y) \to (X', Y')$ in the product category $C \times D$, the morphism $f$ can be factored as the composition of $(1_X, f_2) \colon (X, Y) \to (X, Y')$ followed by $(f_1, 1_{Y'}) \colon (X, Y') \to (X', Y')$, where $f_1$ and $f_2$ are the components of $f$ in $C$ and $D$ respectively, and $1_X$ and $1_{Y'}$ are identity morphisms.
CategoryTheory.Prod.fac' theorem
{x y : C × D} (f : x ⟶ y) : f = ((f.1, 𝟙 x.2) : _ ⟶ ⟨y.1, x.2⟩) ≫ (𝟙 y.1, f.2)
Full source 
/-- Any morphism in a product factors as a morphsim whose right component is an identity
followed by a morphism whose left component is an identity. -/
@[reassoc]
lemma fac' {x y : C × D} (f : x ⟶ y) :
    f = ((f.1, 𝟙 x.2) : _ ⟶ ⟨y.1, x.2⟩) ≫ (𝟙 y.1, f.2) := by aesop
Factorization of Morphisms in Product Category via Identity Components
Informal description
For any morphism $f \colon (X_1, Y_1) \to (X_2, Y_2)$ in the product category $C \times D$, $f$ factors as the composition of $(f_1, \mathrm{id}_{Y_1}) \colon (X_1, Y_1) \to (X_2, Y_1)$ followed by $(\mathrm{id}_{X_2}, f_2) \colon (X_2, Y_1) \to (X_2, Y_2)$, where $f_1 \colon X_1 \to X_2$ and $f_2 \colon Y_1 \to Y_2$ are the components of $f$.
CategoryTheory.evaluation definition
: C ⥤ (C ⥤ D) ⥤ D
Full source 
/-- The "evaluation at `X`" functor, such that
`(evaluation.obj X).obj F = F.obj X`,
which is functorial in both `X` and `F`.
-/
@[simps]
def evaluation : C ⥤ (C ⥤ D) ⥤ D where
  obj X :=
    { obj := fun F => F.obj X
      map := fun α => α.app X }
  map {_} {_} f :=
    { app := fun F => F.map f }
Evaluation functor
Informal description
The evaluation functor, which takes an object $X$ in category $C$ and maps it to the functor that evaluates any functor $F \colon C \to D$ at $X$, i.e., $F \mapsto F(X)$. This functor is contravariant in $X$ and covariant in $F$.
CategoryTheory.evaluationUncurried definition
: C × (C ⥤ D) ⥤ D
Full source 
/-- The "evaluation of `F` at `X`" functor,
as a functor `C × (C ⥤ D) ⥤ D`.
-/
@[simps]
def evaluationUncurried : C × (C ⥤ D)C × (C ⥤ D) ⥤ D where
  obj p := p.2.obj p.1
  map := fun {x} {y} f => x.2.map f.1 ≫ f.2.app y.1
Uncurried evaluation functor
Informal description
The evaluation functor for a pair $(X, F)$ in the product category $C \times (C \ ⥤ \ D)$ maps to the object $F(X)$ in $D$. For a morphism $(f, \eta) \colon (X, F) \to (Y, G)$, the functor applies the morphism $f \colon X \to Y$ via $F$ and composes with the natural transformation $\eta$ evaluated at $Y$, resulting in $F(f) \circ \eta_Y \colon F(X) \to G(Y)$.
CategoryTheory.Functor.constCompEvaluationObj definition
(X : C) : Functor.const C ⋙ (evaluation C D).obj X ≅ 𝟭 D
Full source 
/-- The constant functor followed by the evaluation functor is just the identity. -/
@[simps!]
def Functor.constCompEvaluationObj (X : C) : Functor.constFunctor.const C ⋙ (evaluation C D).obj XFunctor.const C ⋙ (evaluation C D).obj X ≅ 𝟭 D :=
  NatIso.ofComponents fun _ => Iso.refl _
Constant functor composed with evaluation is identity
Informal description
For any object $X$ in category $C$, the composition of the constant functor with the evaluation functor at $X$ is naturally isomorphic to the identity functor on $D$. Specifically, the isomorphism is given by the identity morphism at each object in $D$.
CategoryTheory.Functor.prod definition
(F : A ⥤ B) (G : C ⥤ D) : A × C ⥤ B × D
Full source 
/-- The cartesian product of two functors. -/
@[simps]
def prod (F : A ⥤ B) (G : C ⥤ D) : A × CA × C ⥤ B × D where
  obj X := (F.obj X.1, G.obj X.2)
  map f := (F.map f.1, G.map f.2)

/- Because of limitations in Lean 3's handling of notations, we do not setup a notation `F × G`.
   You can use `F.prod G` as a "poor man's infix", or just write `functor.prod F G`. -/
Product of functors
Informal description
Given two functors $F \colon A \to B$ and $G \colon C \to D$, the product functor $F \times G \colon A \times C \to B \times D$ is defined by: - On objects: $(X, Y) \mapsto (F(X), G(Y))$ - On morphisms: $(f, g) \mapsto (F(f), G(g))$
CategoryTheory.Functor.prod' definition
(F : A ⥤ B) (G : A ⥤ C) : A ⥤ B × C
Full source 
/-- Similar to `prod`, but both functors start from the same category `A` -/
@[simps]
def prod' (F : A ⥤ B) (G : A ⥤ C) : A ⥤ B × C where
  obj a := (F.obj a, G.obj a)
  map f := (F.map f, G.map f)
Product of functors from the same category
Informal description
Given two functors $F \colon A \to B$ and $G \colon A \to C$ from the same category $A$, the functor $F \times G \colon A \to B \times C$ maps an object $a$ in $A$ to the pair $(F(a), G(a))$ in $B \times C$, and a morphism $f$ in $A$ to the pair of morphisms $(F(f), G(f))$ in $B \times C$.
CategoryTheory.Functor.prod'CompFst definition
(F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.fst B C ≅ F
Full source 
/-- The product `F.prod' G` followed by projection on the first component is isomorphic to `F` -/
@[simps!]
def prod'CompFst (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.fst B CF.prod' G ⋙ CategoryTheory.Prod.fst B C ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _
First projection of product functor is isomorphic to first factor
Informal description
For any two functors \( F \colon A \to B \) and \( G \colon A \to C \) from the same category \( A \), the composition of the product functor \( F \times G \colon A \to B \times C \) with the first projection functor \( \text{fst} \colon B \times C \to B \) is naturally isomorphic to \( F \). In other words, the diagram \[ A \xrightarrow{F \times G} B \times C \xrightarrow{\text{fst}} B \] is naturally isomorphic to \( F \).
CategoryTheory.Functor.prod'CompSnd definition
(F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.snd B C ≅ G
Full source 
/-- The product `F.prod' G` followed by projection on the second component is isomorphic to `G` -/
@[simps!]
def prod'CompSnd (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.snd B CF.prod' G ⋙ CategoryTheory.Prod.snd B C ≅ G :=
  NatIso.ofComponents fun _ => Iso.refl _
Second projection of product functor is isomorphic to second functor
Informal description
For any two functors $F \colon A \to B$ and $G \colon A \to C$ from the same category $A$, the composition of the product functor $F \times G \colon A \to B \times C$ with the second projection functor $\text{snd} \colon B \times C \to C$ is naturally isomorphic to $G$. In other words, the diagram \[ A \xrightarrow{F \times G} B \times C \xrightarrow{\text{snd}} C \] is naturally isomorphic to $G \colon A \to C$.
CategoryTheory.Functor.diag definition
: C ⥤ C × C
Full source 
/-- The diagonal functor. -/
@[simps! obj map]
def diag : C ⥤ C × C :=
  (𝟭 C).prod' (𝟭 C)
Diagonal functor
Informal description
The diagonal functor from a category $C$ to the product category $C \times C$, which maps an object $X$ in $C$ to the pair $(X, X)$ and a morphism $f$ in $C$ to the pair $(f, f)$.
CategoryTheory.NatTrans.prod definition
{F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I
Full source 
/-- The cartesian product of two natural transformations. -/
@[simps! app_fst app_snd]
def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I where
  app X := (α.app X.1, β.app X.2)

/- Again, it is inadvisable in Lean 3 to setup a notation `α × β`;
   use instead `α.prod β` or `NatTrans.prod α β`. -/
Product of natural transformations
Informal description
Given two natural transformations $\alpha \colon F \to G$ between functors $F, G \colon A \to B$ and $\beta \colon H \to I$ between functors $H, I \colon C \to D$, the product natural transformation $\alpha \times \beta \colon F \times H \to G \times I$ is defined by: - For each object $(X, Y) \in A \times C$, the component at $(X, Y)$ is $(\alpha_X, \beta_Y)$.
CategoryTheory.NatTrans.prod' definition
{F G : A ⥤ B} {H K : A ⥤ C} (α : F ⟶ G) (β : H ⟶ K) : F.prod' H ⟶ G.prod' K
Full source 
/-- The cartesian product of two natural transformations where both functors have the
same source. -/
@[simps! app_fst app_snd]
def prod' {F G : A ⥤ B} {H K : A ⥤ C} (α : F ⟶ G) (β : H ⟶ K) : F.prod' H ⟶ G.prod' K where
  app X := (α.app X, β.app X)
Product of natural transformations between functors from the same category
Informal description
Given two natural transformations $\alpha \colon F \to G$ and $\beta \colon H \to K$ between functors $F, G \colon A \to B$ and $H, K \colon A \to C$ respectively, the product natural transformation $\alpha \times \beta \colon F \times H \to G \times K$ is defined such that for any object $X$ in $A$, its component at $X$ is the pair $(\alpha_X, \beta_X)$.
CategoryTheory.prodFunctor definition
: (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D
Full source 
/-- The cartesian product functor between functor categories -/
@[simps]
def prodFunctor : (A ⥤ B) × (C ⥤ D)(A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D where
  obj FG := FG.1.prod FG.2
  map nm := NatTrans.prod nm.1 nm.2
Product functor construction
Informal description
The functor that takes a pair of functors $(F, G)$ from $(A \to B) \times (C \to D)$ and returns their product functor $F \times G \colon A \times C \to B \times D$, defined by: - On objects: $(X, Y) \mapsto (F(X), G(Y))$ - On morphisms: $(f, g) \mapsto (F(f), G(g))$
CategoryTheory.NatIso.prod definition
{F F' : A ⥤ B} {G G' : C ⥤ D} (e₁ : F ≅ F') (e₂ : G ≅ G') : F.prod G ≅ F'.prod G'
Full source 
/-- The cartesian product of two natural isomorphisms. -/
@[simps]
def prod {F F' : A ⥤ B} {G G' : C ⥤ D} (e₁ : F ≅ F') (e₂ : G ≅ G') :
    F.prod G ≅ F'.prod G' where
  hom := NatTrans.prod e₁.hom e₂.hom
  inv := NatTrans.prod e₁.inv e₂.inv
Product of natural isomorphisms
Informal description
Given two natural isomorphisms $e_1 \colon F \cong F'$ between functors $F, F' \colon A \to B$ and $e_2 \colon G \cong G'$ between functors $G, G' \colon C \to D$, the product natural isomorphism $e_1 \times e_2 \colon F \times G \cong F' \times G'$ is defined by: - The forward component is the product of the forward components of $e_1$ and $e_2$. - The backward component is the product of the backward components of $e_1$ and $e_2$.
CategoryTheory.Equivalence.prod definition
(E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D
Full source 
/-- The cartesian product of two equivalences of categories. -/
@[simps]
def prod (E₁ : A ≌ B) (E₂ : C ≌ D) : A × CA × C ≌ B × D where
  functor := E₁.functor.prod E₂.functor
  inverse := E₁.inverse.prod E₂.inverse
  unitIso := NatIso.prod E₁.unitIso E₂.unitIso
  counitIso := NatIso.prod E₁.counitIso E₂.counitIso
Product of equivalences of categories
Informal description
Given two equivalences of categories $E_1 \colon A \simeq B$ and $E_2 \colon C \simeq D$, their cartesian product forms an equivalence $E_1 \times E_2 \colon A \times C \simeq B \times D$, where: - The forward functor is the product of the forward functors $E_1.functor \times E_2.functor$, - The inverse functor is the product of the inverse functors $E_1.inverse \times E_2.inverse$, - The unit isomorphism is the product of the unit isomorphisms $E_1.unitIso \times E_2.unitIso$, - The counit isomorphism is the product of the counit isomorphisms $E_1.counitIso \times E_2.counitIso$.
CategoryTheory.flipCompEvaluation definition
(F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a
Full source 
/-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
@[simps!]
def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj aF.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=
  NatIso.ofComponents fun b => Iso.refl _
Flipped functor composition with evaluation is isomorphic to original functor
Informal description
For any functor $F \colon A \to (B \to C)$ and any object $a \in A$, the composition of the flipped functor $F^{\text{flip}} \colon B \to (A \to C)$ with the evaluation functor at $a$ is naturally isomorphic to the original functor $F$ applied to $a$. More precisely, the natural isomorphism is given componentwise by the identity isomorphism at each object $b \in B$, i.e., $(F^{\text{flip}} \circ \text{eval}_a)(b) \cong F(a)(b)$ via the identity morphism.
CategoryTheory.flip_comp_evaluation theorem
(F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a = F.obj a
Full source 
theorem flip_comp_evaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a = F.obj a :=
  rfl
Flipped Functor Composition with Evaluation Equals Original Functor
Informal description
For any functor $F \colon A \to (B \to C)$ and any object $a \in A$, the composition of the flipped functor $F^{\text{flip}} \colon B \to (A \to C)$ with the evaluation functor at $a$ is equal to the original functor $F$ applied to $a$. More precisely, we have $(F^{\text{flip}} \circ \text{eval}_a) = F(a)$, where $\text{eval}_a$ denotes the evaluation functor at $a$.
CategoryTheory.compEvaluation definition
(F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b ≅ F.flip.obj b
Full source 
/-- `F` composed with evaluation is the same as evaluating `F.flip`. -/
@[simps!]
def compEvaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj bF ⋙ (evaluation _ _).obj b ≅ F.flip.obj b :=
  NatIso.ofComponents fun a => Iso.refl _
Composition with evaluation is isomorphic to flipped evaluation
Informal description
For any functor $F \colon A \to (B \to C)$ and any object $b \in B$, the composition of $F$ with the evaluation functor at $b$ is naturally isomorphic to the application of the flipped functor $F^{\text{flip}}$ at $b$. More precisely, the natural isomorphism is given componentwise by the identity isomorphism at each object $a \in A$, i.e., $(F \circ \text{eval}_b)(a) \cong F^{\text{flip}}(b)(a)$ via the identity morphism.
CategoryTheory.comp_evaluation theorem
(F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b = F.flip.obj b
Full source 
theorem comp_evaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b = F.flip.obj b :=
  rfl
Composition with Evaluation Equals Flipped Evaluation
Informal description
For any functor $F \colon A \to (B \to C)$ and any object $b \in B$, the composition of $F$ with the evaluation functor at $b$ is equal to the application of the flipped functor $F^{\text{flip}}$ at $b$. More precisely, for each object $a \in A$, we have $(F \circ \text{eval}_b)(a) = F^{\text{flip}}(b)(a)$.
CategoryTheory.whiskeringLeftCompEvaluation definition
(F : A ⥤ B) (a : A) : (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a ≅ (evaluation B C).obj (F.obj a)
Full source 
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`. -/
@[simps!]
def whiskeringLeftCompEvaluation (F : A ⥤ B) (a : A) :
    (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a(whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a ≅ (evaluation B C).obj (F.obj a) :=
  Iso.refl _
Natural isomorphism between left whiskering and evaluation functors
Informal description
For any functor \( F \colon A \to B \) and any object \( a \in A \), the composition of the left whiskering functor applied to \( F \) with the evaluation functor at \( a \) is naturally isomorphic to the evaluation functor at \( F(a) \). More precisely, the natural isomorphism is given componentwise by the identity isomorphism, meaning that for any functor \( G \colon B \to C \), we have: \[ (F \circ G)(a) \cong G(F(a)) \] via the identity morphism.
CategoryTheory.whiskeringLeft_comp_evaluation theorem
(F : A ⥤ B) (a : A) : (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a = (evaluation B C).obj (F.obj a)
Full source 
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`. -/
@[simp]
theorem whiskeringLeft_comp_evaluation (F : A ⥤ B) (a : A) :
    (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a = (evaluation B C).obj (F.obj a) :=
  rfl
Equality of Left Whiskering and Evaluation Functors: $(F \circ G)(a) = G(F(a))$
Informal description
For any functor $F \colon A \to B$ and any object $a \in A$, the composition of the left whiskering functor applied to $F$ with the evaluation functor at $a$ is equal to the evaluation functor at $F(a)$. More precisely, for any functor $G \colon B \to C$, we have: \[ (F \circ G)(a) = G(F(a)) \]
CategoryTheory.whiskeringRightCompEvaluation definition
(F : B ⥤ C) (a : A) : (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a ≅ (evaluation _ _).obj a ⋙ F
Full source 
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
applying `F`. -/
@[simps!]
def whiskeringRightCompEvaluation (F : B ⥤ C) (a : A) :
    (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a(whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a ≅ (evaluation _ _).obj a ⋙ F :=
  Iso.refl _
Natural isomorphism between whiskering and evaluation functors
Informal description
For any functor \( F \colon B \to C \) and any object \( a \) in category \( A \), the composition of the right whiskering functor applied to \( F \) with the evaluation functor at \( a \) is naturally isomorphic to the composition of the evaluation functor at \( a \) with \( F \). In other words, the diagram \[ \begin{tikzcd} (A \to B) \arrow[r, "F \circ -"] \arrow[d, "\text{eval}_a"] & (A \to C) \arrow[d, "\text{eval}_a"] \\ B \arrow[r, "F"] & C \end{tikzcd} \] commutes up to natural isomorphism.
CategoryTheory.whiskeringRight_comp_evaluation theorem
(F : B ⥤ C) (a : A) : (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a = (evaluation _ _).obj a ⋙ F
Full source 
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
applying `F`. -/
@[simp]
theorem whiskeringRight_comp_evaluation (F : B ⥤ C) (a : A) :
    (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a = (evaluation _ _).obj a ⋙ F :=
  rfl
Right Whiskering and Evaluation Functors Commute
Informal description
For any functor $F \colon B \to C$ and any object $a \in A$, the composition of the right whiskering functor applied to $F$ with the evaluation functor at $a$ is equal to the composition of the evaluation functor at $a$ with $F$. In other words, the following diagram commutes: \[ \begin{tikzcd} (A \to B) \arrow[r, "F \circ -"] \arrow[d, "\text{eval}_a"] & (A \to C) \arrow[d, "\text{eval}_a"] \\ B \arrow[r, "F"] & C \end{tikzcd} \]
CategoryTheory.prodFunctorToFunctorProd definition
: (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C
Full source 
/-- The forward direction for `functorProdFunctorEquiv` -/
@[simps]
def prodFunctorToFunctorProd : (A ⥤ B) × (A ⥤ C)(A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C where
  obj F := F.1.prod' F.2
  map {F G} f := NatTrans.prod' f.1 f.2
Functor from product of functors to functor into product category
Informal description
The functor that takes a pair of functors $(F \colon A \to B, G \colon A \to C)$ and constructs a single functor $F \times G \colon A \to B \times C$ which maps an object $X \in A$ to the pair $(F(X), G(X))$ and a morphism $f$ in $A$ to the pair of morphisms $(F(f), G(f))$ in $B \times C$.
CategoryTheory.functorProdToProdFunctor definition
: (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C)
Full source 
/-- The backward direction for `functorProdFunctorEquiv` -/
@[simps]
def functorProdToProdFunctor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C) where
  obj F := ⟨F ⋙ CategoryTheory.Prod.fst B C, F ⋙ CategoryTheory.Prod.snd B C⟩
  map α := ⟨whiskerRight α _, whiskerRight α _⟩
Decomposition of a functor into product categories
Informal description
The functor `functorProdToProdFunctor` maps a functor $F \colon A \to B \times C$ to the pair of functors $(F \circ \text{fst}, F \circ \text{snd})$, where $\text{fst} \colon B \times C \to B$ and $\text{snd} \colon B \times C \to C$ are the projection functors. For a natural transformation $\alpha \colon F \to G$, it maps $\alpha$ to the pair of natural transformations $(\alpha \circ \text{fst}, \alpha \circ \text{snd})$.
CategoryTheory.functorProdFunctorEquivUnitIso definition
: 𝟭 _ ≅ prodFunctorToFunctorProd A B C ⋙ functorProdToProdFunctor A B C
Full source 
/-- The unit isomorphism for `functorProdFunctorEquiv` -/
@[simps!]
def functorProdFunctorEquivUnitIso :
    𝟭𝟭 _ ≅ prodFunctorToFunctorProd A B C ⋙ functorProdToProdFunctor A B C :=
  NatIso.ofComponents fun F =>
    Functor.prod'CompFst F.fst F.snd |>.prod (Functor.prod'CompSnd F.fst F.snd) |>.trans
      (prod.etaIso F) |>.symm
Unit isomorphism for the equivalence between product of functors and functors into product categories
Informal description
The natural isomorphism between the identity functor on the product category $(A \to B) \times (A \to C)$ and the composition of the functors $\text{prodFunctorToFunctorProd}$ and $\text{functorProdToProdFunctor}$. Specifically, for any pair of functors $(F, G) \colon (A \to B) \times (A \to C)$, this isomorphism is constructed by taking the product of the isomorphisms $F \times G \circ \text{fst} \cong F$ and $F \times G \circ \text{snd} \cong G$, and then composing with the inverse of the isomorphism $(F.1, F.2) \cong F$.
CategoryTheory.functorProdFunctorEquivCounitIso definition
: functorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B C ≅ 𝟭 _
Full source 
/-- The counit isomorphism for `functorProdFunctorEquiv` -/
@[simps!]
def functorProdFunctorEquivCounitIso :
    functorProdToProdFunctorfunctorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B CfunctorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B C ≅ 𝟭 _ :=
  NatIso.ofComponents fun F => NatIso.ofComponents fun X => prod.etaIso (F.obj X)
Counit isomorphism for functor-product equivalence
Informal description
The counit isomorphism for the equivalence between functors into a product category and products of functors. Specifically, it is a natural isomorphism between the composition of the functors `functorProdToProdFunctor` and `prodFunctorToFunctorProd` (which decompose and recompose functors into product categories) and the identity functor on `(A ⥤ B) × (A ⥤ C)`. At each object `F` in `(A ⥤ B) × (A ⥤ C)`, the isomorphism is given componentwise by the isomorphism `prod.etaIso (F.obj X)` for each object `X` in `A`, which identifies a pair of objects with their product.
CategoryTheory.functorProdFunctorEquiv definition
: (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C
Full source 
/-- The equivalence of categories between `(A ⥤ B) × (A ⥤ C)` and `A ⥤ (B × C)` -/
@[simps]
def functorProdFunctorEquiv : (A ⥤ B) × (A ⥤ C)(A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C :=
  { functor := prodFunctorToFunctorProd A B C,
    inverse := functorProdToProdFunctor A B C,
    unitIso := functorProdFunctorEquivUnitIso A B C,
    counitIso := functorProdFunctorEquivCounitIso A B C, }
Equivalence between product of functors and functors into product categories
Informal description
The equivalence of categories between the product of functor categories $(A \to B) \times (A \to C)$ and the functor category $A \to (B \times C)$. This equivalence consists of: - A functor $\text{prodFunctorToFunctorProd}$ that maps a pair of functors $(F, G)$ to the product functor $F \times G$ sending each object $X \in A$ to $(F(X), G(X))$ and each morphism $f$ in $A$ to $(F(f), G(f))$. - An inverse functor $\text{functorProdToProdFunctor}$ that decomposes a functor $H \colon A \to B \times C$ into the pair of functors $(H \circ \text{fst}, H \circ \text{snd})$. - Natural isomorphisms $\text{functorProdFunctorEquivUnitIso}$ and $\text{functorProdFunctorEquivCounitIso}$ witnessing that these functors form an equivalence.
CategoryTheory.prodOpEquiv definition
: (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ
Full source 
/-- The equivalence between the opposite of a product and the product of the opposites. -/
@[simps!]
def prodOpEquiv : (C × D)ᵒᵖ(C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ where
  functor :=
    { obj := fun X ↦ ⟨op X.unop.1, op X.unop.2⟩,
      map := fun f ↦ ⟨f.unop.1.op, f.unop.2.op⟩ }
  inverse :=
    { obj := fun ⟨X,Y⟩ ↦ op ⟨X.unop, Y.unop⟩,
      map := fun ⟨f,g⟩ ↦ op ⟨f.unop, g.unop⟩ }
  unitIso := Iso.refl _
  counitIso := Iso.refl _
Equivalence between opposite of product and product of opposites
Informal description
The equivalence between the opposite category of the product category $C \times D$ and the product of the opposite categories $C^{\mathrm{op}} \times D^{\mathrm{op}}$. Explicitly, this equivalence consists of: - A functor $(C \times D)^{\mathrm{op}} \to C^{\mathrm{op}} \times D^{\mathrm{op}}$ that maps an object $(X,Y)^{\mathrm{op}}$ to $(X^{\mathrm{op}}, Y^{\mathrm{op}})$ and a morphism $(f,g)^{\mathrm{op}}$ to $(f^{\mathrm{op}}, g^{\mathrm{op}})$. - An inverse functor $C^{\mathrm{op}} \times D^{\mathrm{op}} \to (C \times D)^{\mathrm{op}}$ that maps $(X^{\mathrm{op}}, Y^{\mathrm{op}})$ to $(X,Y)^{\mathrm{op}}$ and $(f^{\mathrm{op}}, g^{\mathrm{op}})$ to $(f,g)^{\mathrm{op}}$. - Natural isomorphisms showing these functors form an equivalence of categories.