# Documentation

Mathlib.CategoryTheory.Products.Basic

# 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_Hom (C : Type u₁) [] (D : Type u₂) [] (X : C × D) (Y : C × D) :
(X Y) = ((X.fst Y.fst) × (X.snd Y.snd))
@[simp]
theorem CategoryTheory.prod_comp_snd (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y Z : C × D} (f : X Y) (g : Y Z), ().snd = CategoryTheory.CategoryStruct.comp f.snd g.snd
@[simp]
theorem CategoryTheory.prod_id_fst (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
@[simp]
theorem CategoryTheory.prod_id_snd (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
@[simp]
theorem CategoryTheory.prod_comp_fst (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y Z : C × D} (f : X Y) (g : Y Z), ().fst = CategoryTheory.CategoryStruct.comp f.fst g.fst
instance CategoryTheory.prod (C : Type u₁) [] (D : Type u₂) [] :

prod C D gives the cartesian product of two categories.

@[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_inv {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
().inv =
@[simp]
theorem CategoryTheory.prod.etaIso_hom {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
().hom = (CategoryTheory.CategoryStruct.id (X.fst, X.snd).fst, CategoryTheory.CategoryStruct.id (X.fst, X.snd).snd)
def CategoryTheory.prod.etaIso {C : Type u₁} [] {D : Type u₂} [] (X : C × D) :
(X.fst, X.snd) X

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

Instances For
@[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) :
().inv = (f.inv, g.inv)
@[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) :
().hom = (f.hom, g.hom)
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.

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.

@[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).

Instances For
@[simp]
theorem CategoryTheory.Prod.sectr_map {C : Type u₁} [] (Z : C) (D : Type u₂) [] :
∀ {X Y : D} (f : X Y), ().map f =
@[simp]
theorem CategoryTheory.Prod.sectr_obj {C : Type u₁} [] (Z : C) (D : Type u₂) [] (X : D) :
().obj X = (Z, X)
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) .

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

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

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

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

Instances For
@[simp]
theorem CategoryTheory.Prod.swap_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), ().map f = (f.snd, f.fst)
@[simp]
theorem CategoryTheory.Prod.swap_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().obj X = (X.snd, X.fst)
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.

Instances For
@[simp]
theorem CategoryTheory.Prod.symmetry_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().hom.app X =
@[simp]
theorem CategoryTheory.Prod.symmetry_inv_app (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().inv.app X =
def CategoryTheory.Prod.symmetry (C : Type u₁) [] (D : Type u₂) [] :

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

Instances For
@[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_inverse_obj (C : Type u₁) [] (D : Type u₂) [] (X : D × C) :
().inverse.obj X = (X.snd, X.fst)
@[simp]
theorem CategoryTheory.Prod.braiding_inverse_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : D × C} (f : X Y), ().inverse.map f = (f.snd, f.fst)
@[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_functor_obj (C : Type u₁) [] (D : Type u₂) [] (X : C × D) :
().functor.obj X = (X.snd, X.fst)
@[simp]
theorem CategoryTheory.Prod.braiding_functor_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : C × D} (f : X Y), ().functor.map f = (f.snd, f.fst)
@[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_counitIso_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : D × C) :
().counitIso.hom.app X =
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.

Instances For
instance CategoryTheory.Prod.swapIsEquivalence (C : Type u₁) [] (D : Type u₂) [] :
@[simp]
theorem CategoryTheory.evaluation_obj_map (C : Type u₁) [] (D : Type u₂) [] (X : C) :
∀ {X Y : } (α : X 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.

Instances For
@[simp]
theorem CategoryTheory.evaluationUncurried_obj (C : Type u₁) [] (D : Type u₂) [] (p : ) :
().obj p = p.snd.obj p.fst
@[simp]
theorem CategoryTheory.evaluationUncurried_map (C : Type u₁) [] (D : Type u₂) [] {x : } {y : } (f : x y) :
().map f = CategoryTheory.CategoryStruct.comp (x.snd.map f.fst) (f.snd.app y.fst)
def CategoryTheory.evaluationUncurried (C : Type u₁) [] (D : Type u₂) [] :

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

Instances For
@[simp]
theorem CategoryTheory.Functor.constCompEvaluationObj_inv_app {C : Type u₁} [] (D : Type u₂) [] (X : C) (X : D) :
@[simp]
theorem CategoryTheory.Functor.constCompEvaluationObj_hom_app {C : Type u₁} [] (D : Type u₂) [] (X : C) (X : D) :
def CategoryTheory.Functor.constCompEvaluationObj {C : Type u₁} [] (D : Type u₂) [] (X : C) :

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

Instances For
@[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), ().map f = (F.map f.fst, G.map f.snd)
@[simp]
theorem CategoryTheory.Functor.prod_obj {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (X : A × C) :
().obj X = (F.obj X.fst, G.obj X.snd)
def CategoryTheory.Functor.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) :

The cartesian product of two functors.

Instances For
@[simp]
theorem CategoryTheory.Functor.prod'_obj {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (a : A) :
().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), ().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

Instances For
@[simp]
theorem CategoryTheory.Functor.prod'CompFst_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
().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) :
().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 : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Functor.prod'CompSnd_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] (F : ) (G : ) (X : A) :
().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) :
().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 : ) :

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

Instances For

The diagonal functor.

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.fst, β.app X.snd)
def CategoryTheory.NatTrans.prod {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) :

The cartesian product of two natural transformations.

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.obj a

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

Instances For
@[simp]
theorem CategoryTheory.prodFunctorToFunctorProd_obj (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (F : ) :
().obj F = CategoryTheory.Functor.prod' F.fst F.snd
@[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.fst.app X_1, f.snd.app X_1)
def CategoryTheory.prodFunctorToFunctorProd (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The forward direction for functorProdFunctorEquiv

Instances For
@[simp]
theorem CategoryTheory.functorProdToProdFunctor_map (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
∀ {X Y : CategoryTheory.Functor A (B × C)} (α : X Y), ().map α = (CategoryTheory.NatTrans.mk fun X_1 => (α.app X_1).fst, CategoryTheory.NatTrans.mk fun X_1 => (α.app X_1).snd)
@[simp]
theorem CategoryTheory.functorProdToProdFunctor_obj (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (F : CategoryTheory.Functor A (B × C)) :
().obj F =
def CategoryTheory.functorProdToProdFunctor (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The backward direction for functorProdFunctorEquiv

Instances For
@[simp]
theorem CategoryTheory.functorProdFunctorEquivUnitIso_hom_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : ) :
().hom.app X = ((CategoryTheory.Functor.prod'CompFst X.fst X.snd).inv, (CategoryTheory.Functor.prod'CompSnd X.fst X.snd).inv)
@[simp]
theorem CategoryTheory.functorProdFunctorEquivUnitIso_inv_app (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] (X : ) :
().inv.app X = ((CategoryTheory.Functor.prod'CompFst X.fst X.snd).hom, (CategoryTheory.Functor.prod'CompSnd X.fst X.snd).hom)
def CategoryTheory.functorProdFunctorEquivUnitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The unit isomorphism for functorProdFunctorEquiv

Instances For
@[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).fst, CategoryTheory.CategoryStruct.id (X.obj X).snd)
@[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).fst, CategoryTheory.CategoryStruct.id (X.obj X).snd)
def CategoryTheory.functorProdFunctorEquivCounitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :

The counit isomorphism for functorProdFunctorEquiv

Instances For
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_functor (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
().functor =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_counitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
().counitIso =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_inverse (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
().inverse =
@[simp]
theorem CategoryTheory.functorProdFunctorEquiv_unitIso (A : Type u₁) [] (B : Type u₂) [] (C : Type u₃) [] :
().unitIso =
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)

Instances For