Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i₁ i₂ i₃ : ι)
  {Z : ↑(F.obj { as := Opposite.op (X i₁) }).obj}
  (h :
    (F.map (f i₁).op.toLoc).l.toFunctor.obj
        ((F.map (f i₂).op.toLoc).r.toFunctor.obj
          ((F.map (f i₂).op.toLoc).l.toFunctor.obj ((F.map (f i₃).op.toLoc).r.toFunctor.obj (self.obj i₃)))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (self.hom i₁ i₂)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂ i₃))) h) =
    CategoryTheory.CategoryStruct.comp (self.hom i₁ i₃)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (f i₁).op.toLoc).l.toFunctor.map
          ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (self.obj i₃))))
        h)

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category