Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      (ι : Type u_2) →
        [inst_1 : Unique ι] →
          {X S : C} →
            (f : X ⟶ S) →
              (F.toDescentDataAsCoalgebra fun x => f).comp
                  (CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor ≅
                CategoryTheory.Comonad.comparison (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj)

When ι contains a unique element and f : X ⟶ S is a morphism, the composition of F.toDescentDataAsCoalgebra (fun (_ : ι) ↦ f) and the functor of the equivalence DescentDataAsCoalgebra.coalgebraEquivalence F ι f identifies to Comonad.comparison applied to the adjunction corresponding to F.map f.op.toLoc.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique