Documentation

Mathlib.CategoryTheory.Products.Associator

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

@[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.fst.fst, f.fst.snd, f.snd)
@[simp]

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

Instances For
    @[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.fst, f.snd.fst), f.snd.snd)

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

    Instances For

      The equivalence of categories expressing associativity of products of categories.

      Instances For