Cartesian products of categories

We define the category instance on C × D when C and D are categories.

We define:

• sectl C Z : the functor C ⥤ C × D given by X ↦ ⟨X, Z⟩
• sectr Z D : the functor D ⥤ C × D given by Y ↦ ⟨Z, Y⟩
• fst : the functor ⟨X, Y⟩ ↦ X
• snd : the functor ⟨X, Y⟩ ↦ Y
• swap : the functor C × D ⥤ D × C given by ⟨X, Y⟩ ↦ ⟨Y, X⟩ (and the fact this is an equivalence)

We further define evaluation : C ⥤ (C ⥤ D) ⥤ D and evaluationUncurried : C × (C ⥤ D) ⥤ D, and products of functors and natural transformations, written F.prod G and α.prod β.

@[simp]

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

@[simp]

theorem CategoryTheory.prod_comp_snd (C : Type u₁) [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).snd = CategoryTheory.CategoryStruct.comp f.snd g.snd

@[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).fst = CategoryTheory.CategoryStruct.id X.fst

@[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).snd = CategoryTheory.CategoryStruct.id X.snd

@[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).fst = CategoryTheory.CategoryStruct.comp f.fst g.fst

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_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 : C} {Q : C} {R : C} {S : D} {T : D} {U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : CategoryTheory.CategoryStruct.comp f g = (CategoryTheory.CategoryStruct.comp f.fst g.fst, CategoryTheory.CategoryStruct.comp f.snd g.snd)

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

@[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.fst, CategoryTheory.CategoryStruct.id X.snd)

@[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.fst, X.snd).fst, CategoryTheory.CategoryStruct.id (X.fst, X.snd).snd)

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

@[simp]

theorem CategoryTheory.Iso.prod_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {S : D} {T : D} (f : P ≅ Q) (g : S ≅ T) : (CategoryTheory.Iso.prod f g).hom = (f.hom, g.hom)

def CategoryTheory.Iso.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {S : D} {T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S) ≅ (Q, T)

Construct an isomorphism in C × D out of two isomorphisms in C and D.

Equations

• CategoryTheory.Iso.prod f g = CategoryTheory.Iso.mk (f.hom, g.hom) (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

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

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

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 = CategoryTheory.Functor.mk { obj := fun X => (X, Z), map := fun {X Y} f => (f, CategoryTheory.CategoryStruct.id Z) }

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

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

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 = CategoryTheory.Functor.mk { obj := fun X => (Z, X), map := fun {X Y} f => (CategoryTheory.CategoryStruct.id Z, f) }

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

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

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 = CategoryTheory.Functor.mk { obj := fun X => X.fst, map := fun {X Y} f => f.fst }

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

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

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 = CategoryTheory.Functor.mk { obj := fun X => X.snd, map := fun {X Y} f => f.snd }

@[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.snd, f.fst)

@[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.snd, X.fst)

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 = CategoryTheory.Functor.mk { obj := fun X => (X.snd, X.fst), map := fun {X Y} f => (f.snd, f.fst) }

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

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

def CategoryTheory.Prod.symmetry (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.Functor.comp (CategoryTheory.Prod.swap C D) (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.braiding_counitIso_inv_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : D × C) : (CategoryTheory.Prod.braiding C D).counitIso.inv.app X = (CategoryTheory.CategoryStruct.id X.fst, CategoryTheory.CategoryStruct.id X.snd)

@[simp]

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

@[simp]

theorem CategoryTheory.Prod.braiding_inverse_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : ∀ {X Y : D × C} (f : X ⟶ Y), (CategoryTheory.Prod.braiding C D).inverse.map f = (f.snd, f.fst)

@[simp]

theorem CategoryTheory.Prod.braiding_unitIso_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.braiding C D).unitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.fst, CategoryTheory.CategoryStruct.id X.snd)

@[simp]

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

@[simp]

theorem CategoryTheory.Prod.braiding_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.Prod.braiding C D).functor.map f = (f.snd, f.fst)

@[simp]

theorem CategoryTheory.Prod.braiding_unitIso_inv_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.braiding C D).unitIso.inv.app X = (CategoryTheory.CategoryStruct.id X.fst, CategoryTheory.CategoryStruct.id X.snd)

@[simp]

theorem CategoryTheory.Prod.braiding_counitIso_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : D × C) : (CategoryTheory.Prod.braiding C D).counitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.fst, CategoryTheory.CategoryStruct.id X.snd)

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.

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

Equations

• CategoryTheory.Prod.swapIsEquivalence C D = inferInstance

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

@[simp]

theorem CategoryTheory.evaluation_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (f : X ⟶ Y) (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

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.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.snd.obj p.fst

@[simp]

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

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.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.constCompEvaluationObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) : CategoryTheory.Functor.comp (CategoryTheory.Functor.const C) ((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.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), (CategoryTheory.Functor.prod F G).map f = (F.map f.fst, G.map f.snd)

@[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) : (CategoryTheory.Functor.prod F G).obj X = (F.obj X.fst, G.obj X.snd)

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

• CategoryTheory.Functor.prod F G = CategoryTheory.Functor.mk { obj := fun X => (F.obj X.fst, G.obj X.snd), map := fun {X Y} f => (F.map f.fst, G.map f.snd) }

@[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) : (CategoryTheory.Functor.prod' F 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), (CategoryTheory.Functor.prod' F G).map f = (F.map f, G.map f)

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

• CategoryTheory.Functor.prod' F G = CategoryTheory.Functor.mk { obj := fun a => (F.obj a, G.obj a), map := fun {X Y} f => (F.map f, G.map f) }

@[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) : (CategoryTheory.Functor.prod'CompFst F G).inv.app X = CategoryTheory.CategoryStruct.id (F.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) : (CategoryTheory.Functor.prod'CompFst F G).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

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) : CategoryTheory.Functor.comp (CategoryTheory.Functor.prod' F G) (CategoryTheory.Prod.fst B C) ≅ F

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

Equations

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

@[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) : (CategoryTheory.Functor.prod'CompSnd F G).inv.app X = CategoryTheory.CategoryStruct.id (G.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) : (CategoryTheory.Functor.prod'CompSnd F G).hom.app X = CategoryTheory.CategoryStruct.id (G.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) : CategoryTheory.Functor.comp (CategoryTheory.Functor.prod' F G) (CategoryTheory.Prod.snd B C) ≅ G

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

Equations

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

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.prod' (CategoryTheory.Functor.id C) (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 : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Functor.diag C).map f = (f, f)

@[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 : CategoryTheory.Functor A B} {G : CategoryTheory.Functor A B} {H : CategoryTheory.Functor C D} {I : CategoryTheory.Functor C D} (α : F ⟶ G) (β : H ⟶ I) (X : A × C) : (CategoryTheory.NatTrans.prod α β).app X = (α.app X.fst, β.app X.snd)

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 : CategoryTheory.Functor A B} {G : CategoryTheory.Functor A B} {H : CategoryTheory.Functor C D} {I : CategoryTheory.Functor C D} (α : F ⟶ G) (β : H ⟶ I) : CategoryTheory.Functor.prod F H ⟶ CategoryTheory.Functor.prod G I

The cartesian product of two natural transformations.

Equations

• CategoryTheory.NatTrans.prod α β = CategoryTheory.NatTrans.mk fun X => (α.app X.fst, β.app X.snd)

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

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) : CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) ((CategoryTheory.evaluation A C).obj a) ≅ F.obj a

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

Equations

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

@[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 = CategoryTheory.Functor.prod' F.fst F.snd

@[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_1 : A), ((CategoryTheory.prodFunctorToFunctorProd A B C).map f).app X_1 = (f.fst.app X_1, f.snd.app X_1)

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.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 α = (CategoryTheory.NatTrans.mk fun X_1 => (α.app X_1).fst, CategoryTheory.NatTrans.mk fun X_1 => (α.app X_1).snd)

@[simp]

theorem CategoryTheory.functorProdToProdFunctor_obj (A : Type u₁) [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 = (CategoryTheory.Functor.comp F (CategoryTheory.Prod.fst B C), CategoryTheory.Functor.comp F (CategoryTheory.Prod.snd B C))

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.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 = ((CategoryTheory.Functor.prod'CompFst X.fst X.snd).inv, (CategoryTheory.Functor.prod'CompSnd X.fst X.snd).inv)

@[simp]

theorem CategoryTheory.functorProdFunctorEquivUnitIso_inv_app (A : Type u₁) [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 = ((CategoryTheory.Functor.prod'CompFst X.fst X.snd).hom, (CategoryTheory.Functor.prod'CompSnd X.fst X.snd).hom)

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.Functor.comp (CategoryTheory.prodFunctorToFunctorProd A B C) (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.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).fst, CategoryTheory.CategoryStruct.id (X.obj X).snd)

@[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).fst, CategoryTheory.CategoryStruct.id (X.obj X).snd)

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.Functor.comp (CategoryTheory.functorProdToProdFunctor A B C) (CategoryTheory.prodFunctorToFunctorProd A B C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor A (B × C))

The counit isomorphism for functorProdFunctorEquiv

Equations

• CategoryTheory.functorProdFunctorEquivCounitIso A B C = CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.prod.etaIso (F.obj X)

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

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

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.