Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.injEq

∀ {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} (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj)
  (hom :
    (i₁ i₂ : ι) → obj i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj i₂)))
  (counit :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj i)) =
          CategoryTheory.CategoryStruct.id (obj i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam)
  (coassoc :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom i₁ i₃)
            ((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 (obj i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam)
  (obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj)
  (hom_1 :
    (i₁ i₂ : ι) →
      obj_1 i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj_1 i₂)))
  (counit_1 :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj_1 i)) =
          CategoryTheory.CategoryStruct.id (obj_1 i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam)
  (coassoc_1 :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom_1 i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₃)
            ((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 (obj_1 i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam),
  ({ obj := obj, hom := hom, counit := counit, coassoc := coassoc } =
      { obj := obj_1, hom := hom_1, counit := counit_1, coassoc := coassoc_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1)

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category