From d5f980c7d796a97a94623f52e173d55792599e8b Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Thu, 21 May 2026 21:02:29 +0200 Subject: [PATCH 01/13] Copy stuff from pushforward PR --- Mathlib/Topology/LocallyFinsupp.lean | 8 ++ .../Topology/LocallyFinsupp/Pushforward.lean | 93 +++++++++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 Mathlib/Topology/LocallyFinsupp/Pushforward.lean diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean index 80612fc9ca39a6..50ce1abefbe599 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..ec18713b9ccc65 --- /dev/null +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -0,0 +1,93 @@ +/- +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. This is a nonstandard notion that arises because of our choice in +mathlib to model algebraic cycles as functions with locally finite support. +This makes it so that standard notions in the theory of cycles can be defined in more generality +than usual, and allows us to reuse a lot of API to develop the theory of cycles. + +In the usual definition of the proper pushforward of algebraic cycles, one needs to adjust the +coefficients by scaling by the degree of the corresponding extension of residue fields (assuming +the dimensions are the same and hence that this is a finite extension), or in the case where the +dimensions of the points differ scaling by zero. This is described in more detail in stacks 02R4. +The exact values of this scaling function are not relevant for the mere construction of the +pushforward, so our definition of the pushforward of a cycle `c` on a scheme `X` with coefficients +in `R` is done with respect to some `w : X → R`, about which we do not assume anything. +-/ + +@[expose] public section + +open Set Order Topology TopologicalSpace + +universe u v +variable {X Y R : Type*} [TopologicalSpace X] [TopologicalSpace Y] + {f : X → Y} (hf : IsSpectralMap f) (w : X → R) + +namespace Function.locallyFinsupp + +section map + +variable [Semiring R] {W : Set Y} (hW : IsOpen W) (c : Function.locallyFinsupp X R) + +variable [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`. This is mainly used when interpretting +locally fin supp functions as algebraic cycles (in this case the weight function would be as +described in stacks 02R4, where the weight function is the degree of the corresponding extension of +residue fields if the dimensions of the points correspond, and is zero otherwise). +-/ +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 map_homogeneous (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] + +/-- +The pushforward of `c` along the identity morphism is `c` as long as the weight function is `1` +everywhere. One should note that typically this weight function depends on the map, so this +condition that the weight function must be trivial here is less strange than it may appear at first. +-/ +@[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 map +end Function.locallyFinsupp From 4bea9a03947c9ac55d25ab35c5491c9e07ad538e Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Thu, 21 May 2026 21:32:26 +0200 Subject: [PATCH 02/13] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 4920a8a86d5efc..294fde58f4eec1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7718,6 +7718,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 From 3e9eed1f654fe8f5c49c931668bfc0fccdc7a5de Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:16:32 +0200 Subject: [PATCH 03/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index ec18713b9ccc65..f8ec935f86bec5 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -78,11 +78,6 @@ lemma map_homogeneous (s : Set X) (t : Set Y) (hc : c.support ⊆ s) obtain ⟨x, (rfl : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy grind [mem_support] -/-- -The pushforward of `c` along the identity morphism is `c` as long as the weight function is `1` -everywhere. One should note that typically this weight function depends on the map, so this -condition that the weight function must be trivial here is less strange than it may appear at first. --/ @[simp] lemma map_id [PrespectralSpace X] (hw : ∀ z : X, w z = 1) : map id w isSpectralMap_id c = c := by From 1d0a2629a1534d3b1894cb4ed39353e390ebcc08 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:17:30 +0200 Subject: [PATCH 04/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index f8ec935f86bec5..06a66222c3d37a 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -72,7 +72,7 @@ def map (hf : IsSpectralMap f) (c : locallyFinsupp X R) : Function.locallyFinsup 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 map_homogeneous (s : Set X) (t : Set Y) (hc : c.support ⊆ s) +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 From 6fef1859077673cd3766caa1d31e6d7322a1b800 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:17:58 +0200 Subject: [PATCH 05/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- .../Topology/LocallyFinsupp/Pushforward.lean | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 06a66222c3d37a..1761424943d39a 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -12,18 +12,19 @@ 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. This is a nonstandard notion that arises because of our choice in -mathlib to model algebraic cycles as functions with locally finite support. -This makes it so that standard notions in the theory of cycles can be defined in more generality -than usual, and allows us to reuse a lot of API to develop the theory of cycles. - -In the usual definition of the proper pushforward of algebraic cycles, one needs to adjust the -coefficients by scaling by the degree of the corresponding extension of residue fields (assuming -the dimensions are the same and hence that this is a finite extension), or in the case where the -dimensions of the points differ scaling by zero. This is described in more detail in stacks 02R4. -The exact values of this scaling function are not relevant for the mere construction of the -pushforward, so our definition of the pushforward of a cycle `c` on a scheme `X` with coefficients -in `R` is done with respect to some `w : X → R`, about which we do not assume anything. +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 a + locally of finite support, the pushforward of `c` along `f` at `y : Y` is `∑ᶠ x ∈ f ⁻¹' {z}, 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 From 84e453dfc29cd7ac0758fb4cea01a920addb7eca Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:18:17 +0200 Subject: [PATCH 06/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 1761424943d39a..1186f7cc8e208a 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -45,11 +45,7 @@ variable [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`. This is mainly used when interpretting -locally fin supp functions as algebraic cycles (in this case the weight function would be as -described in stacks 02R4, where the weight function is the degree of the corresponding extension of -residue fields if the dimensions of the points correspond, and is zero otherwise). +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 From ea7732cbded31db9be875ff273ffe888cf276658 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:18:45 +0200 Subject: [PATCH 07/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 1186f7cc8e208a..c221e553f09e0e 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -40,8 +40,7 @@ namespace Function.locallyFinsupp section map variable [Semiring R] {W : Set Y} (hW : IsOpen W) (c : Function.locallyFinsupp X R) - -variable [PrespectralSpace Y] + [PrespectralSpace Y] variable (f) in /-- From ec44b1647e5507e6a6d2e5550b55af32c7059f36 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:19:04 +0200 Subject: [PATCH 08/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index c221e553f09e0e..96ba8d6636bad5 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -31,7 +31,6 @@ In the case of algebraic cycles, the weight function used in `Function.locallyFi open Set Order Topology TopologicalSpace -universe u v variable {X Y R : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsSpectralMap f) (w : X → R) From fb36aecf856fd435ea322aa7569a3cb778eda22c Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:29:11 +0200 Subject: [PATCH 09/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 96ba8d6636bad5..a0b5814e09355a 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -36,8 +36,6 @@ variable {X Y R : Type*} [TopologicalSpace X] [TopologicalSpace Y] namespace Function.locallyFinsupp -section map - variable [Semiring R] {W : Set Y} (hW : IsOpen W) (c : Function.locallyFinsupp X R) [PrespectralSpace Y] From 1839d2f9fc0cf3d77dbb78542b9c32df74a5d5d5 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 14:29:29 +0200 Subject: [PATCH 10/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index a0b5814e09355a..8ca3ccab76f0e1 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -77,5 +77,4 @@ lemma map_id [PrespectralSpace X] (hw : ∀ z : X, w z = 1) : ext simp [map, hw] -end map end Function.locallyFinsupp From 449761e909361047bbef098edb7ff8b7e34e4f6b Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Tue, 26 May 2026 14:35:21 +0200 Subject: [PATCH 11/13] Fixed lines which were too long --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 8ca3ccab76f0e1..19da42c91b1039 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -17,13 +17,14 @@ 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 a - locally of finite support, the pushforward of `c` along `f` at `y : Y` is `∑ᶠ x ∈ f ⁻¹' {z}, c x * w x`, where - `w : X → R` is a weight function. +- `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 ⁻¹' {z}, 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 +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). -/ @@ -41,7 +42,8 @@ variable [Semiring R] {W : Set Y} (hW : IsOpen W) (c : Function.locallyFinsupp X variable (f) in /-- -The pushforward of a function `c` of locally finite support by a spectral map with respect to a weight function `w`. +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 From 3c7052a53488677c343a0d6d6dbec54a76a2d640 Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Tue, 26 May 2026 15:27:18 +0200 Subject: [PATCH 12/13] Triggering CI From 4b3db1614d1dbf71058a7776bc73fd2d538e3a4c Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Tue, 26 May 2026 15:47:24 +0200 Subject: [PATCH 13/13] Update Mathlib/Topology/LocallyFinsupp/Pushforward.lean Co-authored-by: Christian Merten --- Mathlib/Topology/LocallyFinsupp/Pushforward.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean index 19da42c91b1039..caa37458bda0ae 100644 --- a/Mathlib/Topology/LocallyFinsupp/Pushforward.lean +++ b/Mathlib/Topology/LocallyFinsupp/Pushforward.lean @@ -19,7 +19,7 @@ of algebraic cycles in algebraic geometry. - `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 ⁻¹' {z}, c x * w x`, where `w : X → R` is a weight function. + `∑ᶠ x ∈ f ⁻¹' {y}, c x * w x`, where `w : X → R` is a weight function. ## Notes