Theorems · Inductive type · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
        (CategoryTheory.Bicategory.Adj CategoryTheory.Cat) →
      {ι : Type t} → {S : C} → {X : ι → C} → ((i : ι) → X i ⟶ S) → Type (max (max t u') v')

Given a pseudofunctor F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat and a family of morphisms f i : X i ⟶ S in C, this is the category of descent data for F relative to the morphisms f i where the objects are defined as coalgebras: the morphisms relating the various objects obj i over X i are of the form obj i₁ ⟶ (f i₁)^* (f i₂)_* (obj i₂). This category can be compared to the corresponding category DescentData when suitable pullbacks exist and certain base change morphisms are isomorphisms (TODO).

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

39 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category