Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom

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

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique