Theorems · Definition · algebraic geometry

AlgebraicGeometry.AlgebraicCycle.map

{X Y : AlgebraicGeometry.Scheme} →
  {R : Type u_1} →
    (f : X ⟶ Y) →
      [inst : Semiring R] →
        [AlgebraicGeometry.QuasiCompact f] →
          {N : Type u_2} →
            [DecidableEq N] →
              (↥X → N) → (↥Y → N) → AlgebraicGeometry.AlgebraicCycle X R → AlgebraicGeometry.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.

Defined in

Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic

Cited by

1 results in Mathlib

Foundations

Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAlgebraicGeometry.QuasiCompactDecidableEq