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.

@[reducible, inline]

abbrev AlgebraicGeometry.AlgebraicCycle (X : Scheme) (R : Type u_2) [Zero R] : Type (max u u_2)

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.

Equations

• AlgebraicGeometry.AlgebraicCycle X R = Function.locallyFinsupp (↥X) R

noncomputable def AlgebraicGeometry.AlgebraicCycle.mapCoeff {X : Scheme} {N : Type u_2} [DecidableEq N] {Y : Scheme} (f : X ⟶ Y) (wx : ↥X → N) (wy : ↥Y → N) (x : ↥X) : ℕ

Implementation detail for AlgebraicCycle.map: function used to define the coefficient of the pushforward of a cycle c at a point z = f x.

Equations

• AlgebraicGeometry.AlgebraicCycle.mapCoeff f wx wy x = if wx x = wy (f x) then AlgebraicGeometry.Scheme.Hom.residueDegree f x else 0

noncomputable def AlgebraicGeometry.AlgebraicCycle.map {X Y : Scheme} {R : Type u_1} (f : X ⟶ Y) [Semiring R] [QuasiCompact f] {N : Type u_2} [DecidableEq N] (wx : ↥X → N) (wy : ↥Y → N) (c : AlgebraicCycle X R) : AlgebraicCycle Y R

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.

Equations

• AlgebraicGeometry.AlgebraicCycle.map f wx wy c = Function.locallyFinsupp.map (⇑f) (fun (x : ↥X) => ↑(AlgebraicGeometry.AlgebraicCycle.mapCoeff f wx wy x)) ⋯ c

@[simp]

theorem AlgebraicGeometry.AlgebraicCycle.map_id {X : Scheme} {R : Type u_1} [Semiring R] {N : Type u_2} [DecidableEq N] (wx : ↥X → N) (c : AlgebraicCycle X R) : map (CategoryTheory.CategoryStruct.id X) wx wx c = c