category_theory.products.associator

source

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

(C × D) × E ⥤ C × D × E

The associator functor (C × D) × E ⥤ C × (D × E).

Equations

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

Instances for category_theory.prod.associator

category_theory.prod.associator_is_equivalence

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

C × D × E ⥤ (C × D) × E

The inverse associator functor C × (D × E) ⥤ (C × D) × E.

Equations

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

Instances for category_theory.prod.inverse_associator

category_theory.prod.inverse_associator_is_equivalence

source

@[simp]

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

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

source

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

(C × D) × E ≌ C × D × E

The equivalence of categories expressing associativity of products of categories.

Equations

category_theory.prod.associativity C D E = category_theory.equivalence.mk (category_theory.prod.associator C D E) (category_theory.prod.inverse_associator C D E) (category_theory.nat_iso.of_components (λ (X : (C × D) × E), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : C × D × E), category_theory.eq_to_iso _) _)

source

@[protected, instance]

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

category_theory.is_equivalence (category_theory.prod.associator C D E)

Equations

category_theory.prod.associator_is_equivalence C D E = category_theory.is_equivalence.of_equivalence (category_theory.prod.associativity C D E)

source

@[protected, instance]

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

category_theory.is_equivalence (category_theory.prod.inverse_associator C D E)

Equations

category_theory.prod.inverse_associator_is_equivalence C D E = category_theory.is_equivalence.of_equivalence_inverse (category_theory.prod.associativity C D E)