Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk

{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} →
              {D₁ D₂ : F.DescentDataAsCoalgebra f} →
                (e : (i : ι) → D₁.obj i ≅ D₂.obj i) →
                  autoParam
                      (∀ (i₁ i₂ : ι),
                        CategoryTheory.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)) =
                          CategoryTheory.CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂))
                      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk._auto_1 →
                    (D₁ ≅ D₂)

Constructor for isomorphisms in DescentDataAsCoalgebra.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category