Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.inj

∀ {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

1 results in Mathlib

Foundations

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