# 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 β.

@[simp]
theorem CategoryTheory.prod_comp_fst (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y Z : C × D} (f : X Y) (g : Y Z),
@[simp]
theorem CategoryTheory.prod_comp_snd (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y Z : C × D} (f : X Y) (g : Y Z),
@[simp]
theorem CategoryTheory.prod_id_snd (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
@[simp]
theorem CategoryTheory.prod_Hom (C : Type u₁) [] (D : Type u₂) [] (X : C × D) (Y : C × D) :
(X Y) = ((X.1 Y.1) × (X.2 Y.2))
@[simp]
theorem CategoryTheory.prod_id_fst (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
instance CategoryTheory.prod (C : Type u₁) [] (D : Type u₂) [] :

prod C D gives the cartesian product of two categories.

Equations
@[simp]
theorem CategoryTheory.prod_id (C : Type u₁) [] (D : Type u₂) [] (X : C) (Y : D) :

Two rfl lemmas that cannot be generated by @[simps].

@[simp]
theorem CategoryTheory.prod_comp (C : Type u₁) [] (D : Type u₂) [] {P : C} {Q : C} {R : C} {S : D} {T : D} {U : D} (f : (P, S) (Q, T)) (g : (Q, T) (R, U)) :
theorem CategoryTheory.isIso_prod_iff (C : Type u₁) [] (D : Type u₂) [] {P : C} {Q : C} {S : D} {T : D} {f : (P, S) (Q, T)} :
@[simp]
theorem CategoryTheory.prod.etaIso_hom {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
@[simp]
theorem CategoryTheory.prod.etaIso_inv {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
def CategoryTheory.prod.etaIso {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
(X.1, X.2) X

The isomorphism between (X.1, X.2) and X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Iso.prod_hom {C : Type u₁} [] {D : Type u₂} [] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
(f.prod g).hom = (f.hom, g.hom)
@[simp]
theorem CategoryTheory.Iso.prod_inv {C : Type u₁} [] {D : Type u₂} [] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
(f.prod g).inv = (f.inv, g.inv)
def CategoryTheory.Iso.prod {C : Type u₁} [] {D : Type u₂} [] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
(P, S) (Q, T)

Construct an isomorphism in C × D out of two isomorphisms in C and D.

Equations
• f.prod g = { hom := (f.hom, g.hom), inv := (f.inv, g.inv), hom_inv_id := , inv_hom_id := }
Instances For
instance CategoryTheory.uniformProd (C : Type u₁) [] (D : Type u₁) [] :

Category.uniformProd C D is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.

Equations
@[simp]
theorem CategoryTheory.Prod.sectl_map (C : Type u₁) [] {D : Type u₂} [] (Z : D) :
∀ {X Y : C} (f : X Y), .map f =
@[simp]
theorem CategoryTheory.Prod.sectl_obj (C : Type u₁) [] {D : Type u₂} [] (Z : D) (X : C) :
.obj X = (X, Z)
def CategoryTheory.Prod.sectl (C : Type u₁) [] {D : Type u₂} [] (Z : D) :

sectl C Z is the functor C ⥤ C × D given by X ↦ (X, Z).

Equations
• = { obj := fun (X : C) => (X, Z), map := fun {X Y : C} (f : X Y) => , map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Prod.sectr_obj {C : Type u₁} [] (Z : C) (D : Type u₂) [] (X : D) :
.obj X = (Z, X)
@[simp]
theorem CategoryTheory.Prod.sectr_map {C : Type u₁} [] (Z : C) (D : Type u₂) [] :
∀ {X Y : D} (f : X Y), .map f =
def CategoryTheory.Prod.sectr {C : Type u₁} [] (Z : C) (D : Type u₂) [] :

sectr Z D is the functor D ⥤ C × D given by Y ↦ (Z, Y) .

Equations
• = { obj := fun (X : D) => (Z, X), map := fun {X Y : D} (f : X Y) => , map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Prod.fst_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), ().map f = f.1
@[simp]
theorem CategoryTheory.Prod.fst_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().obj X = X.1
def CategoryTheory.Prod.fst (C : Type u₁) [] (D : Type u₂) [] :

fst is the functor (X, Y) ↦ X.

Equations
• = { obj := fun (X : C × D) => X.1, map := fun {X Y : C × D} (f : X Y) => f.1, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Prod.snd_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().obj X = X.2
@[simp]
theorem CategoryTheory.Prod.snd_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), ().map f = f.2
def CategoryTheory.Prod.snd (C : Type u₁) [] (D : Type u₂) [] :

snd is the functor (X, Y) ↦ Y.

Equations
• = { obj := fun (X : C × D) => X.2, map := fun {X Y : C × D} (f : X Y) => f.2, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Prod.swap_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().obj X = (X.2, X.1)
@[simp]
theorem CategoryTheory.Prod.swap_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), ().map f = (f.2, f.1)
def CategoryTheory.Prod.swap (C : Type u₁) [] (D : Type u₂) [] :

The functor swapping the factors of a cartesian product of categories, C × D ⥤ D × C.

Equations
• = { obj := fun (X : C × D) => (X.2, X.1), map := fun {X Y : C × D} (f : X Y) => (f.2, f.1), map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Prod.symmetry_inv_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
.inv.app X =
@[simp]
theorem CategoryTheory.Prod.symmetry_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
.hom.app X =
def CategoryTheory.Prod.symmetry (C : Type u₁) [] (D : Type u₂) [] :
().comp ()

Swapping the factors of a cartesian product of categories twice is naturally isomorphic to the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Prod.braiding_counitIso_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : D × C) :
.counitIso.hom.app X =
@[simp]
theorem CategoryTheory.Prod.braiding_inverse_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : D × C} (f : X Y), .inverse.map f = (f.2, f.1)
@[simp]
theorem CategoryTheory.Prod.braiding_unitIso_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
.unitIso.hom.app X =
@[simp]
theorem CategoryTheory.Prod.braiding_inverse_obj (C : Type u₁) [] (D : Type u₂) [] (X : D × C) :
.inverse.obj X = (X.2, X.1)
@[simp]
theorem CategoryTheory.Prod.braiding_counitIso_inv_app (C : Type u₁) [] (D : Type u₂) [] (X : D × C) :
.counitIso.inv.app X =
@[simp]
theorem CategoryTheory.Prod.braiding_functor_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), .functor.map f = (f.2, f.1)
@[simp]
theorem CategoryTheory.Prod.braiding_unitIso_inv_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
.unitIso.inv.app X =
@[simp]
theorem CategoryTheory.Prod.braiding_functor_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
.functor.obj X = (X.2, X.1)
def CategoryTheory.Prod.braiding (C : Type u₁) [] (D : Type u₂) [] :
C × D D × C

The equivalence, given by swapping factors, between C × D and D × C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Prod.swapIsEquivalence (C : Type u₁) [] (D : Type u₂) [] :
().IsEquivalence
Equations
• =
@[simp]
theorem CategoryTheory.evaluation_obj_map (C : Type u₁) [] (D : Type u₂) [] (X : C) :
∀ {X_1 Y : } (α : X_1 Y), (.obj X).map α = α.app X
@[simp]
theorem CategoryTheory.evaluation_map_app (C : Type u₁) [] (D : Type u₂) [] {X : C} {Y : C} (f : X Y) (F : ) :
(.map f).app F = F.map f
@[simp]
theorem CategoryTheory.evaluation_obj_obj (C : Type u₁) [] (D : Type u₂) [] (X : C) (F : ) :
(.obj X).obj F = F.obj X
def CategoryTheory.evaluation (C : Type u₁) [] (D : Type u₂) [] :

The "evaluation at X" functor, such that (evaluation.obj X).obj F = F.obj X, which is functorial in both X and F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.evaluationUncurried_map (C : Type u₁) [] (D : Type u₂) [] {x : } {y : } (f : x y) :
.map f = CategoryTheory.CategoryStruct.comp (x.2.map f.1) (f.2.app y.1)
@[simp]
theorem CategoryTheory.evaluationUncurried_obj (C : Type u₁) [] (D : Type u₂) [] (p : ) :
.obj p = p.2.obj p.1
def CategoryTheory.evaluationUncurried (C : Type u₁) [] (D : Type u₂) [] :

The "evaluation of F at X" functor, as a functor C × (C ⥤ D) ⥤ D.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.constCompEvaluationObj_hom_app {C : Type u₁} [] (D : Type u₂) [] (X : C) (X : D) :
@[simp]
theorem CategoryTheory.Functor.constCompEvaluationObj_inv_app {C : Type u₁} [] (D : Type u₂) [] (X : C) (X : D) :
def CategoryTheory.Functor.constCompEvaluationObj {C : Type u₁} [] (D : Type u₂) [] (X : C) :
.comp (.obj X)

The constant functor followed by the evaluation functor is just the identity.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.prod_obj {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (X : A × C) :
(F.prod G).obj X = (F.obj X.1, G.obj X.2)
@[simp]
theorem CategoryTheory.Functor.prod_map {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) :
∀ {X Y : A × C} (f : X Y), (F.prod G).map f = (F.map f.1, G.map f.2)
def CategoryTheory.Functor.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) :

The cartesian product of two functors.

Equations
• F.prod G = { obj := fun (X : A × C) => (F.obj X.1, G.obj X.2), map := fun {X Y : A × C} (f : X Y) => (F.map f.1, G.map f.2), map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.prod'_obj {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (a : A) :
(F.prod' G).obj a = (F.obj a, G.obj a)
@[simp]
theorem CategoryTheory.Functor.prod'_map {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) :
∀ {X Y : A} (f : X Y), (F.prod' G).map f = (F.map f, G.map f)
def CategoryTheory.Functor.prod' {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) :

Similar to prod, but both functors start from the same category A

Equations
• F.prod' G = { obj := fun (a : A) => (F.obj a, G.obj a), map := fun {X Y : A} (f : X Y) => (F.map f, G.map f), map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.prod'CompFst_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
(F.prod'CompFst G).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Functor.prod'CompFst_hom_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
(F.prod'CompFst G).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Functor.prod'CompFst {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) :
(F.prod' G).comp () F

The product F.prod' G followed by projection on the first component is isomorphic to F

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.prod'CompSnd_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
(F.prod'CompSnd G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
@[simp]
theorem CategoryTheory.Functor.prod'CompSnd_hom_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
(F.prod'CompSnd G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
def CategoryTheory.Functor.prod'CompSnd {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) :
(F.prod' G).comp () G

The product F.prod' G followed by projection on the second component is isomorphic to G

Equations
Instances For

The diagonal functor.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.diag_obj (C : Type u₃) [] (X : C) :
.obj X = (X, X)
@[simp]
theorem CategoryTheory.Functor.diag_map (C : Type u₃) [] {X : C} {Y : C} (f : X Y) :
.map f = (f, f)
@[simp]
theorem CategoryTheory.NatTrans.prod_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) (X : A × C) :
.app X = (α.app X.1, β.app X.2)
def CategoryTheory.NatTrans.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) :
F.prod H G.prod I

The cartesian product of two natural transformations.

Equations
• = { app := fun (X : A × C) => (α.app X.1, β.app X.2), naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatIso.prod_hom {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {G : } {G' : } (e₁ : F F') (e₂ : G G') :
().hom = CategoryTheory.NatTrans.prod e₁.hom e₂.hom
@[simp]
theorem CategoryTheory.NatIso.prod_inv {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {G : } {G' : } (e₁ : F F') (e₂ : G G') :
().inv = CategoryTheory.NatTrans.prod e₁.inv e₂.inv
def CategoryTheory.NatIso.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {G : } {G' : } (e₁ : F F') (e₂ : G G') :
F.prod G F'.prod G'

The cartesian product of two natural isomorphisms.

Equations
Instances For
@[simp]
theorem CategoryTheory.Equivalence.prod_functor {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (E₁ : A B) (E₂ : C D) :
(E₁.prod E₂).functor = E₁.functor.prod E₂.functor
@[simp]
theorem CategoryTheory.Equivalence.prod_inverse {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (E₁ : A B) (E₂ : C D) :
(E₁.prod E₂).inverse = E₁.inverse.prod E₂.inverse
@[simp]
theorem CategoryTheory.Equivalence.prod_counitIso {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (E₁ : A B) (E₂ : C D) :
(E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso
@[simp]
theorem CategoryTheory.Equivalence.prod_unitIso {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (E₁ : A B) (E₂ : C D) :
(E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
def CategoryTheory.Equivalence.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (E₁ : A B) (E₂ : C D) :
A × C B × D

The cartesian product of two equivalences of categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.flipCompEvaluation_hom_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (a : A) (X : B) :
.hom.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
@[simp]
theorem CategoryTheory.flipCompEvaluation_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (a : A) (X : B) :
.inv.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
def CategoryTheory.flipCompEvaluation {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (a : A) :
F.flip.comp (.obj a) F.obj a

F.flip composed with evaluation is the same as evaluating F.

Equations
Instances For
@[simp]
theorem CategoryTheory.prodFunctorToFunctorProd_map_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
∀ {X Y : } (f : X Y) (X_1 : A), (.map f).app X_1 = (f.1.app X_1, f.2.app X_1)
@[simp]
theorem CategoryTheory.prodFunctorToFunctorProd_obj (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (F : ) :
.obj F = F.1.prod' F.2
def CategoryTheory.prodFunctorToFunctorProd (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The forward direction for functorProdFunctorEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.functorProdToProdFunctor_obj (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (F : CategoryTheory.Functor A (B × C)) :
.obj F = (F.comp (), F.comp ())
@[simp]
theorem CategoryTheory.functorProdToProdFunctor_map (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
∀ {X Y : CategoryTheory.Functor A (B × C)} (α : X Y), .map α = ({ app := fun (X_1 : A) => (α.app X_1).1, naturality := }, { app := fun (X_1 : A) => (α.app X_1).2, naturality := })
def CategoryTheory.functorProdToProdFunctor (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The backward direction for functorProdFunctorEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.functorProdFunctorEquivUnitIso_inv_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : ) :
.inv.app X = ((X.1.prod'CompFst X.2).hom, (X.1.prod'CompSnd X.2).hom)
@[simp]
theorem CategoryTheory.functorProdFunctorEquivUnitIso_hom_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : ) :
.hom.app X = ((X.1.prod'CompFst X.2).inv, (X.1.prod'CompSnd X.2).inv)
def CategoryTheory.functorProdFunctorEquivUnitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The unit isomorphism for functorProdFunctorEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : CategoryTheory.Functor A (B × C)) (X : A) :
(.hom.app X✝).app X = (CategoryTheory.CategoryStruct.id (X✝.obj X).1, CategoryTheory.CategoryStruct.id (X✝.obj X).2)
@[simp]
theorem CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : CategoryTheory.Functor A (B × C)) (X : A) :
(.inv.app X✝).app X = (CategoryTheory.CategoryStruct.id (X✝.obj X).1, CategoryTheory.CategoryStruct.id (X✝.obj X).2)
def CategoryTheory.functorProdFunctorEquivCounitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
.comp

The counit isomorphism for functorProdFunctorEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_counitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
.counitIso =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_unitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
.unitIso =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_inverse (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
.inverse =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_functor (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
.functor =
def CategoryTheory.functorProdFunctorEquiv (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The equivalence of categories between (A ⥤ B) × (A ⥤ C) and A ⥤ (B × C)

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.prodOpEquiv_functor_obj (C : Type u₃) [] {D : Type u₄} [] (X : (C × D)ᵒᵖ) :
.functor.obj X = (Opposite.op ().1, Opposite.op ().2)
@[simp]
theorem CategoryTheory.prodOpEquiv_inverse_map (C : Type u₃) [] {D : Type u₄} [] :
∀ {X Y : Cᵒᵖ × Dᵒᵖ} (x : X Y), .inverse.map x = match x with | (f, g) => Opposite.op (f.unop, g.unop)
@[simp]
theorem CategoryTheory.prodOpEquiv_functor_map (C : Type u₃) [] {D : Type u₄} [] :
∀ {X Y : (C × D)ᵒᵖ} (f : X Y), .functor.map f = (f.unop.1.op, f.unop.2.op)
@[simp]
theorem CategoryTheory.prodOpEquiv_unitIso (C : Type u₃) [] {D : Type u₄} [] :
.unitIso =
@[simp]
theorem CategoryTheory.prodOpEquiv_counitIso (C : Type u₃) [] {D : Type u₄} [] :
.counitIso = CategoryTheory.Iso.refl ({ obj := fun (x : Cᵒᵖ × Dᵒᵖ) => match x with | (X, Y) => , map := fun {X Y : Cᵒᵖ × Dᵒᵖ} (x : X Y) => match x with | (f, g) => Opposite.op (f.unop, g.unop), map_id := , map_comp := }.comp { obj := fun (X : (C × D)ᵒᵖ) => (Opposite.op ().1, Opposite.op ().2), map := fun {X Y : (C × D)ᵒᵖ} (f : X Y) => (f.unop.1.op, f.unop.2.op), map_id := , map_comp := })
@[simp]
theorem CategoryTheory.prodOpEquiv_inverse_obj (C : Type u₃) [] {D : Type u₄} [] :
∀ (x : Cᵒᵖ × Dᵒᵖ), .inverse.obj x = match x with | (X, Y) =>
def CategoryTheory.prodOpEquiv (C : Type u₃) [] {D : Type u₄} [] :

The equivalence between the opposite of a product and the product of the opposites.

Equations
• One or more equations did not get rendered due to their size.
Instances For