feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites

[joelriou]

---

• depends on: feat(Algebra/Category/ModuleCat): pullback of presheaves of modules #17366

[github-actions]

PR summary 853a093a69

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Adjunction.PartialAdjoint	405
Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono	1188
Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	1224
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator	1274
Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback	1278

---

Declarations diff

+ Elements
+ FreeYoneda
+ LeftAdjointObjIsDefined
+ PartialLeftAdjointSource
+ PullbackObjIsDefined
+ adj_homEquiv
+ corepresentableByCompCoyonedaObjOfIsColimit
+ elementsMk
+ epi_of_surjective
+ free
+ freeAdjunction
+ freeAdjunctionUnit
+ freeAdjunction_homEquiv
+ freeAdjunction_unit_app
+ freeDesc
+ freeDesc_apply
+ freeMk
+ freeObj
+ freeObjDesc
+ freeYoneda
+ freeYonedaCoproduct
+ freeYonedaCoproductMk
+ freeYonedaCoproductsCokernelCofork
+ freeYonedaEquiv
+ freeYonedaEquiv_comp
+ freeYonedaEquiv_symm_apply
+ free_map_apply
+ fromFreeYoneda
+ fromFreeYonedaCoproduct
+ fromFreeYonedaCoproduct_app_mk
+ fromFreeYoneda_app_apply
+ hasLimitsOfSize
+ instance (X : F.PartialLeftAdjointSource) :
+ instance : (pushforward.{u} φ).IsRightAdjoint
+ instance : (pushforward.{v} (F := F ⋙ G) (φ ≫ whiskerLeft F.op ψ)).IsRightAdjoint
+ instance : (pushforward.{v} (F := 𝟭 C) (𝟙 S)).IsRightAdjoint
+ instance : Epi M.fromFreeYonedaCoproduct
+ instance : Small.{u} (FreeYoneda R)
+ isColimitFreeYonedaCoproductsCokernelCofork
+ isDetecting
+ isRightAdjoint_of_leftAdjointObjIsDefined_eq_top
+ isSeparating
+ leftAdjointObjIsDefined_colimit
+ leftAdjointObjIsDefined_iff
+ leftAdjointObjIsDefined_of_isColimit
+ mk
+ mk_surjective
+ partialLeftAdjoint
+ partialLeftAdjointHomEquiv
+ partialLeftAdjointHomEquiv_comp
+ partialLeftAdjointHomEquiv_map
+ partialLeftAdjointHomEquiv_map_comp
+ partialLeftAdjointMap
+ partialLeftAdjointObj
+ pullback
+ pullbackComp
+ pullbackId
+ pullbackObjIsDefined_eq_top
+ pullbackObjIsDefined_free_yoneda
+ pullbackPushforwardAdjunction
+ pushforwardComp
+ pushforwardCompCoyonedaFreeYonedaCorepresentableBy
+ pushforwardId
+ pushforward_assoc
+ pushforward_comp_id
+ pushforward_id_comp
+ sheafificationAdjunction_homEquiv_apply
+ toFreeYonedaCoproduct
+ toFreeYonedaCoproduct_fromFreeYonedaCoproduct
+ wellPowered
+ ιFreeYonedaCoproduct
+ ι_fromFreeYonedaCoproduct
+ ι_fromFreeYonedaCoproduct_apply
++ freeHomEquiv
++ free_hom_ext
- sheaififcationAdjunction_homEquiv_apply

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 script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra/Category/ModuleCat): pullback of presheaves of modules #17366
  By Dependent Issues (🤖). Happy coding!