feat(AlgebraicGeometry): define algebraic cycles (#37901)

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>

Author: Raph-DG

Mathlib.lean

@@ -1346,6 +1346,7 @@ public import Mathlib.AlgebraicGeometry.AffineScheme
 public import Mathlib.AlgebraicGeometry.AffineSpace
 public import Mathlib.AlgebraicGeometry.AffineTransitionLimit
 public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
+public import Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
 public import Mathlib.AlgebraicGeometry.Artinian
 public import Mathlib.AlgebraicGeometry.Birational.Dominant
 public import Mathlib.AlgebraicGeometry.Birational.RationalMap

Mathlib/AlgebraicGeometry/AlgebraicCycle/Basic.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Raphael Douglas Giles. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Raphael Douglas Giles
+-/
+module
+
+public import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
+public import Mathlib.AlgebraicGeometry.Properties
+public import Mathlib.Topology.LocallyFinsupp.Pushforward
+public import Mathlib.AlgebraicGeometry.ResidueField
+
+/-!
+# Algebraic Cycles
+
+In this file we define algebraic cycles on a scheme `X` with coefficients in a type `R` and provide
+some basic API for working with them. We define an algebraic cycle on a scheme `X` with
+coefficients in a type `R` to be functions `c : X → R` whose support is locally finite.
+
+## Implementation notes
+
+Here we're making use of the equivalence between irreducible closed subsets of a scheme and their
+generic points in order to reuse the API in `Function.locallyFinsupp`, hence the slightly
+nonstandard definition.
+-/
+
+@[expose] public section
+
+namespace AlgebraicGeometry
+
+open CategoryTheory
+
+universe u v
+variable {X Y : Scheme.{u}} {R : Type*}
+
+/--
+Algebraic cycle on a scheme `X` with coefficients in a type `Z` is just a function from `X` to `Z`
+with locally finite support (see the module docstring for more details).
+
+Note: currently this is an abbrev to save some effort in duplicating API. This seems fine for now,
+but be aware of this if there is ever an instance clash involving algebraic cycles.
+-/
+@[stacks 02QR]
+abbrev AlgebraicCycle (X : Scheme.{u}) (R : Type*) [Zero R] :=
+  Function.locallyFinsupp X R
+
+variable (f : X ⟶ Y) [Semiring R] (c : AlgebraicCycle X R) (x : X) (z : Y)
+namespace AlgebraicCycle
+
+/--
+Implementation detail for `AlgebraicCycle.map`: function used to define the coefficient of the
+pushforward of a cycle `c` at a point `z = f x`.
+-/
+@[stacks 02R3]
+noncomputable def mapCoeff {N : Type*} [DecidableEq N] {Y : Scheme} (f : X ⟶ Y) (wx : X → N)
+    (wy : Y → N) (x : X) : ℕ := if wx x = wy (f.base x) then f.residueDegree x else 0
+
+/--
+The pushforward of algebraic cycles with respect to a quasicompact morphism of schemes. The
+arguments `wx` and `wy` are certain weight functions used to calculate how the weights of the
+algebraic cycle should be adjusted to make the pushforward operation functorial. Typically in
+applications these will be some notions of dimension or codimension. The most common notion of
+dimension is `Order.height`, and the most common notion of codimension is `Order.coheight`, though
+more sophisticated notions exist in the literature which are useful when sufficient
+equidimensionality hypotheses cannot be assumed.
+-/
+@[stacks 02R3]
+noncomputable
+def map [QuasiCompact f] {N : Type*} [DecidableEq N] (wx : X → N) (wy : Y → N)
+    (c : AlgebraicCycle X R) : AlgebraicCycle Y R :=
+  Function.locallyFinsupp.map f (Nat.cast (R := R) <| mapCoeff f wx wy ·) f.isSpectralMap c
+
+@[simp]
+lemma map_id {N : Type*} [DecidableEq N] (wx : X → N) (c : AlgebraicCycle X R) :
+    map (𝟙 _) wx wx c = c := by
+  apply Function.locallyFinsupp.map_id
+  simp [mapCoeff]
+
+end AlgebraicGeometry.AlgebraicCycle

Mathlib/AlgebraicGeometry/ResidueField.lean

@@ -140,6 +140,20 @@ lemma residueFieldMap_comp {Z : Scheme.{u}} (g : Y ⟶ Z) (x : X) :
     (f ≫ g).residueFieldMap x = g.residueFieldMap (f x) ≫ f.residueFieldMap x :=
   LocallyRingedSpace.residueFieldMap_comp _ _ _
 
+/--
+Degree of `f` at a point `x` is defined to be the degree of the associated field extension
+from `κ(f x)` to `κ(x)`. We return a default value of zero when this degree is infinite.
+-/
+def Hom.residueDegree (f : X ⟶ Y) (x : X) : ℕ :=
+  letI := (f.residueFieldMap x).hom.toAlgebra
+  Module.finrank (Y.residueField (f x)) (X.residueField x)
+
+@[simp]
+lemma Hom.residueDegree_id (x : X) : (𝟙 _ : X ⟶ X).residueDegree x = 1 := by
+  dsimp [residueDegree]
+  rw [residueFieldMap_id]
+  exact CommSemiring.finrank_self _
+
 @[reassoc]
 lemma evaluation_naturality {V : Opens Y} (x : X) (hx : f x ∈ V) :
     Y.evaluation V (f x) hx ≫ f.residueFieldMap x =