feat(AlgebraicGeometry): Pushforward of algebraic cycles

[Raph-DG]

In this PR we define a notion of the "pushfoward of functions with locally finite support". We give this PR the suggestive title "pushforward of algebraic cycles" because we will go on to model algebraic cycles on a scheme X as functions from X to the integers with locally finite support.

• depends on: [Merged by Bors] - feat(AlgebraicGeometry): Add some minimal API for orders on schemes #26225
• depends on: [Merged by Bors] - feat(Topology): Connecting different notions of locally finite #26259
• depends on: [Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin  #35807

---

[github-actions]

PR summary 4bea9a0394

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.LocallyFinsupp.Pushforward (new file)	938

---

Declarations diff

+ coe_mk
+ map
+ map_apply
+ map_homogeneous
+ map_id
+ toFun_eq_coe

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[leanprover-community-bot-assistant]

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

[chrisflav]

After some discussion with Andrew, the following is my suggestion for this PR:

• Define a pushforward for Function.locallyFinsupp for prespectral and sober topological spaces taking a weight function as an argument X → R, which is what replaces the mapAux (the proof might require some more topological assumptions, of which we can of course assume the ones that are true in the application).
• Given s : Set X, t : Set Y and a Function.locallyFinsupp with support in s, there should be a lemma showing that, under some compatibility with the weights, the image of the pushforward has support in t.
• This will then induce a map between the "homogeneous cycles", which is just the additive submonoid of cycles with support in a given set.

In the next PR, I would suggest to:

• Add the abbrev for AlgebraicCycle as it is done here.
• Define the weights function for a morphism of schemes as you do here, but make it Nat-valued. This will still allow to apply the above construction by coercing the Nats to elements of the coefficient ring.
• Remove Grading and HasDegree.

[mathlib-merge-conflicts]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): Add some minimal API for orders on schemes #26225
• [Merged by Bors] - feat(Topology): Connecting different notions of locally finite #26259
• [Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin  #35807
  By Dependent Issues (🤖). Happy coding!

[Raph-DG]

After some discussion with Andrew, the following is my suggestion for this PR:

• Define a pushforward for Function.locallyFinsupp for prespectral and sober topological spaces taking a weight function as an argument X → R, which is what replaces the mapAux (the proof might require some more topological assumptions, of which we can of course assume the ones that are true in the application).
• Given s : Set X, t : Set Y and a Function.locallyFinsupp with support in s, there should be a lemma showing that, under some compatibility with the weights, the image of the pushforward has support in t.
• This will then induce a map between the "homogeneous cycles", which is just the additive submonoid of cycles with support in a given set.

In the next PR, I would suggest to:

• Add the abbrev for AlgebraicCycle as it is done here.
• Define the weights function for a morphism of schemes as you do here, but make it Nat-valued. This will still allow to apply the above construction by coercing the Nats to elements of the coefficient ring.
• Remove Grading and HasDegree.

What's here I think fulfils this, but I now think it's probably more sensible design-wise to directly use Function.locallyFinsuppWithin to talk about locally finsupp functions with support in s. I'm temporarily making this PR WIP to try and do such a refactor.

Edit: Christian already knows this, but for anyone else who happens to be reading this, we realised this idea does not quite work so I've reverted this to the state it was in before I attempted the refactor and have removed the WIP label

[chrisflav]

If I remember correctly, I showed you how to rewrite this using wlog some time ago, but this proof looks like the old one. Could you please restore the wlog version or is that lost in time?

[Raph-DG]

Yes unfortunately I couldn't find this old version of the lemma (in fact I couldn't find the other proof either, I just rewrote this and I suppose I made the same mistake again). I'll try and rewrite it using wlog, but I'm a little bit hazy on the details of how that improvement to the code went tbh

[Raph-DG]

I had a go using wlog for this proof. I think what's there is definitely conceptually cleaner and there is less repetition, but it's still less clean than I remember the proof you showed me