Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra

{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) →
              CategoryTheory.Functor (↑(F.obj { as := Opposite.op S }).obj) (F.DescentDataAsCoalgebra f)

The functor (F.obj (.mk (op S))).obj ⥤ F.DescentDataAsCoalgebra f when f i : X i ⟶ S is a family of morphisms.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category