…uiv/Basic): move definitions and add symmetric version (#20416)

Move the two definitions `MonoidHom.precompEquiv` (the equivalence `(β →* γ) ≃ (α →* γ)` obtained by precomposition with a multiplicative equivalence `e : α ≃* β`)  and `AddMonoidHom.precompEquiv` (its additive version) from `Algebra.Category.MonCat.ForgetCorepresentable` to `Algebra.Group.Equiv.Basic`, so they can be used without importing files about `MonCat`. Also merge them into one definition using `@[to_additive]` and add the symmetric definition `(Add)MonoidHom.postcompEquiv`.

* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...

* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...

…ory of commutative additive groups (#20522)

If `F : J ⥤ AddCommGrp.{w}` is a functor, we show that `F` admits a colimit if and only
if `Colimits.Quot F` (the quotient of the direct sum of the commutative groups `F.obj j`
by the relations given by the morphisms in the diagram) is `w`-small.

- [x] depends on: #20416
- [x] depends on: #20512



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

…mmutative additive groups preserves colimits (#20417)

Prove that the functor `AddCommGrp.ulift` preserves all colimits, hence creates small colimits. (This also finished the proof that it is an exact functor.)

Method: Suppose that we have a functor `K : J ⥤ AddCommGrp.{u}` (with `J` any category), a
colimit cocone `c` of `K` and a cocone `lc` of `K ⋙ uliftFunctor.{u v}`. We want to
construct a morphism of cocones `uliftFunctor.mapCocone c → lc` witnessing the fact
that `uliftFunctor.mapCocone c` is also a colimit cocone, but we have no direct way
to do this. The idea is to use that `AddCommGrp.{max v u}` has a small cogenerator,
which is just the additive (rational) circle `ℚ / ℤ`, so any abelian group of
any size can be recovered from its morphisms into `ℚ / ℤ`. More precisely, the functor
sending an abelian group `A` to its dual `A →+ ℚ / ℤ` is fully faithful, *if* we consider
the dual as a (right) module over the endomorphism ring of `ℚ / ℤ`. So an abelian
group `C` is totally determined by the restriction of the coyoneda
functor `A ↦ (C →+ A)` to the category of abelian groups at a smaller universe level.
We do not develop this totally here but do a direct construction. Every time we have
a morphism from `lc.pt` into `ℚ / ℤ`, or more generally into any small abelian group
`A`, we can construct a cocone of `K ⋙ uliftFunctor` by sticking `ULift A` at the
cocone point (this is `CategoryTheory.Limits.Cocone.extensions`), and this cocone is
actually made up of `u`-small abelian groups, hence gives a cocone of `K`. Using
the universal property of `c`, we get a morphism `c.pt →+ A`. So we have constructed
a map `(lc.pt →+ A) → (c.pt →+ A)`, and it is easy to prove that it is compatible with
postcomposition of morphisms of small abelian groups. To actually get the
morphism `c.pt →+ lc.pt`, we apply this to the canonical embedding of `lc.pt` into
`Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` (this group is not small but is a product of small
groups, so our construction extends). To show that the image of `c.pt` in this product
is contained in that of `lc.pt`, we use the compatibility with postcomposition and the
fact that we can detect elements of the image just by applying morphisms from
`Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` to `ℚ / ℤ`.

- [x] depends on: #20416
- [x] depends on: #20512
- [x] depends on: #20522