diff --git a/Mathlib.lean b/Mathlib.lean
index 14ee8ec6788e43..f953d85e7af5d1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7818,6 +7818,7 @@ public import Mathlib.Topology.LocallyConstant.Algebra
 public import Mathlib.Topology.LocallyConstant.Basic
 public import Mathlib.Topology.LocallyFinite
 public import Mathlib.Topology.LocallyFinsupp
+public import Mathlib.Topology.LocallyFinsupp.Pushforward
 public import Mathlib.Topology.Maps.Basic
 public import Mathlib.Topology.Maps.OpenQuotient
 public import Mathlib.Topology.Maps.Proper.Basic
diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index c3eac2f6669606..d4da4994684ac8 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -126,6 +126,14 @@ instance [Zero Y] : FunLike (locallyFinsuppWithin U Y) X Y where
   coe D := D.toFun
   coe_injective' := fun ⟨_, _, _⟩ ⟨_, _, _⟩ ↦ by simp
 
+@[simp]
+lemma toFun_eq_coe [Zero Y] (c : locallyFinsuppWithin U Y) : c.toFun = ⇑c := rfl
+
+@[simp]
+lemma coe_mk [Zero Y] (f : X → Y) (h : f.support ⊆ U)
+    (h' : ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)) :
+    ⇑(Function.locallyFinsuppWithin.mk f h h') = f := rfl
+
 /-- This allows writing `D.support` instead of `Function.support D` -/
 abbrev support [Zero Y] (D : locallyFinsuppWithin U Y) := Function.support D
 
diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean
new file mode 100644
index 00000000000000..caa37458bda0ae
--- /dev/null
+++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean
@@ -0,0 +1,82 @@
+/-
+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.Topology.LocallyFinsupp
+public import Mathlib.Topology.Spectral.Basic
+
+/-!
+# 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).
+-/
+
+@[expose] public section
+
+open Set Order Topology TopologicalSpace
+
+variable {X Y R : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+  {f : X → Y} (hf : IsSpectralMap f) (w : X → R)
+
+namespace Function.locallyFinsupp
+
+variable [Semiring R] {W : Set Y} (hW : IsOpen W) (c : Function.locallyFinsupp X R)
+  [PrespectralSpace Y]
+
+variable (f) in
+/--
+The pushforward of a function `c` of locally finite support by a spectral map with respect to a
+weight function `w`.
+-/
+noncomputable
+def map (hf : IsSpectralMap f) (c : locallyFinsupp X R) : Function.locallyFinsupp Y R where
+  toFun z := ∑ᶠ x ∈ f ⁻¹' {z}, c x * w x
+  supportWithinDomain' := by simp
+  supportLocallyFiniteWithinDomain' y _ := by
+    obtain ⟨U, hU⟩ := (PrespectralSpace.isTopologicalBasis (X := Y)).exists_subset_of_mem_open
+      (by simp : y ∈ ⊤) (by simp)
+    refine ⟨U, IsOpen.mem_nhds hU.1.1 hU.2.1, ?_⟩
+    suffices h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite by
+      refine h.subset (inter_subset_inter_right U fun y hy ↦ ?_)
+      obtain ⟨x, (hx : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy
+      use x
+      grind [mem_support]
+    suffices (f ⁻¹' (U ∩ {z | (f ⁻¹' {z} ∩ c.support).Nonempty}) ∩ c.support).Finite from
+      (this.image f).subset (fun a ha ↦ by grind [Set.Nonempty])
+    exact (c.locallyFiniteSupport.finite_inter_support_of_isCompact <| hf.2 hU.1.1 hU.1.2).subset
+      (by simp; grind)
+
+@[simp]
+lemma map_apply (hf : IsSpectralMap f) (c : locallyFinsupp X R) (y : Y) :
+    map f w hf c y = ∑ᶠ x ∈ f ⁻¹' {y}, c x * w x := rfl
+
+lemma support_map_subset_of_forall_mem (s : Set X) (t : Set Y) (hc : c.support ⊆ s)
+    (h : ∀ x : X, x ∈ s → w x ≠ 0 → f x ∈ t) : (map f w hf c).support ⊆ t := by
+  intro y hy
+  obtain ⟨x, (rfl : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy
+  grind [mem_support]
+
+@[simp]
+lemma map_id [PrespectralSpace X] (hw : ∀ z : X, w z = 1) :
+    map id w isSpectralMap_id c = c := by
+  ext
+  simp [map, hw]
+
+end Function.locallyFinsupp