Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj

∀ {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) (M : ↑(F.obj { as := Opposite.op S }).obj) (i : ι),
  ((F.toDescentDataAsCoalgebra f).obj M).obj i = (F.map (f i).op.toLoc).l.toFunctor.obj M

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category