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

instance CategoryTheory.prod (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Category.{max v₁ v₂, max u₂ u₁} (C × D)

prod C D gives the cartesian product of two categories.

Stacks Tag 001K

@[simp]

theorem CategoryTheory.prod_id_snd (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (CategoryStruct.id X).2 = CategoryStruct.id X.2

@[simp]

theorem CategoryTheory.prod_comp_fst (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ Z✝ : C × D} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) : (CategoryStruct.comp f g).1 = CategoryStruct.comp f.1 g.1

@[simp]

theorem CategoryTheory.prod_comp_snd (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ Z✝ : C × D} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) : (CategoryStruct.comp f g).2 = CategoryStruct.comp f.2 g.2

@[simp]

theorem CategoryTheory.prod_id_fst (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (CategoryStruct.id X).1 = CategoryStruct.id X.1

@[simp]

theorem CategoryTheory.prod_Hom (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X Y : C × D) : (X ⟶ Y) = ((X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))

theorem CategoryTheory.prod.hom_ext (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X Y : C × D} {f g : X ⟶ Y} (h₁ : f.1 = g.1) (h₂ : f.2 = g.2) : f = g

theorem CategoryTheory.prod.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C × D} {f g : X ⟶ Y} : f = g ↔ f.1 = g.1 ∧ f.2 = g.2

@[simp]

theorem CategoryTheory.prod_id (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) (Y : D) : CategoryStruct.id (X, Y) = (CategoryStruct.id X, CategoryStruct.id Y)

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

@[simp]

theorem CategoryTheory.prod_comp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : CategoryStruct.comp f g = (CategoryStruct.comp f.1 g.1, CategoryStruct.comp f.2 g.2)

@[reducible, inline]

abbrev CategoryTheory.Prod.mkHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X₁ X₂ : C} {Y₁ Y₂ : D} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (X₁, Y₁) ⟶ (X₂, Y₂)

Construct a morphism in a product category by giving its constituent components. This constructor should be preferred over Prod.mk, because lean infers better the source and target of the resulting morphism.

def CategoryTheory.Prod.«term_×ₘ_» : Lean.TrailingParserDescr

Construct a morphism in a product category by giving its constituent components. This constructor should be preferred over Prod.mk, because lean infers better the source and target of the resulting morphism.

theorem CategoryTheory.isIso_prod_iff (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} : IsIso f ↔ IsIso f.1 ∧ IsIso f.2

def CategoryTheory.prod.etaIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (X : C × D) : (X.1, X.2) ≅ X

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

@[simp]

theorem CategoryTheory.prod.etaIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (X : C × D) : (etaIso X).inv = (CategoryStruct.id X.1, CategoryStruct.id X.2)

@[simp]

theorem CategoryTheory.prod.etaIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (X : C × D) : (etaIso X).hom = (CategoryStruct.id (X.1, X.2).1, CategoryStruct.id (X.1, X.2).2)

def CategoryTheory.Iso.prod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {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.

@[simp]

theorem CategoryTheory.Iso.prod_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P Q : C} {S 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (f.prod g).inv = (f.inv, g.inv)

instance CategoryTheory.uniformProd (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] : Category.{v₁, u₁} (C × D)

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

def CategoryTheory.Prod.sectL (C : Type u₁) [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (Z : D) : Functor C (C × D)

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

@[simp]

theorem CategoryTheory.Prod.sectL_obj (C : Type u₁) [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (Z : D) (X : C) : (sectL C Z).obj X = (X, Z)

@[simp]

theorem CategoryTheory.Prod.sectL_map (C : Type u₁) [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (Z : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (sectL C Z).map f = (f, CategoryStruct.id Z)

def CategoryTheory.Prod.sectR {C : Type u₁} [Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [Category.{v₂, u₂} D] : Functor D (C × D)

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

@[simp]

theorem CategoryTheory.Prod.sectR_obj {C : Type u₁} [Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [Category.{v₂, u₂} D] (X : D) : (sectR Z D).obj X = (Z, X)

@[simp]

theorem CategoryTheory.Prod.sectR_map {C : Type u₁} [Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (sectR Z D).map f = (CategoryStruct.id Z, f)

def CategoryTheory.Prod.fst (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C × D) C

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

@[simp]

theorem CategoryTheory.Prod.fst_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (fst C D).map f = f.1

@[simp]

theorem CategoryTheory.Prod.fst_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (fst C D).obj X = X.1

def CategoryTheory.Prod.snd (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C × D) D

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

@[simp]

theorem CategoryTheory.Prod.snd_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (snd C D).map f = f.2

@[simp]

theorem CategoryTheory.Prod.snd_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (snd C D).obj X = X.2

def CategoryTheory.Prod.swap (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C × D) (D × C)

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

@[simp]

theorem CategoryTheory.Prod.swap_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (swap C D).map f = (f.2, f.1)

@[simp]

theorem CategoryTheory.Prod.swap_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (swap C D).obj X = (X.2, X.1)

def CategoryTheory.Prod.symmetry (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (swap C D).comp (swap D C) ≅ Functor.id (C × D)

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

@[simp]

theorem CategoryTheory.Prod.symmetry_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (symmetry C D).hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Prod.symmetry_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C × D) : (symmetry C D).inv.app X = CategoryStruct.id X

def CategoryTheory.Prod.braiding (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : C × D ≌ D × C

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

@[simp]

theorem CategoryTheory.Prod.braiding_unitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (braiding C D).unitIso = Iso.refl (Functor.id (C × D))

@[simp]

theorem CategoryTheory.Prod.braiding_counitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (braiding C D).counitIso = Iso.refl ((swap D C).comp (swap C D))

@[simp]

theorem CategoryTheory.Prod.braiding_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (braiding C D).functor = swap C D

@[simp]

theorem CategoryTheory.Prod.braiding_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (braiding C D).inverse = swap D C

instance CategoryTheory.Prod.swapIsEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (swap C D).IsEquivalence

theorem CategoryTheory.Prod.fac {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryStruct.comp (mkHom (CategoryStruct.id x.1) f.2) (mkHom f.1 (CategoryStruct.id y.2))

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.

theorem CategoryTheory.Prod.fac_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryStruct.comp f h = CategoryStruct.comp (mkHom (CategoryStruct.id x.1) f.2) (CategoryStruct.comp (mkHom f.1 (CategoryStruct.id y.2)) h)

theorem CategoryTheory.Prod.fac' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryStruct.comp (mkHom f.1 (CategoryStruct.id x.2)) (mkHom (CategoryStruct.id y.1) f.2)

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.

theorem CategoryTheory.Prod.fac'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryStruct.comp f h = CategoryStruct.comp (mkHom f.1 (CategoryStruct.id x.2)) (CategoryStruct.comp (mkHom (CategoryStruct.id y.1) f.2) h)

def CategoryTheory.evaluation (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor C (Functor (Functor 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.

@[simp]

theorem CategoryTheory.evaluation_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) (F : Functor C D) : ((evaluation C D).obj X).obj F = F.obj X

@[simp]

theorem CategoryTheory.evaluation_map_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) (F : Functor C D) : ((evaluation C D).map f).app F = F.map f

@[simp]

theorem CategoryTheory.evaluation_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) {X✝ Y✝ : Functor C D} (α : X✝ ⟶ Y✝) : ((evaluation C D).obj X).map α = α.app X

def CategoryTheory.evaluationUncurried (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C × Functor C D) D

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

@[simp]

theorem CategoryTheory.evaluationUncurried_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {x y : C × Functor C D} (f : x ⟶ y) : (evaluationUncurried C D).map f = CategoryStruct.comp (x.2.map f.1) (f.2.app y.1)

@[simp]

theorem CategoryTheory.evaluationUncurried_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (p : C × Functor C D) : (evaluationUncurried C D).obj p = p.2.obj p.1

def CategoryTheory.Functor.constCompEvaluationObj {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) : (const C).comp ((evaluation C D).obj X) ≅ Functor.id D

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

@[simp]

theorem CategoryTheory.Functor.constCompEvaluationObj_inv_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) (X✝ : D) : (constCompEvaluationObj D X).inv.app X✝ = CategoryStruct.id X✝

@[simp]

theorem CategoryTheory.Functor.constCompEvaluationObj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) (X✝ : D) : (constCompEvaluationObj D X).hom.app X✝ = CategoryStruct.id X✝

def CategoryTheory.Functor.prod {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (F : Functor A B) (G : Functor C D) : Functor (A × C) (B × D)

The cartesian product of two functors.

@[simp]

theorem CategoryTheory.Functor.prod_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (F : Functor A B) (G : Functor C D) {X✝ Y✝ : A × C} (f : X✝ ⟶ Y✝) : (F.prod G).map f = (F.map f.1, G.map f.2)

@[simp]

theorem CategoryTheory.Functor.prod_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (F : Functor A B) (G : Functor C D) (X : A × C) : (F.prod G).obj X = (F.obj X.1, G.obj X.2)

def CategoryTheory.Functor.prod' {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) : Functor A (B × C)

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

@[simp]

theorem CategoryTheory.Functor.prod'_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) (a : A) : (F.prod' G).obj a = (F.obj a, G.obj a)

@[simp]

theorem CategoryTheory.Functor.prod'_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : (F.prod' G).map f = (F.map f, G.map f)

def CategoryTheory.Functor.prod'CompFst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) : (F.prod' G).comp (Prod.fst B C) ≅ F

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

@[simp]

theorem CategoryTheory.Functor.prod'CompFst_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) (X : A) : (F.prod'CompFst G).hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.prod'CompFst_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) (X : A) : (F.prod'CompFst G).inv.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.prod'CompSnd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) : (F.prod' G).comp (Prod.snd B C) ≅ G

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

@[simp]

theorem CategoryTheory.Functor.prod'CompSnd_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) (X : A) : (F.prod'CompSnd G).hom.app X = CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Functor.prod'CompSnd_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor A C) (X : A) : (F.prod'CompSnd G).inv.app X = CategoryStruct.id (G.obj X)

def CategoryTheory.Functor.diag (C : Type u₃) [Category.{v₃, u₃} C] : Functor C (C × C)

The diagonal functor.

@[simp]

theorem CategoryTheory.Functor.diag_map (C : Type u₃) [Category.{v₃, u₃} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (diag C).map f = (f, f)

@[simp]

theorem CategoryTheory.Functor.diag_obj (C : Type u₃) [Category.{v₃, u₃} C] (a : C) : (diag C).obj a = (a, a)

def CategoryTheory.NatTrans.prod {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I

The cartesian product of two natural transformations.

@[simp]

theorem CategoryTheory.NatTrans.prod_app_snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) (X : A × C) : ((prod α β).app X).2 = β.app X.2

@[simp]

theorem CategoryTheory.NatTrans.prod_app_fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) (X : A × C) : ((prod α β).app X).1 = α.app X.1

def CategoryTheory.NatTrans.prod' {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor A B} {H K : Functor A C} (α : F ⟶ G) (β : H ⟶ K) : F.prod' H ⟶ G.prod' K

The cartesian product of two natural transformations where both functors have the same source.

@[simp]

theorem CategoryTheory.NatTrans.prod'_app_fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor A B} {H K : Functor A C} (α : F ⟶ G) (β : H ⟶ K) (X : A) : ((prod' α β).app X).1 = α.app X

@[simp]

theorem CategoryTheory.NatTrans.prod'_app_snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor A B} {H K : Functor A C} (α : F ⟶ G) (β : H ⟶ K) (X : A) : ((prod' α β).app X).2 = β.app X

def CategoryTheory.prodFunctor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] : Functor (Functor A B × Functor C D) (Functor (A × C) (B × D))

The cartesian product functor between functor categories

@[simp]

theorem CategoryTheory.prodFunctor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {X✝ Y✝ : Functor A B × Functor C D} (nm : X✝ ⟶ Y✝) : prodFunctor.map nm = NatTrans.prod nm.1 nm.2

@[simp]

theorem CategoryTheory.prodFunctor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (FG : Functor A B × Functor C D) : prodFunctor.obj FG = FG.1.prod FG.2

def CategoryTheory.NatIso.prod {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F F' : Functor A B} {G G' : Functor C D} (e₁ : F ≅ F') (e₂ : G ≅ G') : F.prod G ≅ F'.prod G'

The cartesian product of two natural isomorphisms.

@[simp]

theorem CategoryTheory.NatIso.prod_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F F' : Functor A B} {G G' : Functor C D} (e₁ : F ≅ F') (e₂ : G ≅ G') : (prod e₁ e₂).hom = NatTrans.prod e₁.hom e₂.hom

@[simp]

theorem CategoryTheory.NatIso.prod_inv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F F' : Functor A B} {G G' : Functor C D} (e₁ : F ≅ F') (e₂ : G ≅ G') : (prod e₁ e₂).inv = NatTrans.prod e₁.inv e₂.inv

def CategoryTheory.Equivalence.prod {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D

The cartesian product of two equivalences of categories.

@[simp]

theorem CategoryTheory.Equivalence.prod_functor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).functor = E₁.functor.prod E₂.functor

@[simp]

theorem CategoryTheory.Equivalence.prod_counitIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).counitIso = NatIso.prod E₁.counitIso E₂.counitIso

@[simp]

theorem CategoryTheory.Equivalence.prod_inverse {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).inverse = E₁.inverse.prod E₂.inverse

@[simp]

theorem CategoryTheory.Equivalence.prod_unitIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).unitIso = NatIso.prod E₁.unitIso E₂.unitIso

def CategoryTheory.flipCompEvaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (a : A) : F.flip.comp ((evaluation A C).obj a) ≅ F.obj a

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

@[simp]

theorem CategoryTheory.flipCompEvaluation_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (a : A) (X : B) : (flipCompEvaluation F a).inv.app X = CategoryStruct.id ((F.obj a).obj X)

@[simp]

theorem CategoryTheory.flipCompEvaluation_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (a : A) (X : B) : (flipCompEvaluation F a).hom.app X = CategoryStruct.id ((F.obj a).obj X)

theorem CategoryTheory.flip_comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (a : A) : F.flip.comp ((evaluation A C).obj a) = F.obj a

def CategoryTheory.compEvaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (b : B) : F.comp ((evaluation B C).obj b) ≅ F.flip.obj b

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

@[simp]

theorem CategoryTheory.compEvaluation_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (b : B) (X : A) : (compEvaluation F b).inv.app X = CategoryStruct.id ((F.obj X).obj b)

@[simp]

theorem CategoryTheory.compEvaluation_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (b : B) (X : A) : (compEvaluation F b).hom.app X = CategoryStruct.id ((F.obj X).obj b)

theorem CategoryTheory.comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A (Functor B C)) (b : B) : F.comp ((evaluation B C).obj b) = F.flip.obj b

def CategoryTheory.whiskeringLeftCompEvaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (a : A) : ((Functor.whiskeringLeft A B C).obj F).comp ((evaluation A C).obj a) ≅ (evaluation B C).obj (F.obj a)

Whiskering by F and then evaluating at a is the same as evaluating at F.obj a.

@[simp]

theorem CategoryTheory.whiskeringLeftCompEvaluation_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (a : A) (X : Functor B C) : (whiskeringLeftCompEvaluation F a).inv.app X = CategoryStruct.id (X.obj (F.obj a))

@[simp]

theorem CategoryTheory.whiskeringLeftCompEvaluation_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (a : A) (X : Functor B C) : (whiskeringLeftCompEvaluation F a).hom.app X = CategoryStruct.id (X.obj (F.obj a))

@[simp]

theorem CategoryTheory.whiskeringLeft_comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (a : A) : ((Functor.whiskeringLeft A B C).obj F).comp ((evaluation A C).obj a) = (evaluation B C).obj (F.obj a)

Whiskering by F and then evaluating at a is the same as evaluating at F.obj a.

def CategoryTheory.whiskeringRightCompEvaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor B C) (a : A) : ((Functor.whiskeringRight A B C).obj F).comp ((evaluation A C).obj a) ≅ ((evaluation A B).obj a).comp F

Whiskering by F and then evaluating at a is the same as evaluating at F and then applying F.

@[simp]

theorem CategoryTheory.whiskeringRightCompEvaluation_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor B C) (a : A) (X : Functor A B) : (whiskeringRightCompEvaluation F a).inv.app X = CategoryStruct.id (F.obj (X.obj a))

@[simp]

theorem CategoryTheory.whiskeringRightCompEvaluation_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor B C) (a : A) (X : Functor A B) : (whiskeringRightCompEvaluation F a).hom.app X = CategoryStruct.id (F.obj (X.obj a))

@[simp]

theorem CategoryTheory.whiskeringRight_comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor B C) (a : A) : ((Functor.whiskeringRight A B C).obj F).comp ((evaluation A C).obj a) = ((evaluation A B).obj a).comp F

Whiskering by F and then evaluating at a is the same as evaluating at F and then applying F.

def CategoryTheory.prodFunctorToFunctorProd (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : Functor (Functor A B × Functor A C) (Functor A (B × C))

The forward direction for functorProdFunctorEquiv

@[simp]

theorem CategoryTheory.prodFunctorToFunctorProd_obj (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (F : Functor A B × Functor A C) : (prodFunctorToFunctorProd A B C).obj F = F.1.prod' F.2

@[simp]

theorem CategoryTheory.prodFunctorToFunctorProd_map (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] {F G : Functor A B × Functor A C} (f : F ⟶ G) : (prodFunctorToFunctorProd A B C).map f = NatTrans.prod' f.1 f.2

def CategoryTheory.functorProdToProdFunctor (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : Functor (Functor A (B × C)) (Functor A B × Functor A C)

The backward direction for functorProdFunctorEquiv

@[simp]

theorem CategoryTheory.functorProdToProdFunctor_map (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] {X✝ Y✝ : Functor A (B × C)} (α : X✝ ⟶ Y✝) : (functorProdToProdFunctor A B C).map α = (Functor.whiskerRight α (Prod.fst B C), Functor.whiskerRight α (Prod.snd B C))

@[simp]

theorem CategoryTheory.functorProdToProdFunctor_obj (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (F : Functor A (B × C)) : (functorProdToProdFunctor A B C).obj F = (F.comp (Prod.fst B C), F.comp (Prod.snd B C))

def CategoryTheory.functorProdFunctorEquivUnitIso (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : Functor.id (Functor A B × Functor A C) ≅ (prodFunctorToFunctorProd A B C).comp (functorProdToProdFunctor A B C)

The unit isomorphism for functorProdFunctorEquiv

@[simp]

theorem CategoryTheory.functorProdFunctorEquivUnitIso_hom_app (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (X : Functor A B × Functor A C) : (functorProdFunctorEquivUnitIso A B C).hom.app X = ((X.1.prod'CompFst X.2).inv, (X.1.prod'CompSnd X.2).inv)

@[simp]

theorem CategoryTheory.functorProdFunctorEquivUnitIso_inv_app (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (X : Functor A B × Functor A C) : (functorProdFunctorEquivUnitIso A B C).inv.app X = ((X.1.prod'CompFst X.2).hom, (X.1.prod'CompSnd X.2).hom)

def CategoryTheory.functorProdFunctorEquivCounitIso (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : (functorProdToProdFunctor A B C).comp (prodFunctorToFunctorProd A B C) ≅ Functor.id (Functor A (B × C))

The counit isomorphism for functorProdFunctorEquiv

@[simp]

theorem CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (X : Functor A (B × C)) (X✝ : A) : ((functorProdFunctorEquivCounitIso A B C).hom.app X).app X✝ = (CategoryStruct.id (X.obj X✝).1, CategoryStruct.id (X.obj X✝).2)

@[simp]

theorem CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] (X : Functor A (B × C)) (X✝ : A) : ((functorProdFunctorEquivCounitIso A B C).inv.app X).app X✝ = (CategoryStruct.id (X.obj X✝).1, CategoryStruct.id (X.obj X✝).2)

def CategoryTheory.functorProdFunctorEquiv (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : Functor A B × Functor A C ≌ Functor A (B × C)

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

@[simp]

theorem CategoryTheory.functorProdFunctorEquiv_functor (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : (functorProdFunctorEquiv A B C).functor = prodFunctorToFunctorProd A B C

@[simp]

theorem CategoryTheory.functorProdFunctorEquiv_inverse (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : (functorProdFunctorEquiv A B C).inverse = functorProdToProdFunctor A B C

@[simp]

theorem CategoryTheory.functorProdFunctorEquiv_counitIso (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : (functorProdFunctorEquiv A B C).counitIso = functorProdFunctorEquivCounitIso A B C

@[simp]

theorem CategoryTheory.functorProdFunctorEquiv_unitIso (A : Type u₁) [Category.{v₁, u₁} A] (B : Type u₂) [Category.{v₂, u₂} B] (C : Type u₃) [Category.{v₃, u₃} C] : (functorProdFunctorEquiv A B C).unitIso = functorProdFunctorEquivUnitIso A B C

def CategoryTheory.prodOpEquiv (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] : (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ

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

@[simp]

theorem CategoryTheory.prodOpEquiv_counitIso_inv_app (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (X : Cᵒᵖ × Dᵒᵖ) : (prodOpEquiv C).counitIso.inv.app X = (CategoryStruct.id X.1, CategoryStruct.id X.2)

@[simp]

theorem CategoryTheory.prodOpEquiv_unitIso_hom_app (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (prodOpEquiv C).unitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.prodOpEquiv_counitIso_hom_app (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (X : Cᵒᵖ × Dᵒᵖ) : (prodOpEquiv C).counitIso.hom.app X = (CategoryStruct.id X.1, CategoryStruct.id X.2)

@[simp]

theorem CategoryTheory.prodOpEquiv_functor_map (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {X✝ Y✝ : (C × D)ᵒᵖ} (f : X✝ ⟶ Y✝) : (prodOpEquiv C).functor.map f = (f.unop.1.op, f.unop.2.op)

@[simp]

theorem CategoryTheory.prodOpEquiv_inverse_map (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {X✝ Y✝ : Cᵒᵖ × Dᵒᵖ} (x✝ : X✝ ⟶ Y✝) : (prodOpEquiv C).inverse.map x✝ = Opposite.op (x✝.1.unop, x✝.2.unop)

@[simp]

theorem CategoryTheory.prodOpEquiv_functor_obj (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (prodOpEquiv C).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)

@[simp]

theorem CategoryTheory.prodOpEquiv_inverse_obj (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (x✝ : Cᵒᵖ × Dᵒᵖ) : (prodOpEquiv C).inverse.obj x✝ = Opposite.op (Opposite.unop x✝.1, Opposite.unop x✝.2)

@[simp]

theorem CategoryTheory.prodOpEquiv_unitIso_inv_app (C : Type u₃) [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (prodOpEquiv C).unitIso.inv.app X = CategoryStruct.id X