feat(Algebra/ModuleCat): descent data

[dagurtomas]

Co-authored-by: Jack McKoen mckoen@ualberta.ca
Co-authored-by: Christian Merten christian@merten.dev
Co-authored-by: Joël Riou rioujoel@gmail.com
Co-authored-by: Adam Topaz atopaz@fastmail.com

---

• depends on: [Merged by Bors] - feat(RingTheory): faithfully flat ring maps #24530

[github-actions]

PR summary 75f43a0c35

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.RingHom.FaithfullyFlat (new file)	1985
Mathlib.Algebra.Category.ModuleCat.Descent (new file)	2082

---

Declarations diff

+ FaithfullyFlat
+ IsStableUnderBaseChange.and
+ ModuleCat.preservesFiniteLimits_extendScalars_of_flat
+ ModuleCat.preservesFiniteLimits_tensorLeft_of_flat
+ ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat
+ RespectsIso.and
+ RingHom.LocalizationAwayPreserves.and
+ RingHom.OfLocalizationSpan.and
+ RingHom.OfLocalizationSpanTarget.and
+ RingHom.PropertyIsLocal.and
+ RingHom.StableUnderCompositionWithLocalizationAwayTarget.and
+ RingHom.flat_algebraMap_iff
+ StableUnderComposition.and
+ comonadicExtendScalars
+ comp_ofBijective_symm
+ eq_and
+ faithfullyFlat_algebraMap_iff
+ flat
+ iff_flat_and_comap_surjective
+ instance (M : ModuleCat.{u} A) [Module.Flat A M] : PreservesFiniteLimits <| tensorLeft M := by
+ instance {R S : Type*} [Ring R] [Ring S] (f : R →+* S) :
+ isStableUnderBaseChange
+ lTensor_bijective_iff_bijective
+ ofBijective_symm_comp
+ of_bijective
+ preservesFiniteColimits_iff_forall_exact_map_and_epi
+ preservesFiniteLimits_iff_forall_exact_map_and_mono
+ respectsIso
+ stableUnderComposition
- flat_algebraMap_iff

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.

---

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).

[dagurtomas]

The diff in Monad.Adjunction makes no sense. The file is unchanged

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(RingTheory): faithfully flat ring maps #24530
  By Dependent Issues (🤖). Happy coding!

[chrisflav]

In consultation with Dagur, I migrated this PR to my fork in #32326.