[Merged by Bors] - feat(AlgebraicGeometry): define algebraic cycles#37901
[Merged by Bors] - feat(AlgebraicGeometry): define algebraic cycles#37901Raph-DG wants to merge 79 commits into
Conversation
Co-authored-by: Christian Merten <christian@merten.dev>
Raph-DG
removed
the
awaiting-author
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <christian@merten.dev>
|
🚀 Pull request has been placed on the maintainer queue by chrisflav. |
mathlib-triage
Bot
added
the
maintainer-merge
grunweg
changed the title
riccardobrasca
left a comment
riccardobrasca
left a comment
There was a problem hiding this comment.
Can you add the relevant stack project tags?
| pushforward of a cycle `c` at a point `z = f x`, as in stacks `02R3`. | ||
| -/ | ||
| noncomputable | ||
| def mapAux {N : Type*} [DecidableEq N] {Y : Scheme} (f : X ⟶ Y) (wx : X → N) (wy : Y → N) (x : X) : |
There was a problem hiding this comment.
Can you make this private?
| (see the module docstring for more details). | ||
| -/ | ||
| @[stacks 02QR] | ||
| abbrev AlgebraicCycle (X : Scheme.{u}) (R : Type*) [Zero R] := |
There was a problem hiding this comment.
Why is this an abbrev rather than a def? I am not sure but, beside the basic API, I expect that cycles will have their own API.
There was a problem hiding this comment.
It just saves a lot of effort duplicating all of the Function.locallyFinsuppWithin API, and having this as an abbrev hasn't caused problems for me so far. I suppose this is also modelled on the situation in analysis, where divisors are just defined to be terms of type Function.locallyFinsuppWithin (see, e.g. MeromorphicOn.divisor)
There was a problem hiding this comment.
OK, can you maybe add a short comment? I am just afraid of some instance clash at some point, but we can always change if needed. Thanks!
|
bors d+ |
mathlib-bors
Bot
added
the
delegated
|
✌️ Raph-DG can now approve this pull request until 2026-07-09 12:17 UTC (in 2 weeks). To approve and merge, reply with
|
mathlib-triage
Bot
removed
the
maintainer-merge
…ion of AlgebraicCycle
|
Thanks! bors r+ |
In this PR we define the notion of algebraic cycles on a scheme, and define the pushforward of an algebraic cycle by a quasicompact morhphism. This was originally defined in #26304, but after some refactoring it was decided that it would be best to split this definition into a separate PR. Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
mathlib-bors
Bot
added
the
bors-staging
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
mathlib-bors
Bot
removed
the
delegated
5 participants
In this PR we define the notion of algebraic cycles on a scheme, and define the pushforward of an algebraic cycle by a quasicompact morhphism. This was originally defined in #26304, but after some refactoring it was decided that it would be best to split this definition into a separate PR.