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

source

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

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

Equations

CategoryTheory.uniformProd C D = CategoryTheory.prod C D

source

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

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

source

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

source

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

source

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

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

source

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

source

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

source

@[deprecated CategoryTheory.Prod.sectL (since := "2024-11-12")]

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

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

source

@[deprecated CategoryTheory.Prod.sectR (since := "2024-11-12")]

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

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

source

@[deprecated CategoryTheory.Prod.sectL_obj (since := "2024-11-12")]

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)

Alias of CategoryTheory.Prod.sectL_obj.

source

@[deprecated CategoryTheory.Prod.sectR_obj (since := "2024-11-12")]

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)

Alias of CategoryTheory.Prod.sectR_obj.

source

@[deprecated CategoryTheory.Prod.sectL_map (since := "2024-11-12")]

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)

Alias of CategoryTheory.Prod.sectL_map.

source

@[deprecated CategoryTheory.Prod.sectR_map (since := "2024-11-12")]

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)

Alias of CategoryTheory.Prod.sectR_map.

source

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.

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

source

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

source

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

source

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.

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

source

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

source

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

source

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.

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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

source

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

source

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

(swap C D).IsEquivalence

source

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 (CategoryStruct.id x.1, f.2) (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.

source

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 (CategoryStruct.id x.1, f.2) (CategoryStruct.comp (f.1, CategoryStruct.id y.2) h)

source

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 (f.1, CategoryStruct.id x.2) (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.

source

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 (f.1, CategoryStruct.id x.2) (CategoryStruct.comp (CategoryStruct.id y.1, f.2) h)

source

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.

Equations

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

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

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

source

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

source

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

source

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

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

source

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

source

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

source

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

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)) ⋯

source

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

source

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

source

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

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)) ⋯

source

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

source

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

source

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

Functor C (C × C)

The diagonal functor.

Equations

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

source

@[simp]

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

(diag C).obj a = (a, a)

source

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

source

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.

Equations

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

source

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

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] {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

source

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.

Equations

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

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

source

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

source

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

Equations

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

source

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

source

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

source

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.

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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

source

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

source

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.

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)) ⋯

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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

source

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) :

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

Equations

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

source

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

source

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

source

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

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

source

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) :

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

Equations

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

source

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

source

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

source

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

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

source

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

Equations

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

source

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

source

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

source

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

Equations

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

source

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

source

@[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 α = (whiskerRight α (Prod.fst B C), whiskerRight α (Prod.snd B C))

source

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

Equations

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

source

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

source

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

source

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

Equations

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

source

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

source

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

source

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)

Equations

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

source

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

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.CategoryTheory.Products.Basic

Cartesian products of categories #