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_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).toPrefunctor.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).toPrefunctor.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
  • One or more equations did not get rendered due to their size.
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).toPrefunctor.map f = ((f.1, f.2.1), f.2.2)
    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).toPrefunctor.obj X = ((X.1, X.2.1), X.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
      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.IsEquivalence (CategoryTheory.prod.associator C D E)
        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.IsEquivalence (CategoryTheory.prod.inverseAssociator C D E)
        Equations