Documentation

Mathlib.CategoryTheory.Products.Associator

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

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

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

    Instances For
      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.

      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.IsEquivalence (CategoryTheory.prod.associator C D E)
        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.IsEquivalence (CategoryTheory.prod.inverseAssociator C D E)