Theorems · Definition · algebraic geometry

AlgebraicGeometry.AlgebraicCycle

AlgebraicGeometry.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.

Defined in

Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

Zero