associativity — Mathlib

English

There is an equivalence of categories between Sum (Sum C D) E and Sum C (Sum D E), exhibiting the associativity of the direct sum operation on categories. The equivalence is given by the associativity functor and its inverse, with explicit unit and counit described by standard sum-based isomorphisms.

Русский

Существует эквивалентность категорий между Sum (Sum C D) E и Sum C (Sum D E), демонстрирующая ассоциативность операции суммы категорий. Эквивалентность задаётся соответствующей функцией ассоциативности и её обратной стороной, а единица и counit описаны стандартными изоморфиями суммы.

LaTeX

$$$$ (C \oplus D) \oplus E \simeq C \oplus (D \oplus E). $$$$

Lean4

/-- The equivalence of categories expressing associativity of sums of categories.
-/
@[simps functor inverse]
def associativity : (C ⊕ D) ⊕ E ≌ C ⊕ (D ⊕ E)
    where
  functor := associator C D E
  inverse := inverseAssociator C D E
  unitIso :=
    Functor.sumIsoExt
      (Functor.sumIsoExt
        ((Functor.associator _ _ _).symm ≪≫
          Functor.rightUnitor _ ≪≫
            (isoWhiskerRight (inlCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                  inlCompInverseAssociator C D E).symm ≪≫
              Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Functor.associator _ _ _))
        ((Functor.associator _ _ _).symm ≪≫
          Functor.rightUnitor _ ≪≫
            (isoWhiskerRight (inrCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                  Functor.associator _ _ _ ≪≫ inlCompInrCompInverseAssociator C D E).symm ≪≫
              Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Functor.associator _ _ _)))
      (Functor.rightUnitor _ ≪≫
        (isoWhiskerRight (inrCompAssociator C D E) (inverseAssociator C D E) ≪≫
              Functor.associator _ _ _ ≪≫ inrCompInrCompInverseAssociator C D E).symm ≪≫
          Functor.associator _ _ _)
  counitIso :=
    Functor.sumIsoExt
      ((Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (inlCompInverseAssociator C D E) (associator C D E) ≪≫
          Functor.associator _ _ _ ≪≫ inlCompInlCompAssociator C D E ≪≫ (Functor.rightUnitor _).symm)
      (Functor.sumIsoExt
        ((Functor.associator _ _ _).symm ≪≫
          (Functor.associator _ _ _).symm ≪≫
            isoWhiskerRight (Functor.associator _ _ _ ≪≫ inlCompInrCompInverseAssociator C D E) (associator C D E) ≪≫
              Functor.associator _ _ _ ≪≫
                inrCompInlCompAssociator C D E ≪≫ (Functor.rightUnitor _).symm ≪≫ Functor.associator _ _ _)
        ((Functor.associator _ _ _).symm ≪≫
          (Functor.associator _ _ _).symm ≪≫
            isoWhiskerRight (Functor.associator _ _ _ ≪≫ inrCompInrCompInverseAssociator C D E) (associator C D E) ≪≫
              inrCompAssociator C D E ≪≫ isoWhiskerLeft _ (Functor.rightUnitor _).symm))
  functor_unitIso_comp
    x :=
    match x with
    | inl (inl c) => by simp [inlCompInlCompAssociator, inlCompInverseAssociator]
    | inl (inr d) => by simp [inrCompInlCompAssociator, inlCompInrCompInverseAssociator]
    | inr e => by simp [inrCompAssociator, inrCompInrCompInverseAssociator]

Похожие утверждения