feat(Algebra/Category): finitely presented algebras are finitely presented

[erdOne]

Co-authored-by: Christian Merten

---

[github-actions]

PR summary 83b6b79818

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Limits.Preserves.Over (new file)	545
Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (new file)	577
Mathlib.Algebra.Category.Ring.FinitePresentation (new file)	1326

---

Declarations diff

+ EssFiniteType
+ EssFiniteType.ext
+ EssFiniteType.finset
+ FiniteType.essFiniteType
+ exists_comp_map_eq_of_isColimit
+ exists_eq_comp_ι_app_of_isColimit
+ instance : FinCategory (WalkingMulticospan fst snd)
+ instance : FinCategory (WalkingMultispan fst snd)
+ instance {X : C} : PreservesCofilteredLimitsOfSize (Over.forget X) := by
+ instance {X : C} : PreservesFilteredColimitsOfSize (Under.forget X) := by
+ preservesColimit_coyoneda_of_finitePresentation
+ preservesFilteredColimits_coyoneda

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

[joelriou]

It could be nice to add an IsFinitelyPresentable abbreviation at https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Presentable/Basic.html#CategoryTheory.IsCardinalPresentable (by saying it satisfies IsCardinalPresentable X Cardinal.aleph0.{w}) and show it is equivalent to the preservation of filtered colimits by using https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.html#CategoryTheory.isCardinalFiltered_aleph0_iff