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 that 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

@[implicit_reducible]

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

CategoryStruct.{max v₁ v₂, max u₂ u₁} (C × D)

CategoryStruct.prod C D gives the Cartesian product of two CategoryStruct's.

source

@[simp]

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

(CategoryStruct.id X).2 = CategoryStruct.id X.2

source

@[simp]

theorem CategoryTheory.prod_comp_snd (C : Type u₁) [CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryStruct.{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_comp_fst (C : Type u₁) [CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryStruct.{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_Hom (C : Type u₁) [CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryStruct.{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₁) [CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryStruct.{v₂, u₂} D] (X : C × D) :

(CategoryStruct.id X).1 = CategoryStruct.id X.1

source

theorem CategoryTheory.Prod.hom_ext {C : Type u₁} [CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryStruct.{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₁} [CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryStruct.{v₂, u₂} D] {X Y : C × D} {f g : X ⟶ Y} :

f = g ↔ f.1 = g.1 ∧ f.2 = g.2

source

@[reducible, inline]

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

(X₁, Y₁) ⟶ (X₂, Y₂)

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

Instances For

source

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

Lean.TrailingParserDescr

Instances For

source

theorem CategoryTheory.Prod.mkHom_eq {C : Type u₁} [CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryStruct.{v₂, u₂} D] {X₁ X₂ : C} {Y₁ Y₂ : D} (f f' : X₁ ⟶ X₂) (g g' : Y₁ ⟶ Y₂) :

mkHom f g = mkHom f' g' ↔ f = f' ∧ g = g'

Analogue of Prod.mk.injEq in this setting.

source

@[simp]

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

CategoryStruct.id (X, Y) = Prod.mkHom (CategoryStruct.id X) (CategoryStruct.id Y)

source

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

CategoryStruct.id (X, Y) = (CategoryStruct.id X, CategoryStruct.id Y)

source

@[simp]

theorem CategoryTheory.prod_comp {C : Type u₁} [CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryStruct.{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 = Prod.mkHom (CategoryStruct.comp f.1 g.1) (CategoryStruct.comp f.2 g.2)

source

@[implicit_reducible]

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.

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.

Instances For

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 = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.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 = Prod.mkHom (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.

Instances For

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 = Prod.mkHom f.hom g.hom

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 = Prod.mkHom f.inv g.inv

source

@[implicit_reducible]

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.

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

Instances For

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

Instances For

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 = mkHom (CategoryStruct.id Z) f

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.

Instances For

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

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

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.

Instances For

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.

Instances For

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

@[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 = mkHom f.2 f.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.

Instances For

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.

Instances For

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

(braiding C D).functor = swap C D

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

(braiding C D).inverse = swap D C

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

Any morphism in a product factors as a morphism 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 (mkHom (CategoryStruct.id x.1) f.2) (CategoryStruct.comp (mkHom f.1 (CategoryStruct.id y.2)) h)

Any morphism in a product factors as a morphism whose left component is an identity followed by a morphism whose right component is an identity.

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

Any morphism in a product factors as a morphism 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 (mkHom f.1 (CategoryStruct.id x.2)) (CategoryStruct.comp (mkHom (CategoryStruct.id y.1) f.2) h)

Any morphism in a product factors as a morphism whose right component is an identity followed by a morphism whose left component is an identity.

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.

Instances For

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_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

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

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.

Instances For

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

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

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.

Instances For

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

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

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.

Instances For

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 = Prod.mkHom (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

Instances For

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 = Prod.mkHom (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

Instances For

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

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

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

Instances For

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

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

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

Functor C (C × C)

The diagonal functor.

Instances For

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 = Prod.mkHom 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.

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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

((Functor.whiskeringLeft A B C).obj F).comp ((evaluation A C).obj a) ≅ (evaluation B C).obj (F.obj a)

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

Instances For

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.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.whiskeringLeft_comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (a : A) :

((Functor.whiskeringLeft A B C).obj F).comp ((evaluation A C).obj a) = (evaluation B C).obj (F.obj a)

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

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

((Functor.whiskeringRight A B C).obj F).comp ((evaluation A C).obj a) ≅ ((evaluation A B).obj a).comp F

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

Instances For

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.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.whiskeringRight_comp_evaluation {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor B C) (a : A) :

((Functor.whiskeringRight A B C).obj F).comp ((evaluation A C).obj a) = ((evaluation A B).obj a).comp F

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

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

Instances For

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

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

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

Instances For

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 α = Prod.mkHom (Functor.whiskerRight α (Prod.fst B C)) (Functor.whiskerRight α (Prod.snd B C))

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

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

Instances For

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 = Prod.mkHom (X.1.prod'CompFst X.2).hom (X.1.prod'CompSnd X.2).hom

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 = Prod.mkHom (X.1.prod'CompFst X.2).inv (X.1.prod'CompSnd X.2).inv

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

Instances For

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✝ = Prod.mkHom (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✝ = Prod.mkHom (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)

Instances For

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_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

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

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.

Instances For

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 = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.2)

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 = Prod.mkHom f.unop.1.op f.unop.2.op

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)

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 = Prod.mkHom (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_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 (Prod.mkHom x✝.1.unop x✝.2.unop)

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_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

Documentation

Mathlib.CategoryTheory.Products.Basic

Cartesian products of categories #