[Merged by Bors] - feat(CategoryTheory/Sites): descent data, given as coalgebras

[joelriou]

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 PR, 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.

Co-authored-by: Christian Merten

---

[github-actions]

PR summary 8dbc02da01

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Bicategory.Adjunction.Cat	428	434	+6 (+1.40%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Bicategory.Adjunction.Cat	6
Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (new file)	448

---

Declarations diff

+ DescentDataAsCoalgebra
+ Hom
+ coalgebraEquivalence
+ comp_hom
+ counit_naturality
+ hom_ext
+ id_hom
+ instance : Category (F.DescentDataAsCoalgebra f)
+ isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison
+ isoMk
+ left_triangle_components
+ right_triangle_components
+ toDescentDataAsCoalgebra
+ toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso
+ unit_naturality

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[robin-carlier]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build