Documentation

Mathlib.CategoryTheory.Products.Associator

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

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

Equations
Instances For
    @[simp]
    theorem CategoryTheory.prod.associator_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : (C × D) × E) :
    (associator C D E).obj X = (X.1.1, X.1.2, X.2)
    @[simp]
    theorem CategoryTheory.prod.associator_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (x✝ x✝¹ : (C × D) × E) (f : x✝ x✝¹) :
    (associator C D E).map f = (f.1.1, f.1.2, f.2)

    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
      @[simp]
      theorem CategoryTheory.prod.inverseAssociator_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C × D × E) :
      (inverseAssociator C D E).obj X = ((X.1, X.2.1), X.2.2)
      @[simp]
      theorem CategoryTheory.prod.inverseAssociator_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (x✝ x✝¹ : C × D × E) (f : x✝ x✝¹) :
      (inverseAssociator C D E).map f = ((f.1, f.2.1), f.2.2)

      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