The category of finite topological spaces.

In this PR, we define the single functors from a preadditive category (with a zero object) to its homotopy category of cochain complexes and show they behave well with respect to shift functors.

…3613)

Refactor Module.AEval out of Algebra/Polynomial/Module/Basic.

Follow-up on #13419: fix three cases with an easy fix which were merged since then, and three harder cases.

Move 3 definitions that depend on `Num` to a new file.

…different rings (#13042)

Generalise `compl₂` and `compl₁₂` for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

…ty and surjectivity (#13621)

This PR proves that precomposition with a cocontinuous functor preserves local injectivity and surjectivity of morphisms of presheaves, and that precomposition with a cover preserving and cover dense functor reflects the same properties.

This copies the API for order lemmas on `Rat`

Also renames `Nat.floor_coe` to `floor_natCast`, leaving behind a deprecation.

…stance to a less obscure file (#13654)

There is little point in avoiding to import `CharZero` in `Algebra.Order.Ring.Defs` (where `StrictOrderedSemiring` is defined) since it is so basic. Exiling the titular basic instance to an obscure file meant that people had trouble finding that instance (and it just happened to Eric).

Seems like shake wants to move things around due to the `Std`/`Batteries` rename, so I'm running `lake exe shake --update` now to avoid polluting later PRs.

... rather than `a`, `b`, `m`, `n`, `r`. Also make arguments to rewriting lemmas explicit.

Without this change, the infoview gives
```
Error updating: Error fetching goals: Rpc error: InternalError: unknown free variable '_fvar.231'
```
when you hover over the variable name

Extend the style linter with two tiny features:
- lint on "isolated where": all occurrences were already fixed in #12991 and #13202.
- lint on "leading by": if one line starts with `by ` but the previous line ends with `:=`, according to the style guide the `by` should move to the previous line. For now, we only lint if the `by` fits on the previous line (fixed in #13618 and predecessors): there about other 28 cases in mathlib which don't have an obvious fix.

…use (#13784)

This is a few isolated lemmas split out of
#10853.

1. AnalyticAt.comp_of_eq
2. FormalMultilinearSeries.zero_radius
3. constFormalMultilinearSeries_zero

... as was discussed on zulip the other day; I cannot find the link quickly.
After this PR, a handful of uses remain which are harder to remove: [this branch](https://github.com/leanprover-community/mathlib4/compare/MR-mono-gcongr) comments them all

Inspired by #12661: let's start with some easy instances, so we can focus on the difficult ones.

In particular, this PR does not depend on any in-progress bugfixes, not tries to change a default value `by continuity` to `by fun_prop`.

I am not at all confident about the tagging of lemmas with fun_prop: I remember this being subtle, but can't find any documentation on this. @lecopivo Can you advise on these lemmas (or simply link to the right documentation if I just overlooked it)?

... and similar results for lipschitzness.

From LeanCamCombi

Unnecessary, and unhelpful.

…IsLocalization` (#13933)

If `x` is a point in the basic open set `D(f)` where `f` is a homogeneous element of positive
degree, then the homogeneously localized ring `A⁰ₓ` has the universal property of the localization
of `A⁰_f` at `φ(x)` where `φ : Proj|D(f) ⟶ Spec A⁰_f` is the morphism of locally ringed space
constructed as above.


Co-authored-by: Andrew Yang <the.erd.one@gmail.com>




Co-authored-by: zjj <j.jj@j.jj>

This is the first part of the refactor of `CompHaus` and friends (adding the new API which will eventually be used to redefine  the categories of compact Hausdorff spaces, see #12930)

…ile. (#13942)

…ive functors (#13948)

These are not actionable anymore (if they ever were).

Fixes #10756.

This is a proposal to rename what was in mathlib `Group` and in mathlib4 `GroupCat` to its literature name `Grp`. This has the advantage not to conflict with `group` that has been capitalised to `Group` and to be shorter.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

… sets (#13638)

We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` 
iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.

Put materials about (Mv)Polynomial into Kaehler/Polynomial and the others into Kaehler/Basic