mathlib documentation

category_theory.products.basic

@[instance]

prod C D gives the cartesian product of two categories.

See https://stacks.math.columbia.edu/tag/001K.

Equations
@[simp]
theorem category_theory.prod_id (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (Y : D) :
𝟙 (X, Y) = (𝟙 X, 𝟙 Y)

@[simp]
theorem category_theory.prod_comp (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] {P Q R : C} {S T U : D} (f : (P, S) (Q, T)) (g : (Q, T) (R, U)) :
f g = (f.fst g.fst, f.snd g.snd)

@[simp]
theorem category_theory.prod_id_fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :
(𝟙 X).fst = 𝟙 X.fst

@[simp]
theorem category_theory.prod_id_snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :
(𝟙 X).snd = 𝟙 X.snd

@[simp]
theorem category_theory.prod_comp_fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] {X Y Z : C × D} (f : X Y) (g : Y Z) :
(f g).fst = f.fst g.fst

@[simp]
theorem category_theory.prod_comp_snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] {X Y Z : C × D} (f : X Y) (g : Y Z) :
(f g).snd = f.snd g.snd

@[instance]

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

Equations
@[simp]
theorem category_theory.prod.sectl_map (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] (Z : D) (X Y : C) (f : X Y) :

def category_theory.prod.sectl (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] :
D → C C × D

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

Equations
@[simp]
theorem category_theory.prod.sectl_obj (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] (Z : D) (X : C) :

@[simp]
theorem category_theory.prod.sectr_map {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] (X Y : D) (f : X Y) :

def category_theory.prod.sectr {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] :
D C × D

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

Equations
@[simp]
theorem category_theory.prod.sectr_obj {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] (X : D) :

def category_theory.prod.fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
C × D C

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

Equations
@[simp]
theorem category_theory.prod.fst_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C × D) (f : X Y) :

@[simp]
theorem category_theory.prod.fst_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

@[simp]
theorem category_theory.prod.snd_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C × D) (f : X Y) :

@[simp]
theorem category_theory.prod.snd_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

def category_theory.prod.snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
C × D D

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

Equations
@[simp]
theorem category_theory.prod.swap_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

@[simp]
theorem category_theory.prod.swap_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : C × D) (f : _x _x_1) :

def category_theory.prod.swap (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
C × D D × C

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

Equations
@[simp]

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

Equations
@[simp]

@[simp]
theorem category_theory.prod.braiding_functor_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : C × D) (f : _x _x_1) :

@[simp]
theorem category_theory.prod.braiding_inverse_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : D × C) (f : _x _x_1) :

@[simp]

@[simp]

@[simp]
theorem category_theory.evaluation_map_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C) (f : X Y) (F : C D) :

def category_theory.evaluation (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
C (C D) D

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

Equations
@[simp]
theorem category_theory.evaluation_obj_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (F : C D) :

@[simp]
theorem category_theory.evaluation_obj_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (F G : C D) (α : F G) :

@[simp]
theorem category_theory.evaluation_uncurried_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (x y : C × (C D)) (f : x y) :

def category_theory.evaluation_uncurried (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
C × (C D) D

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

Equations
@[simp]
theorem category_theory.functor.prod_map {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] (F : A B) (G : C D) (_x _x_1 : A × C) (f : _x _x_1) :
(F.prod G).map f = (F.map f.fst, G.map f.snd)

@[simp]
theorem category_theory.functor.prod_obj {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] (F : A B) (G : C D) (X : A × C) :
(F.prod G).obj X = (F.obj X.fst, G.obj X.snd)

def category_theory.functor.prod {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] :
A BC DA × C B × D

The cartesian product of two functors.

Equations
def category_theory.nat_trans.prod {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F G : A B} {H I : C D} :
(F G)(H I)(F.prod H G.prod I)

The cartesian product of two natural transformations.

Equations
@[simp]
theorem category_theory.nat_trans.prod_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F G : A B} {H I : C D} (α : F G) (β : H I) (X : A × C) :