mathlib3documentation

category_theory.products.basic

Cartesian products of categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 evaluation_uncurried : C × (C ⥤ D) ⥤ D, and products of functors and natural transformations, written F.prod G and α.prod β.

@[simp]
theorem category_theory.prod_id_fst (C : Type u₁) (D : Type u₂) (X : C × D) :
(𝟙 X).fst = 𝟙 X.fst
@[simp]
theorem category_theory.prod_id_snd (C : Type u₁) (D : Type u₂) (X : C × D) :
(𝟙 X).snd = 𝟙 X.snd
@[simp]
theorem category_theory.prod_comp_fst (C : Type u₁) (D : Type u₂) (_x _x_1 _x_2 : C × D) (f : _x _x_1) (g : _x_1 _x_2) :
(f g).fst = f.fst g.fst
@[protected, instance]
def category_theory.prod (C : Type u₁) (D : Type u₂)  :

prod C D gives the cartesian product of two categories.

Equations
@[simp]
theorem category_theory.prod_comp_snd (C : Type u₁) (D : Type u₂) (_x _x_1 _x_2 : C × D) (f : _x _x_1) (g : _x_1 _x_2) :
(f g).snd = f.snd g.snd
@[simp]
theorem category_theory.prod_id (C : Type u₁) (D : Type u₂) (X : C) (Y : D) :
𝟙 (X, Y) = (𝟙 X, 𝟙 Y)

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

@[simp]
theorem category_theory.prod_comp (C : Type u₁) (D : Type u₂) {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)
theorem category_theory.is_iso_prod_iff (C : Type u₁) (D : Type u₂) {P Q : C} {S T : D} {f : (P, S) (Q, T)} :
@[simp]
theorem category_theory.prod.eta_iso_hom {C : Type u₁} {D : Type u₂} (X : C × D) :
= (𝟙 (X.fst, X.snd).fst, 𝟙 (X.fst, X.snd).snd)
@[simp]
theorem category_theory.prod.eta_iso_inv {C : Type u₁} {D : Type u₂} (X : C × D) :
= (𝟙 X.fst, 𝟙 X.snd)
def category_theory.prod.eta_iso {C : Type u₁} {D : Type u₂} (X : C × D) :
(X.fst, X.snd) X

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

Equations
def category_theory.iso.prod {C : Type u₁} {D : Type u₂} {P Q : C} {S 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
@[simp]
theorem category_theory.iso.prod_hom {C : Type u₁} {D : Type u₂} {P Q : C} {S T : D} (f : P Q) (g : S T) :
(f.prod g).hom = (f.hom, g.hom)
@[simp]
theorem category_theory.iso.prod_inv {C : Type u₁} {D : Type u₂} {P Q : C} {S T : D} (f : P Q) (g : S T) :
(f.prod g).inv = (f.inv, g.inv)
@[protected, instance]
def category_theory.uniform_prod (C : Type u₁) (D : Type u₁)  :

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₁) {D : Type u₂} (Z : D) (X Y : C) (f : X Y) :
f = (f, 𝟙 Z)
def category_theory.prod.sectl (C : Type u₁) {D : Type u₂} (Z : 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₁) {D : Type u₂} (Z : D) (X : C) :
X = (X, Z)
@[simp]
theorem category_theory.prod.sectr_map {C : Type u₁} (Z : C) (D : Type u₂) (X Y : D) (f : X Y) :
f = (𝟙 Z, f)
def category_theory.prod.sectr {C : Type u₁} (Z : C) (D : Type u₂)  :
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₁} (Z : C) (D : Type u₂) (X : D) :
X = (Z, X)
def category_theory.prod.fst (C : Type u₁) (D : Type u₂)  :
C × D C

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

Equations
@[simp]
theorem category_theory.prod.fst_map (C : Type u₁) (D : Type u₂) (X Y : C × D) (f : X Y) :
.map f = f.fst
@[simp]
theorem category_theory.prod.fst_obj (C : Type u₁) (D : Type u₂) (X : C × D) :
.obj X = X.fst
@[simp]
theorem category_theory.prod.snd_map (C : Type u₁) (D : Type u₂) (X Y : C × D) (f : X Y) :
.map f = f.snd
@[simp]
theorem category_theory.prod.snd_obj (C : Type u₁) (D : Type u₂) (X : C × D) :
.obj X = X.snd
def category_theory.prod.snd (C : Type u₁) (D : Type u₂)  :
C × D D

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

Equations
@[simp]
theorem category_theory.prod.swap_obj (C : Type u₁) (D : Type u₂) (X : C × D) :
.obj X = (X.snd, X.fst)
@[simp]
theorem category_theory.prod.swap_map (C : Type u₁) (D : Type u₂) (_x _x_1 : C × D) (f : _x _x_1) :
.map f = (f.snd, f.fst)
def category_theory.prod.swap (C : Type u₁) (D : Type u₂)  :
C × D D × C

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

Equations
Instances for category_theory.prod.swap
@[simp]
theorem category_theory.prod.symmetry_hom_app (C : Type u₁) (D : Type u₂) (X : C × D) :
X = 𝟙 X
def category_theory.prod.symmetry (C : Type u₁) (D : Type u₂)  :
𝟭 (C × D)

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

Equations
@[simp]
theorem category_theory.prod.symmetry_inv_app (C : Type u₁) (D : Type u₂) (X : C × D) :
X = 𝟙 X
@[simp]
theorem category_theory.prod.braiding_unit_iso_inv_app (C : Type u₁) (D : Type u₂) (X : C × D) :
= (𝟙 X.fst, 𝟙 X.snd) (𝟙 X.fst, 𝟙 X.snd) (𝟙 X.fst, 𝟙 X.snd) (𝟙 X.fst, 𝟙 X.snd) (𝟙 X.fst, 𝟙 X.snd)
@[simp]
theorem category_theory.prod.braiding_functor_map (C : Type u₁) (D : Type u₂) (_x _x_1 : C × D) (f : _x _x_1) :
= (f.snd, f.fst)
@[simp]
theorem category_theory.prod.braiding_inverse_map (C : Type u₁) (D : Type u₂) (_x _x_1 : D × C) (f : _x _x_1) :
= (f.snd, f.fst)
@[simp]
theorem category_theory.prod.braiding_counit_iso_hom_app (C : Type u₁) (D : Type u₂) (X : D × C) :
def category_theory.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
@[simp]
theorem category_theory.prod.braiding_inverse_obj (C : Type u₁) (D : Type u₂) (X : D × C) :
= (X.snd, X.fst)
@[simp]
theorem category_theory.prod.braiding_functor_obj (C : Type u₁) (D : Type u₂) (X : C × D) :
= (X.snd, X.fst)
@[simp]
theorem category_theory.prod.braiding_unit_iso_hom_app (C : Type u₁) (D : Type u₂) (X : C × D) :
@[simp]
theorem category_theory.prod.braiding_counit_iso_inv_app (C : Type u₁) (D : Type u₂) (X : D × C) :
@[protected, instance]
Equations
@[simp]
theorem category_theory.evaluation_map_app (C : Type u₁) (D : Type u₂) (X Y : C) (f : X Y) (F : C D) :
.map f).app F = F.map f
def category_theory.evaluation (C : Type u₁) (D : Type u₂)  :
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₁) (D : Type u₂) (X : C) (F : C D) :
.obj X).obj F = F.obj X
@[simp]
theorem category_theory.evaluation_obj_map (C : Type u₁) (D : Type u₂) (X : C) (F G : C D) (α : F G) :
.obj X).map α = α.app X
@[simp]
theorem category_theory.evaluation_uncurried_map (C : Type u₁) (D : Type u₂) (x y : C × (C D)) (f : x y) :
= x.snd.map f.fst f.snd.app y.fst
def category_theory.evaluation_uncurried (C : Type u₁) (D : Type u₂)  :
C × (C D) D

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

Equations
@[simp]
theorem category_theory.evaluation_uncurried_obj (C : Type u₁) (D : Type u₂) (p : C × (C D)) :
= p.snd.obj p.fst
@[simp]
theorem category_theory.functor.const_comp_evaluation_obj_inv_app {C : Type u₁} (D : Type u₂) (X : C) (X_1 : D) :
= 𝟙 X_1
def category_theory.functor.const_comp_evaluation_obj {C : Type u₁} (D : Type u₂) (X : C) :

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

Equations
@[simp]
theorem category_theory.functor.const_comp_evaluation_obj_hom_app {C : Type u₁} (D : Type u₂) (X : C) (X_1 : D) :
= 𝟙 X_1
@[simp]
theorem category_theory.functor.prod_map {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} (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₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} (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₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} (F : A B) (G : C D) :
A × C B × D

The cartesian product of two functors.

Equations
@[simp]
theorem category_theory.functor.prod'_map {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (x y : A) (f : x y) :
(F.prod' G).map f = (F.map f, G.map f)
@[simp]
theorem category_theory.functor.prod'_obj {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (a : A) :
(F.prod' G).obj a = (F.obj a, G.obj a)
def category_theory.functor.prod' {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) :
A B × C

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

Equations
@[simp]
theorem category_theory.functor.prod'_comp_fst_inv_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (X : A) :
(F.prod'_comp_fst G).inv.app X = 𝟙 (F.obj X)
def category_theory.functor.prod'_comp_fst {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) :
F.prod' G F

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

Equations
@[simp]
theorem category_theory.functor.prod'_comp_fst_hom_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (X : A) :
(F.prod'_comp_fst G).hom.app X = 𝟙 (F.obj X)
@[simp]
theorem category_theory.functor.prod'_comp_snd_hom_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (X : A) :
(F.prod'_comp_snd G).hom.app X = 𝟙 (G.obj X)
def category_theory.functor.prod'_comp_snd {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) :
F.prod' G G

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

Equations
@[simp]
theorem category_theory.functor.prod'_comp_snd_inv_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B) (G : A C) (X : A) :
(F.prod'_comp_snd G).inv.app X = 𝟙 (G.obj X)
def category_theory.functor.diag (C : Type u₃)  :
C C × C

The diagonal functor.

Equations
@[simp]
theorem category_theory.functor.diag_obj (C : Type u₃) (X : C) :
= (X, X)
@[simp]
theorem category_theory.functor.diag_map (C : Type u₃) {X Y : C} (f : X Y) :
= (f, f)
def category_theory.nat_trans.prod {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {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₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {F G : A B} {H I : C D} (α : F G) (β : H I) (X : A × C) :
= (α.app X.fst, β.app X.snd)
@[simp]
theorem category_theory.flip_comp_evaluation_hom_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B C) (a : A) (X : B) :
= 𝟙 ((F.obj a).obj X)
@[simp]
theorem category_theory.flip_comp_evaluation_inv_app {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B C) (a : A) (X : B) :
= 𝟙 ((F.obj a).obj X)
def category_theory.flip_comp_evaluation {A : Type u₁} {B : Type u₂} {C : Type u₃} (F : A B C) (a : A) :
F.flip a F.obj a

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

Equations
@[simp]
theorem category_theory.prod_functor_to_functor_prod_obj (A : Type u₁) (B : Type u₂) (C : Type u₃) (F : (A B) × (A C)) :
= F.fst.prod' F.snd
@[simp]
theorem category_theory.prod_functor_to_functor_prod_map_app (A : Type u₁) (B : Type u₂) (C : Type u₃) (F G : (A B) × (A C)) (f : F G) (X : A) :
f).app X = (f.fst.app X, f.snd.app X)
def category_theory.prod_functor_to_functor_prod (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
(A B) × (A C) A B × C

The forward direction for functor_prod_functor_equiv

Equations
@[simp]
theorem category_theory.functor_prod_to_prod_functor_obj (A : Type u₁) (B : Type u₂) (C : Type u₃) (F : A B × C) :
= ,
def category_theory.functor_prod_to_prod_functor (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
(A B × C) (A B) × (A C)

The backward direction for functor_prod_functor_equiv

Equations
@[simp]
theorem category_theory.functor_prod_to_prod_functor_map (A : Type u₁) (B : Type u₂) (C : Type u₃) (F G : A B × C) (α : F G) :
= ({app := λ (X : A), (α.app X).fst, naturality' := _}, {app := λ (X : A), (α.app X).snd, naturality' := _})
def category_theory.functor_prod_functor_equiv_unit_iso (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
𝟭 ((A B) × (A C))

The unit isomorphism for functor_prod_functor_equiv

Equations
@[simp]
theorem category_theory.functor_prod_functor_equiv_unit_iso_hom_app (A : Type u₁) (B : Type u₂) (C : Type u₃) (X : (A B) × (A C)) :
@[simp]
theorem category_theory.functor_prod_functor_equiv_unit_iso_inv_app (A : Type u₁) (B : Type u₂) (C : Type u₃) (X : (A B) × (A C)) :
@[simp]
theorem category_theory.functor_prod_functor_equiv_counit_iso_hom_app_app (A : Type u₁) (B : Type u₂) (C : Type u₃) (X : A B × C) (X_1 : A) :
X_1 = (𝟙 (X.obj X_1).fst, 𝟙 (X.obj X_1).snd)
@[simp]
theorem category_theory.functor_prod_functor_equiv_counit_iso_inv_app_app (A : Type u₁) (B : Type u₂) (C : Type u₃) (X : A B × C) (X_1 : A) :
X_1 = (𝟙 (X.obj X_1).fst, 𝟙 (X.obj X_1).snd)
def category_theory.functor_prod_functor_equiv_counit_iso (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
𝟭 (A B × C)

The counit isomorphism for functor_prod_functor_equiv

Equations
@[simp]
theorem category_theory.functor_prod_functor_equiv_functor (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
@[simp]
theorem category_theory.functor_prod_functor_equiv_unit_iso_2 (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
def category_theory.functor_prod_functor_equiv (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
(A B) × (A C) A B × C

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

Equations
@[simp]
theorem category_theory.functor_prod_functor_equiv_inverse (A : Type u₁) (B : Type u₂) (C : Type u₃)  :
@[simp]
theorem category_theory.functor_prod_functor_equiv_counit_iso_2 (A : Type u₁) (B : Type u₂) (C : Type u₃)  :