Descent data as coalgebras

Let F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat be a pseudofunctor to the bicategory of adjunctions in Cat. In particular, for any morphism g : X ⟶ Y in C, we have an adjunction (g^*, g_*) between a pullback functor and a pushforward functor.

In this file, given a family of morphisms f i : X i ⟶ S indexed by a type ι in C, we introduce a category F.DescentDataAsCoalgebra f of descent data relative to the morphisms f i, where the objects are described as a family of objects obj i over X i, and the morphisms relating them are described as morphisms obj i₁ ⟶ (f i₁)^* (f i₂)_* (obj i₂), similarly as Eilenberg-Moore coalgebras. Indeed, when the index type ι contains a unique element, we show that F.DescentDataAsCoalgebra (fun (i : ι) ↦ f identifies to the category of coalgebras for the comonad attached to the adjunction (F.map f.op.toLoc).adj.

TODO (@joelriou, @chrisflav)

• Compare DescentDataAsCoalgebra with DescentData when suitable pullbacks exist and certain base change morphisms are isomorphims

structure CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) {ι : Type t} {S : C} {X : ι → C} (f : (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).

• obj (i : ι) : ↑(F.obj { as := Opposite.op (X i) }).obj

  The objects over X i for all i

• hom (i₁ i₂ : ι) : self.obj i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (self.obj i₂))

  The compatibility morphisms.

• counit (i : ι) : CategoryStruct.comp (self.hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (self.obj i)) = CategoryStruct.id (self.obj i)
• coassoc (i₁ i₂ i₃ : ι) : CategoryStruct.comp (self.hom i₁ i₂) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂ i₃))) = CategoryStruct.comp (self.hom i₁ i₃) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (self.obj i₃))))

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i : ι) {Z : ↑(F.obj { as := Opposite.op (X i) }).obj} (h : (CategoryStruct.id (F.obj { as := Opposite.op (X i) }).obj).toFunctor.obj (self.obj i) ⟶ Z) : CategoryStruct.comp (self.hom i i) (CategoryStruct.comp ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (self.obj i)) h) = h

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (X i₁) }).obj} (h : (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj ((F.map (f i₂).op.toLoc).l.toFunctor.obj ((F.map (f i₃).op.toLoc).r.toFunctor.obj (self.obj i₃)))) ⟶ Z) : CategoryStruct.comp (self.hom i₁ i₂) (CategoryStruct.comp ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂ i₃))) h) = CategoryStruct.comp (self.hom i₁ i₃) (CategoryStruct.comp ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (self.obj i₃)))) h)

structure CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D₁ D₂ : F.DescentDataAsCoalgebra f) : Type (max t v')

The type of morphisms in DescentDataAsCoalgebra.

• hom (i : ι) : D₁.obj i ⟶ D₂.obj i

  The morphisms between the obj fields of descent data.

• comm (i₁ i₂ : ι) : CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂))) = CategoryStruct.comp (self.hom i₁) (D₂.hom i₁ i₂)

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {x y : D₁.Hom D₂} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {x y : D₁.Hom D₂} (hom : x.hom = y.hom) : x = y

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} (self : D₁.Hom D₂) (i₁ i₂ : ι) {Z : ↑(F.obj { as := Opposite.op (X i₁) }).obj} (h : (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (D₂.obj i₂)) ⟶ Z) : CategoryStruct.comp (D₁.hom i₁ i₂) (CategoryStruct.comp ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂))) h) = CategoryStruct.comp (self.hom i₁) (CategoryStruct.comp (D₂.hom i₁ i₂) h)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom_ext {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {φ φ' : D₁ ⟶ D₂} (h : ∀ (i : ι), φ.hom i = φ'.hom i) : φ = φ'

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom_ext_iff {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {φ φ' : D₁ ⟶ D₂} : φ = φ' ↔ ∀ (i : ι), φ.hom i = φ'.hom i

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.id_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentDataAsCoalgebra f) (i : ι) : (CategoryStruct.id D).hom i = CategoryStruct.id (D.obj i)

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentDataAsCoalgebra f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι) : (CategoryStruct.comp φ φ').hom i = CategoryStruct.comp (φ.hom i) (φ'.hom i)

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentDataAsCoalgebra f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι) {Z : ↑(F.obj { as := Opposite.op (X i) }).obj} (h : D₃.obj i ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp φ φ').hom i) h = CategoryStruct.comp (φ.hom i) (CategoryStruct.comp (φ'.hom i) h)

def CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) = CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂) := by cat_disch) : D₁ ≅ D₂

Constructor for isomorphisms in DescentDataAsCoalgebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_hom_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) = CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂) := by cat_disch) (i : ι) : (isoMk e comm).hom.hom i = (e i).hom

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_inv_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) = CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂) := by cat_disch) (i : ι) : (isoMk e comm).inv.hom i = (e i).inv

def CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) : (F.DescentDataAsCoalgebra fun (x : ι) => f) ≌ (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra

When the index type ι contains a unique element, the category DescentDataAsCoalgebra identifies to the category of coalgebras over the comonoad corresponding to the adjunction (F.map f.op.toLoc).adj.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) : ((coalgebraEquivalence F ι f).counitIso.hom.app X✝).f = CategoryStruct.id X✝.A

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) {X✝ Y✝ : F.DescentDataAsCoalgebra fun (x : ι) => f} (φ : X✝ ⟶ Y✝) : ((coalgebraEquivalence F ι f).functor.map φ).f = φ.hom default

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) {X✝ Y✝ : (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra} (φ : X✝ ⟶ Y✝) (i : ι) : ((coalgebraEquivalence F ι f).inverse.map φ).hom i = φ.f

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (A : (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x✝ : ι) : ((coalgebraEquivalence F ι f).inverse.obj A).obj x✝ = A.A

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (D : F.DescentDataAsCoalgebra fun (x : ι) => f) : ((coalgebraEquivalence F ι f).functor.obj D).A = D.obj default

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (A : (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x✝ x✝¹ : ι) : ((coalgebraEquivalence F ι f).inverse.obj A).hom x✝ x✝¹ = A.a

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (D : F.DescentDataAsCoalgebra fun (x : ι) => f) : ((coalgebraEquivalence F ι f).functor.obj D).a = D.hom default default

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : (Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) : ((coalgebraEquivalence F ι f).counitIso.inv.app X✝).f = CategoryStruct.id X✝.A

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : F.DescentDataAsCoalgebra fun (x : ι) => f) (i : ι) : ((coalgebraEquivalence F ι f).unitIso.inv.app X✝).hom i = eqToHom ⋯

theorem CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : F.DescentDataAsCoalgebra fun (x : ι) => f) (i : ι) : ((coalgebraEquivalence F ι f).unitIso.hom.app X✝).hom i = eqToHom ⋯

def CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M : ↑(F.obj { as := Opposite.op S }).obj) (i₁ i₂ : ι) : ((F.toDescentDataAsCoalgebra f).obj M).hom i₁ i₂ = (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M)

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj 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

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_map_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {X✝ Y✝ : ↑(F.obj { as := Opposite.op S }).obj} (g : X✝ ⟶ Y✝) (i : ι) : ((F.toDescentDataAsCoalgebra f).map g).hom i = (F.map (f i).op.toLoc).l.toFunctor.map g

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

When ι contains a unique element and f : X ⟶ S is a morphim, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} (ι : Type u_2) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : ↑(F.obj { as := Opposite.op S }).obj) : ((toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).inv.app X✝).f = CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X✝)

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} (ι : Type u_2) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : ↑(F.obj { as := Opposite.op S }).obj) : ((toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).hom.app X✝).f = CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X✝)

theorem CategoryTheory.Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) (Bicategory.Adj Cat)} (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) : (F.toDescentDataAsCoalgebra fun (x : ι) => f).IsEquivalence ↔ (Comonad.comparison (Adjunction.ofCat (F.map f.op.toLoc).adj)).IsEquivalence