Pushforward of functions with locally finite support

In this file we define the notion of the pushforward of a function with locally finite support between prespectral spaces along a spectral map. This is used for defining the (proper) pushforward of algebraic cycles in algebraic geometry.

Main declarations

• Function.locallyFinsupp.map: If f : X → Y is a spectral map between spectral spaces and c : X → R is locally of finite support, the pushforward of c along f at y : Y is ∑ᶠ x ∈ f ⁻¹' {y}, c x * w x, where w : X → R is a weight function.

Notes

In the case of algebraic cycles, the weight function used in Function.locallyFinsupp.map will be specialized to the degree of the residue field extension (see https://stacks.math.columbia.edu/tag/02R4).

noncomputable def Function.locallyFinsupp.map {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (w : X → R) [Semiring R] [PrespectralSpace Y] (hf : IsSpectralMap f) (c : locallyFinsupp X R) : locallyFinsupp Y R

The pushforward of a function c of locally finite support by a spectral map with respect to a weight function w.

Equations

• Function.locallyFinsupp.map f w hf c = { toFun := fun (z : Y) => ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem Function.locallyFinsupp.map_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (w : X → R) [Semiring R] [PrespectralSpace Y] (hf : IsSpectralMap f) (c : locallyFinsupp X R) (y : Y) : (map f w hf c) y = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {y}), c x * w x

theorem Function.locallyFinsupp.support_map_subset_of_forall_mem {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsSpectralMap f) (w : X → R) [Semiring R] (c : locallyFinsupp X R) [PrespectralSpace Y] (s : Set X) (t : Set Y) (hc : locallyFinsuppWithin.support c ⊆ s) (h : ∀ x ∈ s, w x ≠ 0 → f x ∈ t) : locallyFinsuppWithin.support (map f w hf c) ⊆ t

@[simp]

theorem Function.locallyFinsupp.map_id {X : Type u_1} {R : Type u_3} [TopologicalSpace X] (w : X → R) [Semiring R] (c : locallyFinsupp X R) [PrespectralSpace X] (hw : ∀ (z : X), w z = 1) : map id w ⋯ c = c