Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentData.obj

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} → {f : (i : ι) → X i ⟶ S} → F.DescentData f → (i : ι) → ↑(F.obj { as := Opposite.op (X i) })

The objects over X i for all i

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

44 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category