Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.noConfusion

{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} →
              {P : Sort u_1} →
                {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' : (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 := obj, hom := hom, counit := counit, coassoc := coassoc } =
                                    { obj := obj', hom := hom', counit := counit', coassoc := coassoc' } →
                                  (obj ≍ obj' → hom ≍ hom' → P) → P

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

1 results in Mathlib

Foundations

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