Mathlib.CategoryTheory.Products.Associator

The associator functor ((C × D) × E) ⥤ (C × (D × E)) and its inverse form an equivalence.

@[simp]

theorem CategoryTheory.prod.associator_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (X : (C × D) × E) :

(CategoryTheory.prod.associator C D E).obj X = (X.1.1, X.1.2, X.2)

source

@[simp]

theorem CategoryTheory.prod.associator_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

∀ (x x_1 : (C × D) × E) (f : x ⟶ x_1), (CategoryTheory.prod.associator C D E).map f = (f.1.1, f.1.2, f.2)

source

def CategoryTheory.prod.associator (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

CategoryTheory.Functor ((C × D) × E) (C × D × E)

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

Equations

CategoryTheory.prod.associator C D E = { obj := fun (X : (C × D) × E) => (X.1.1, X.1.2, X.2), map := fun (x x_1 : (C × D) × E) (f : x ⟶ x_1) => (f.1.1, f.1.2, f.2), map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.prod.inverseAssociator_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (X : C × D × E) :

(CategoryTheory.prod.inverseAssociator C D E).obj X = ((X.1, X.2.1), X.2.2)

source

@[simp]

theorem CategoryTheory.prod.inverseAssociator_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

∀ (x x_1 : C × D × E) (f : x ⟶ x_1), (CategoryTheory.prod.inverseAssociator C D E).map f = ((f.1, f.2.1), f.2.2)

source

def CategoryTheory.prod.inverseAssociator (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

CategoryTheory.Functor (C × D × E) ((C × D) × E)

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

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.prod.associativity_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.associativity C D E).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.prod.inverseAssociator C D E).comp (CategoryTheory.prod.associator C D E))

source

@[simp]

theorem CategoryTheory.prod.associativity_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.associativity C D E).inverse = CategoryTheory.prod.inverseAssociator C D E

source

@[simp]

theorem CategoryTheory.prod.associativity_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.associativity C D E).functor = CategoryTheory.prod.associator C D E

source

@[simp]

theorem CategoryTheory.prod.associativity_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.associativity C D E).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id ((C × D) × E))

source

def CategoryTheory.prod.associativity (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

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

The equivalence of categories expressing associativity of products of categories.

Equations

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

Instances For

source

instance CategoryTheory.prod.associatorIsEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.associator C D E).IsEquivalence

Equations

⋯ = ⋯

source

instance CategoryTheory.prod.inverseAssociatorIsEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :

(CategoryTheory.prod.inverseAssociator C D E).IsEquivalence

Equations

⋯ = ⋯