category_theory.products.basic

@[simp]

theorem category_theory.prod_id_fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(𝟙 X).fst = 𝟙 X.fst

source

@[simp]

theorem category_theory.prod_id_snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(𝟙 X).snd = 𝟙 X.snd

source

@[simp]

theorem category_theory.prod_comp_fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 _x_2 : C × D) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2) :

(f ≫ g).fst = f.fst ≫ g.fst

source

@[simp]

theorem category_theory.prod_hom (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C × D) :

(X ⟶ Y) = ((X.fst ⟶ Y.fst) × (X.snd ⟶ Y.snd))

source

@[protected, instance]

def category_theory.prod (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

category_theory.category (C × D)

prod C D gives the cartesian product of two categories.

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

Equations

category_theory.prod C D = {to_category_struct := {to_quiver := {hom := λ (X Y : C × D), (X.fst ⟶ Y.fst) × (X.snd ⟶ Y.snd)}, id := λ (X : C × D), (𝟙 X.fst, 𝟙 X.snd), comp := λ (_x _x_1 _x_2 : C × D) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), (f.fst ≫ g.fst, f.snd ≫ g.snd)}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.prod_comp_snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 _x_2 : C × D) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2) :

(f ≫ g).snd = f.snd ≫ g.snd

source

@[simp]

theorem category_theory.prod_id (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (Y : D) :

𝟙 (X, Y) = (𝟙 X, 𝟙 Y)

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

source

@[simp]

theorem category_theory.prod_comp (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) :

f ≫ g = (f.fst ≫ g.fst, f.snd ≫ g.snd)

source

theorem category_theory.is_iso_prod_iff (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :

category_theory.is_iso f ↔ category_theory.is_iso f.fst ∧ category_theory.is_iso f.snd

source

def category_theory.iso.prod {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category 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 category_theory.iso.prod_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) :

(f.prod g).hom = (f.hom, g.hom)

source

@[simp]

theorem category_theory.iso.prod_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) :

(f.prod g).inv = (f.inv, g.inv)

source

@[protected, instance]

def category_theory.uniform_prod (C : Type u₁) [category_theory.category C] (D : Type u₁) [category_theory.category D] :

category_theory.category (C × D)

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

Equations

category_theory.uniform_prod C D = category_theory.prod C D

source

@[simp]

theorem category_theory.prod.sectl_map (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] (Z : D) (X Y : C) (f : X ⟶ Y) :

(category_theory.prod.sectl C Z).map f = (f, 𝟙 Z)

source

def category_theory.prod.sectl (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] (Z : D) :

C ⥤ C × D

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

Equations

category_theory.prod.sectl C Z = {obj := λ (X : C), (X, Z), map := λ (X Y : C) (f : X ⟶ Y), (f, 𝟙 Z), map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.prod.sectl_obj (C : Type u₁) [category_theory.category C] {D : Type u₂} [category_theory.category D] (Z : D) (X : C) :

(category_theory.prod.sectl C Z).obj X = (X, Z)

source

@[simp]

theorem category_theory.prod.sectr_map {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] (X Y : D) (f : X ⟶ Y) :

(category_theory.prod.sectr Z D).map f = (𝟙 Z, f)

source

def category_theory.prod.sectr {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] :

D ⥤ C × D

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

Equations

category_theory.prod.sectr Z D = {obj := λ (X : D), (Z, X), map := λ (X Y : D) (f : X ⟶ Y), (𝟙 Z, f), map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.prod.sectr_obj {C : Type u₁} [category_theory.category C] (Z : C) (D : Type u₂) [category_theory.category D] (X : D) :

(category_theory.prod.sectr Z D).obj X = (Z, X)

source

def category_theory.prod.fst (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C × D ⥤ C

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

Equations

category_theory.prod.fst C D = {obj := λ (X : C × D), X.fst, map := λ (X Y : C × D) (f : X ⟶ Y), f.fst, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.prod.fst_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C × D) (f : X ⟶ Y) :

(category_theory.prod.fst C D).map f = f.fst

source

@[simp]

theorem category_theory.prod.fst_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.fst C D).obj X = X.fst

source

@[simp]

theorem category_theory.prod.snd_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C × D) (f : X ⟶ Y) :

(category_theory.prod.snd C D).map f = f.snd

source

@[simp]

theorem category_theory.prod.snd_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.snd C D).obj X = X.snd

source

def category_theory.prod.snd (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C × D ⥤ D

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

Equations

category_theory.prod.snd C D = {obj := λ (X : C × D), X.snd, map := λ (X Y : C × D) (f : X ⟶ Y), f.snd, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.prod.swap_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.swap C D).obj X = (X.snd, X.fst)

source

@[simp]

theorem category_theory.prod.swap_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : C × D) (f : _x ⟶ _x_1) :

(category_theory.prod.swap C D).map f = (f.snd, f.fst)

source

def category_theory.prod.swap (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C × D ⥤ D × C

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

Equations

category_theory.prod.swap C D = {obj := λ (X : C × D), (X.snd, X.fst), map := λ (_x _x_1 : C × D) (f : _x ⟶ _x_1), (f.snd, f.fst), map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.prod.symmetry_hom_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.symmetry C D).hom.app X = 𝟙 X

source

def category_theory.prod.symmetry (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

category_theory.prod.swap C D ⋙ category_theory.prod.swap D C ≅ 𝟭 (C × D)

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

Equations

category_theory.prod.symmetry C D = {hom := {app := λ (X : C × D), 𝟙 X, naturality' := _}, inv := {app := λ (X : C × D), 𝟙 X, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.prod.symmetry_inv_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.symmetry C D).inv.app X = 𝟙 X

source

@[simp]

theorem category_theory.prod.braiding_unit_iso_inv_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.braiding C D).unit_iso.inv.app X = (𝟙 X.fst, 𝟙 X.snd) ≫ category_theory.eq_to_hom _ ≫ (𝟙 X.fst, 𝟙 X.snd) ≫ (𝟙 X.fst, 𝟙 X.snd) ≫ (𝟙 X.fst, 𝟙 X.snd) ≫ (𝟙 X.fst, 𝟙 X.snd) ≫ category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.prod.braiding_functor_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : C × D) (f : _x ⟶ _x_1) :

(category_theory.prod.braiding C D).functor.map f = (f.snd, f.fst)

source

@[simp]

theorem category_theory.prod.braiding_inverse_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (_x _x_1 : D × C) (f : _x ⟶ _x_1) :

(category_theory.prod.braiding C D).inverse.map f = (f.snd, f.fst)

source

@[simp]

theorem category_theory.prod.braiding_counit_iso_hom_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : D × C) :

(category_theory.prod.braiding C D).counit_iso.hom.app X = category_theory.eq_to_hom _

source

def category_theory.prod.braiding (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C × D ≌ D × C

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

Equations

category_theory.prod.braiding C D = category_theory.equivalence.mk (category_theory.prod.swap C D) (category_theory.prod.swap D C) (category_theory.nat_iso.of_components (λ (X : C × D), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : D × C), category_theory.eq_to_iso _) _)

source

@[simp]

theorem category_theory.prod.braiding_inverse_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : D × C) :

(category_theory.prod.braiding C D).inverse.obj X = (X.snd, X.fst)

source

@[simp]

theorem category_theory.prod.braiding_functor_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.braiding C D).functor.obj X = (X.snd, X.fst)

source

@[simp]

theorem category_theory.prod.braiding_unit_iso_hom_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C × D) :

(category_theory.prod.braiding C D).unit_iso.hom.app X = category_theory.eq_to_hom _ ≫ ((category_theory.iso.refl ((X.snd, X.fst).fst, (X.snd, X.fst).snd)).inv.snd ≫ (category_theory.eq_to_hom _).fst ≫ 𝟙 X.fst, (category_theory.iso.refl ((X.snd, X.fst).fst, (X.snd, X.fst).snd)).inv.fst ≫ (category_theory.eq_to_hom _).snd ≫ 𝟙 X.snd)

source

@[simp]

theorem category_theory.prod.braiding_counit_iso_inv_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : D × C) :

(category_theory.prod.braiding C D).counit_iso.inv.app X = category_theory.eq_to_hom _

source

@[protected, instance]

def category_theory.prod.swap_is_equivalence (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

category_theory.is_equivalence (category_theory.prod.swap C D)

Equations

category_theory.prod.swap_is_equivalence C D = category_theory.is_equivalence.of_equivalence (category_theory.prod.braiding C D)

source

@[simp]

theorem category_theory.evaluation_map_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X Y : C) (f : X ⟶ Y) (F : C ⥤ D) :

((category_theory.evaluation C D).map f).app F = F.map f

source

def category_theory.evaluation (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C ⥤ (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

category_theory.evaluation C D = {obj := λ (X : C), {obj := λ (F : C ⥤ D), F.obj X, map := λ (F G : C ⥤ D) (α : F ⟶ G), α.app X, map_id' := _, map_comp' := _}, map := λ (X Y : C) (f : X ⟶ Y), {app := λ (F : C ⥤ D), F.map f, naturality' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.evaluation_obj_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (F : C ⥤ D) :

((category_theory.evaluation C D).obj X).obj F = F.obj X

source

@[simp]

theorem category_theory.evaluation_obj_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (X : C) (F G : C ⥤ D) (α : F ⟶ G) :

((category_theory.evaluation C D).obj X).map α = α.app X

source

@[simp]

theorem category_theory.evaluation_uncurried_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (x y : C × (C ⥤ D)) (f : x ⟶ y) :

(category_theory.evaluation_uncurried C D).map f = x.snd.map f.fst ≫ f.snd.app y.fst

source

def category_theory.evaluation_uncurried (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

C × (C ⥤ D) ⥤ D

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

Equations

category_theory.evaluation_uncurried C D = {obj := λ (p : C × (C ⥤ D)), p.snd.obj p.fst, map := λ (x y : C × (C ⥤ D)) (f : x ⟶ y), x.snd.map f.fst ≫ f.snd.app y.fst, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.evaluation_uncurried_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (p : C × (C ⥤ D)) :

(category_theory.evaluation_uncurried C D).obj p = p.snd.obj p.fst

source

@[simp]

theorem category_theory.functor.prod_map {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] (F : A ⥤ B) (G : C ⥤ D) (_x _x_1 : A × C) (f : _x ⟶ _x_1) :

(F.prod G).map f = (F.map f.fst, G.map f.snd)

source

@[simp]

theorem category_theory.functor.prod_obj {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] (F : A ⥤ B) (G : C ⥤ D) (X : A × C) :

(F.prod G).obj X = (F.obj X.fst, G.obj X.snd)

source

def category_theory.functor.prod {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] (F : A ⥤ B) (G : C ⥤ D) :

A × C ⥤ B × D

The cartesian product of two functors.

Equations

F.prod G = {obj := λ (X : A × C), (F.obj X.fst, G.obj X.snd), map := λ (_x _x_1 : A × C) (f : _x ⟶ _x_1), (F.map f.fst, G.map f.snd), map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.prod'_map {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B) (G : A ⥤ C) (x y : A) (f : x ⟶ y) :

(F.prod' G).map f = (F.map f, G.map f)

source

@[simp]

theorem category_theory.functor.prod'_obj {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B) (G : A ⥤ C) (a : A) :

(F.prod' G).obj a = (F.obj a, G.obj a)

source

def category_theory.functor.prod' {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B) (G : A ⥤ C) :

A ⥤ B × C

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

Equations

F.prod' G = {obj := λ (a : A), (F.obj a, G.obj a), map := λ (x y : A) (f : x ⟶ y), (F.map f, G.map f), map_id' := _, map_comp' := _}

source

def category_theory.functor.diag (C : Type u₃) [category_theory.category C] :

C ⥤ C × C

The diagonal functor.

Equations

category_theory.functor.diag C = (𝟭 C).prod' (𝟭 C)

source

@[simp]

theorem category_theory.functor.diag_obj (C : Type u₃) [category_theory.category C] (X : C) :

(category_theory.functor.diag C).obj X = (X, X)

source

@[simp]

theorem category_theory.functor.diag_map (C : Type u₃) [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

(category_theory.functor.diag C).map f = (f, f)

source

def category_theory.nat_trans.prod {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) :

F.prod H ⟶ G.prod I

The cartesian product of two natural transformations.

Equations

category_theory.nat_trans.prod α β = {app := λ (X : A × C), (α.app X.fst, β.app X.snd), naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.prod_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) (X : A × C) :

(category_theory.nat_trans.prod α β).app X = (α.app X.fst, β.app X.snd)

source

@[simp]

theorem category_theory.flip_comp_evaluation_hom_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B ⥤ C) (a : A) (X : B) :

(category_theory.flip_comp_evaluation F a).hom.app X = 𝟙 ((F.obj a).obj X)

source

@[simp]

theorem category_theory.flip_comp_evaluation_inv_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B ⥤ C) (a : A) (X : B) :

(category_theory.flip_comp_evaluation F a).inv.app X = 𝟙 ((F.obj a).obj X)

source

def category_theory.flip_comp_evaluation {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] (F : A ⥤ B ⥤ C) (a : A) :

F.flip ⋙ (category_theory.evaluation A C).obj a ≅ F.obj a

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

Equations

category_theory.flip_comp_evaluation F a = category_theory.nat_iso.of_components (λ (b : B), category_theory.eq_to_iso _) _

mathlib documentation

Cartesian products of categories #