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

prod C D gives the cartesian product of two categories.

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

Equations

• CategoryTheory.prod C D = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

Equations

• f.prod g = { hom := (f.hom, g.hom), inv := (f.inv, g.inv), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

Equations

• CategoryTheory.uniformProd C D = CategoryTheory.prod C D

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

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

Equations

• CategoryTheory.Prod.sectL C Z = { obj := fun (X : C) => (X, Z), map := fun {X Y : C} (f : X ⟶ Y) => (f, CategoryTheory.CategoryStruct.id Z), map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Prod.sectR Z D = { obj := fun (X : D) => (Z, X), map := fun {X Y : D} (f : X ⟶ Y) => (CategoryTheory.CategoryStruct.id Z, f), map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

@[deprecated CategoryTheory.Prod.sectL]

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

Alias of CategoryTheory.Prod.sectL.

---

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

Equations

• CategoryTheory.Prod.sectl = CategoryTheory.Prod.sectL

@[deprecated CategoryTheory.Prod.sectR]

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

Alias of CategoryTheory.Prod.sectR.

---

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

Equations

• @CategoryTheory.Prod.sectr = @CategoryTheory.Prod.sectR

@[deprecated CategoryTheory.Prod.sectL_obj]

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

Alias of CategoryTheory.Prod.sectL_obj.

@[deprecated CategoryTheory.Prod.sectR_obj]

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

Alias of CategoryTheory.Prod.sectR_obj.

@[deprecated CategoryTheory.Prod.sectL_map]

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

Alias of CategoryTheory.Prod.sectL_map.

@[deprecated CategoryTheory.Prod.sectR_map]

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

Alias of CategoryTheory.Prod.sectR_map.

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

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

Equations

• CategoryTheory.Prod.fst C D = { obj := fun (X : C × D) => X.1, map := fun {X Y : C × D} (f : X ⟶ Y) => f.1, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Prod.snd C D = { obj := fun (X : C × D) => X.2, map := fun {X Y : C × D} (f : X ⟶ Y) => f.2, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Prod.swap C D = { 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 := ⋯ }

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

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

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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.prod_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) : CategoryTheory.Functor A (B × C)

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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.prod'_obj {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) : (F.prod' G).comp (CategoryTheory.Prod.fst B C) ≅ F

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

Equations

• F.prod'CompFst G = CategoryTheory.NatIso.ofComponents (fun (x : A) => CategoryTheory.Iso.refl (((F.prod' G).comp (CategoryTheory.Prod.fst B C)).obj x)) ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• F.prod'CompSnd G = CategoryTheory.NatIso.ofComponents (fun (x : A) => CategoryTheory.Iso.refl (((F.prod' G).comp (CategoryTheory.Prod.snd B C)).obj x)) ⋯

@[simp]

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

@[simp]

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

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

The diagonal functor.

Equations

• CategoryTheory.Functor.diag C = (CategoryTheory.Functor.id C).prod' (CategoryTheory.Functor.id C)

@[simp]

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

@[simp]

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

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

The cartesian product of two natural transformations.

Equations

• CategoryTheory.NatTrans.prod α β = { app := fun (X : A × C) => (α.app X.1, β.app X.2), naturality := ⋯ }

@[simp]

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

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

The cartesian product of two natural transformations.

Equations

• CategoryTheory.NatTrans.prod' α β = { app := fun (X : A) => (α.app X, β.app X), naturality := ⋯ }

@[simp]

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

@[simp]

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

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

The cartesian product functor between functor categories

Equations

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

@[simp]

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

@[simp]

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

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

The cartesian product of two natural isomorphisms.

Equations

• CategoryTheory.NatIso.prod e₁ e₂ = { hom := CategoryTheory.NatTrans.prod e₁.hom e₂.hom, inv := CategoryTheory.NatTrans.prod e₁.inv e₂.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.Equivalence.prod {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (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.

@[simp]

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

@[simp]

theorem CategoryTheory.Equivalence.prod_inverse {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso

@[simp]

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

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

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

Equations

• CategoryTheory.flipCompEvaluation F a = CategoryTheory.NatIso.ofComponents (fun (b : B) => CategoryTheory.Iso.refl ((F.flip.comp ((CategoryTheory.evaluation A C).obj a)).obj b)) ⋯

@[simp]

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

@[simp]

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

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

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

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

Equations

• CategoryTheory.compEvaluation F b = CategoryTheory.NatIso.ofComponents (fun (a : A) => CategoryTheory.Iso.refl ((F.comp ((CategoryTheory.evaluation B C).obj b)).obj a)) ⋯

@[simp]

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

@[simp]

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

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

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

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

Equations

• CategoryTheory.whiskeringLeftCompEvaluation F a = CategoryTheory.Iso.refl (((CategoryTheory.whiskeringLeft A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a))

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.whiskeringLeft_comp_evaluation {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (a : A) : ((CategoryTheory.whiskeringLeft A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) = (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) : ((CategoryTheory.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) ≅ ((CategoryTheory.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.

Equations

• CategoryTheory.whiskeringRightCompEvaluation F a = CategoryTheory.Iso.refl (((CategoryTheory.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a))

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.whiskeringRight_comp_evaluation {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) : ((CategoryTheory.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) = ((CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Functor (CategoryTheory.Functor A B × CategoryTheory.Functor A C) (CategoryTheory.Functor A (B × C))

The forward direction for functorProdFunctorEquiv

Equations

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

@[simp]

theorem CategoryTheory.prodFunctorToFunctorProd_map_app (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : CategoryTheory.Functor A B × CategoryTheory.Functor A C} (f : X✝ ⟶ Y✝) (X : A) : ((CategoryTheory.prodFunctorToFunctorProd A B C).map f).app X = (f.1.app X, f.2.app X)

@[simp]

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

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

The backward direction for functorProdFunctorEquiv

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.functorProdToProdFunctor_map (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : CategoryTheory.Functor A (B × C)} (α : X✝ ⟶ Y✝) : (CategoryTheory.functorProdToProdFunctor A B C).map α = ({ app := fun (X : A) => (α.app X).1, naturality := ⋯ }, { app := fun (X : A) => (α.app X).2, naturality := ⋯ })

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

The unit isomorphism for functorProdFunctorEquiv

Equations

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

@[simp]

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

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

The counit isomorphism for functorProdFunctorEquiv

Equations

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

@[simp]

theorem CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).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₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X✝ = (CategoryTheory.CategoryStruct.id (X.obj X✝).1, CategoryTheory.CategoryStruct.id (X.obj X✝).2)

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

theorem CategoryTheory.prodOpEquiv_unitIso (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] : (CategoryTheory.prodOpEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × D)ᵒᵖ)

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.prodOpEquiv_counitIso (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] : (CategoryTheory.prodOpEquiv C).counitIso = CategoryTheory.Iso.refl ({ obj := fun (x : Cᵒᵖ × Dᵒᵖ) => match x with | (X, Y) => Opposite.op (Opposite.unop X, Opposite.unop 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 (Opposite.unop X).1, Opposite.op (Opposite.unop X).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_functor_map (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : (C × D)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).functor.map f = (f.unop.1.op, f.unop.2.op)