Skip to content

Commit d72ce4d

Browse files
ADedeckerBergschaf
ADedecker
authored and
Bergschaf
committed
feat: LinearMap.HasFiniteRange and the associated relation (leanprover-community#39468)
We add two predicates on linear maps: `HasFiniteRange` says that the range is finitely generated, and `HasNoetherianRange` says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition. This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators. This also adds four supporting lemmas: `map_smul_le_map`, `range_smul_le_range`, `ker_le_ker_smul` and `isNoetherian_map`.
1 parent ecbb77c commit d72ce4d

6 files changed

Lines changed: 309 additions & 8 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -780,6 +780,7 @@ public import Mathlib.Algebra.Module.LinearMap.Basic
780780
public import Mathlib.Algebra.Module.LinearMap.Defs
781781
public import Mathlib.Algebra.Module.LinearMap.DivisionRing
782782
public import Mathlib.Algebra.Module.LinearMap.End
783+
public import Mathlib.Algebra.Module.LinearMap.FiniteRange
783784
public import Mathlib.Algebra.Module.LinearMap.Polynomial
784785
public import Mathlib.Algebra.Module.LinearMap.Prod
785786
public import Mathlib.Algebra.Module.LinearMap.Rat

‎Mathlib/Algebra/Module/LinearMap/FiniteRange.lean‎

Lines changed: 271 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,271 @@
1+
/-
2+
Copyright (c) 2026 Patrick Massot. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Patrick Massot, Anatole Dedecker
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Finiteness.Cofinite
9+
public import Mathlib.Algebra.Module.Submodule.EqLocus
10+
11+
/-!
12+
# `HasFiniteRange` predicate on linear maps, and the associated equivalence relation
13+
14+
In this file, we define:
15+
16+
* `LinearMap.HasFiniteRange`: a predicate expressing that a linear map has finitely generated range.
17+
* `LinearMap.HasNoetherianRange`: a predicate expressing that a linear map has noetherian range,
18+
i.e, all submodules of the range are finitely generated. This should be thought of as the
19+
"better behaved" version of `LinearMap.HasFiniteRange`: for example, `HasNoetherianRange`
20+
is always stable by addition, whereas `HasFiniteRange` might not be. The two notions agree
21+
over noetherian rings (hence, in particular, over fields).
22+
* `LinearMap.finiteRange`: the submodule of `E →ₗ[K] F` consisting of linear maps with
23+
*noetherian* ranges. We allow ourself this slightly abusive name because the more natural
24+
definition (the submodule of linear maps with finitely generated ranges) only makes sense over a
25+
noetherian ring, in which case the two notions agree.
26+
* `LinearMap.FiniteRangeSetoid.setoid`: the setoid on `E →ₗ[K] F` associated to
27+
`LinearMap.finiteRange`. This identifies linear maps which differ by a linear map with
28+
noetherian range. Equivalently, two linear maps are equivalent for this
29+
relation if and only if they agree on a subspace `A` of the domain such that `E ⧸ A` is
30+
noetherian. As with `LinearMap.finiteRange`, we allow ourself a slightly abusive name because the
31+
more natural definition in terms of `LinearMap.HasFiniteRange` is only well behaved over a
32+
noetherian ring, in which case the two notions agree.
33+
This is an instance in the scope `LinearMap.FiniteRangeSetoid`,
34+
so opening this scope allows this relation to be denoted by `≈`.
35+
-/
36+
37+
@[expose] public section
38+
39+
open LinearMap Submodule Module
40+
41+
namespace LinearMap
42+
43+
variable {K V V' V₂ V₂' V₃ : Type*}
44+
45+
section Semiring
46+
47+
variable [Semiring K]
48+
[AddCommMonoid V] [Module K V]
49+
[AddCommMonoid V₂] [Module K V₂]
50+
[AddCommMonoid V₃] [Module K V₃]
51+
52+
/-- A linear map **has Noetherian range** if its range is a Noetherian module. -/
53+
def HasNoetherianRange (f : V →ₗ[K] V₂) := IsNoetherian K f.range
54+
55+
/-- A linear map **has finite range** if its range is finitely generated. -/
56+
def HasFiniteRange (f : V →ₗ[K] V₂) := f.range.FG
57+
58+
lemma hasNoetherianRange_iff_range {f : V →ₗ[K] V₂} :
59+
f.HasNoetherianRange ↔ IsNoetherian K f.range :=
60+
Iff.rfl
61+
62+
lemma hasFiniteRange_iff_range {f : V →ₗ[K] V₂} :
63+
f.HasFiniteRange ↔ f.range.FG :=
64+
Iff.rfl
65+
66+
alias ⟨HasNoetherianRange.isNoetherian_range, _⟩ := hasNoetherianRange_iff_range
67+
alias ⟨HasFiniteRange.fg_range, _⟩ := hasFiniteRange_iff_range
68+
69+
lemma HasNoetherianRange.hasFiniteRange {u : V →ₗ[K] V₂} (h : u.HasNoetherianRange) :
70+
u.HasFiniteRange :=
71+
have := h.isNoetherian_range; FG.of_finite
72+
73+
@[simp] lemma HasNoetherianRange.zero : (0 : V →ₗ[K] V₂).HasNoetherianRange := by
74+
simp [HasNoetherianRange, isNoetherian_submodule, Submodule.fg_bot]
75+
76+
@[simp] lemma HasFiniteRange.zero : (0 : V →ₗ[K] V₂).HasFiniteRange :=
77+
HasNoetherianRange.zero.hasFiniteRange
78+
79+
lemma HasNoetherianRange.comp_left {u : V →ₗ[K] V₂} (h : u.HasNoetherianRange)
80+
(v : V₂ →ₗ[K] V₃) : (v ∘ₗ u).HasNoetherianRange := by
81+
rw [LinearMap.HasNoetherianRange, LinearMap.range_comp] at *
82+
infer_instance
83+
84+
lemma HasFiniteRange.comp_left {u : V →ₗ[K] V₂} (h : u.HasFiniteRange)
85+
(v : V₂ →ₗ[K] V₃) : (v ∘ₗ u).HasFiniteRange := by
86+
rw [LinearMap.HasFiniteRange, LinearMap.range_comp] at *
87+
exact Submodule.FG.map v h
88+
89+
@[simp] lemma HasNoetherianRange.of_isNoetherian_dom [IsNoetherian K V] {f : V →ₗ[K] V₂} :
90+
f.HasNoetherianRange :=
91+
hasNoetherianRange_iff_range.mpr inferInstance
92+
93+
@[simp] lemma HasFiniteRange.of_finite_dom [Module.Finite K V] {f : V →ₗ[K] V₂} :
94+
f.HasFiniteRange := by
95+
simp [HasFiniteRange]
96+
97+
@[simp] lemma HasNoetherianRange.of_isNoetherian_rng [IsNoetherian K V₂] {f : V →ₗ[K] V₂} :
98+
f.HasNoetherianRange :=
99+
hasNoetherianRange_iff_range.mpr inferInstance
100+
101+
@[simp] lemma HasFiniteRange.of_isNoetherian_rng [IsNoetherian K V₂] {f : V →ₗ[K] V₂} :
102+
f.HasFiniteRange :=
103+
HasNoetherianRange.of_isNoetherian_rng.hasFiniteRange
104+
105+
end Semiring
106+
107+
section Ring
108+
109+
variable [Ring K]
110+
[AddCommGroup V] [Module K V]
111+
[AddCommGroup V₂] [Module K V₂]
112+
[AddCommGroup V₃] [Module K V₃]
113+
114+
lemma HasFiniteRange.hasNoetherianRange [IsNoetherianRing K] {u : V →ₗ[K] V₂}
115+
(h : u.HasFiniteRange) : u.HasNoetherianRange := by
116+
rw [HasNoetherianRange]
117+
have := Finite.of_fg h.fg_range
118+
infer_instance
119+
120+
lemma hasNoetherianRange_iff_hasFiniteRange [IsNoetherianRing K] {u : V →ₗ[K] V₂} :
121+
u.HasNoetherianRange ↔ u.HasFiniteRange :=
122+
⟨HasNoetherianRange.hasFiniteRange, HasFiniteRange.hasNoetherianRange⟩
123+
124+
lemma HasNoetherianRange.comp_right {v : V₂ →ₗ[K] V₃} (h : v.HasNoetherianRange)
125+
(u : V →ₗ[K] V₂) : (v ∘ₗ u).HasNoetherianRange := by
126+
rw [HasNoetherianRange, LinearMap.range_comp] at *
127+
exact isNoetherian_of_le map_le_range
128+
129+
lemma HasFiniteRange.comp_right [IsNoetherianRing K] {v : V₂ →ₗ[K] V₃} (h : v.HasFiniteRange)
130+
(u : V →ₗ[K] V₂) : (v ∘ₗ u).HasFiniteRange :=
131+
h.hasNoetherianRange.comp_right _ |>.hasFiniteRange
132+
133+
@[simp] lemma HasNoetherianRange.neg {f : V →ₗ[K] V₂}
134+
(hf : f.HasNoetherianRange) : (-f).HasNoetherianRange := by
135+
rwa [HasNoetherianRange, LinearMap.range_neg]
136+
137+
@[simp] lemma HasFiniteRange.neg {f : V →ₗ[K] V₂}
138+
(hf : f.HasFiniteRange) : (-f).HasFiniteRange := by
139+
rwa [HasFiniteRange, LinearMap.range_neg]
140+
141+
@[simp] lemma HasNoetherianRange.add {f g : V →ₗ[K] V₂}
142+
(hf : f.HasNoetherianRange) (hg : g.HasNoetherianRange) : (f + g).HasNoetherianRange := by
143+
rw [HasNoetherianRange] at *
144+
exact isNoetherian_of_le (range_add_le f g)
145+
146+
@[simp] lemma HasFiniteRange.add [IsNoetherianRing K] {f g : V →ₗ[K] V₂}
147+
(hf : f.HasFiniteRange) (hg : g.HasFiniteRange) : (f + g).HasFiniteRange :=
148+
hf.hasNoetherianRange.add hg.hasNoetherianRange |>.hasFiniteRange
149+
150+
@[simp] lemma HasNoetherianRange.sub {f g : V →ₗ[K] V₂}
151+
(hf : f.HasNoetherianRange) (hg : g.HasNoetherianRange) : (f - g).HasNoetherianRange :=
152+
sub_eq_add_neg f g ▸ hf.add hg.neg
153+
154+
@[simp] lemma HasFiniteRange.sub [IsNoetherianRing K] {f g : V →ₗ[K] V₂}
155+
(hf : f.HasFiniteRange) (hg : g.HasFiniteRange) : (f - g).HasFiniteRange :=
156+
sub_eq_add_neg f g ▸ hf.add hg.neg
157+
158+
theorem hasNoetherianRange_iff_quotient_ker {f : V →ₗ[K] V₂} :
159+
f.HasNoetherianRange ↔ IsNoetherian K (V ⧸ f.ker) :=
160+
f.quotKerEquivRange.isNoetherian_iff.symm
161+
162+
@[simp]
163+
theorem ker_coFG_iff_hasFiniteRange {f : V →ₗ[K] V₂} :
164+
f.ker.CoFG ↔ f.HasFiniteRange :=
165+
range_fg_iff_ker_cofg.symm
166+
167+
alias ⟨HasNoetherianRange.quotient_ker, _⟩ := hasNoetherianRange_iff_quotient_ker
168+
alias ⟨_, HasFiniteRange.cofg_ker⟩ := ker_coFG_iff_hasFiniteRange
169+
170+
end Ring
171+
172+
section CommRing
173+
174+
variable [CommRing K]
175+
[AddCommGroup V] [Module K V]
176+
[AddCommGroup V₂] [Module K V₂]
177+
[AddCommGroup V₃] [Module K V₃]
178+
179+
@[simp] lemma HasNoetherianRange.smul {f : V →ₗ[K] V₂}
180+
(hf : f.HasNoetherianRange) (c : K) : (c • f).HasNoetherianRange :=
181+
hf.comp_left (lsmul K V₂ c)
182+
183+
@[simp] lemma HasFiniteRange.smul {f : V →ₗ[K] V₂}
184+
(hf : f.HasFiniteRange) (c : K) : (c • f).HasFiniteRange :=
185+
hf.comp_left (lsmul K V₂ c)
186+
187+
variable (K V V₂) in
188+
/-- `LinearMap.finiteRange` is the submodule of `V →ₗ[K] W` consisting of linear maps satisfying
189+
`LinearMap.HasNoetherianRange`. We allow ourself this slightly abusive name because the set of
190+
linear maps satisfying `LinearMap.HasFiniteRange` is only a submodule over a noetherian ring,
191+
in which case the two notions agree. -/
192+
def finiteRange : Submodule K (V →ₗ[K] V₂) where
193+
carrier := {u | u.HasNoetherianRange}
194+
add_mem' hu hv := by simp_all
195+
zero_mem' := by simp
196+
smul_mem' c hu := by simp_all
197+
198+
lemma mem_finiteRange_iff_hasNoetherianRange {f : V →ₗ[K] V₂} :
199+
f ∈ finiteRange K V V₂ ↔ f.HasNoetherianRange :=
200+
Iff.rfl
201+
202+
lemma mem_finiteRange_iff_hasFiniteRange [IsNoetherianRing K] {f : V →ₗ[K] V₂} :
203+
f ∈ finiteRange K V V₂ ↔ f.HasFiniteRange := by
204+
rw [mem_finiteRange_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
205+
206+
end CommRing
207+
208+
section Setoid
209+
210+
variable [CommRing K]
211+
[AddCommGroup V] [Module K V]
212+
[AddCommGroup V₂] [Module K V₂]
213+
[AddCommGroup V₃] [Module K V₃]
214+
215+
namespace FiniteRangeSetoid
216+
217+
/-- This is the equivalence relation on linear maps such that `u ≈ v` precisely
218+
when `u - v` is a linear map with noetherian range. We allow ourself this slightly abusive name
219+
because the more natural definition (`u - v` has finitely generated range) only yields a
220+
well-behaved relation (more precisely, an additive congruence relation compatible with composition
221+
on both sides) over a noetherian ring, in which case the two notions agree.
222+
223+
This setoid is declared as an instance in scope `LinearMap.FiniteRangeSetoid`. -/
224+
scoped instance setoid : Setoid (V →ₗ[K] V₂) := (LinearMap.finiteRange K V V₂).quotientRel
225+
226+
lemma equiv_iff_hasNoetherianRange {u v : V →ₗ[K] V₂} : u ≈ v ↔ (u - v).HasNoetherianRange :=
227+
Submodule.quotientRel_def _
228+
229+
lemma equiv_iff_hasFiniteRange [IsNoetherianRing K] {u v : V →ₗ[K] V₂} :
230+
u ≈ v ↔ (u - v).HasFiniteRange := by
231+
rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
232+
233+
lemma equiv_iff_isNoetherian_quotient_eqLocus {u v : V →ₗ[K] V₂} :
234+
u ≈ v ↔ IsNoetherian K (V ⧸ eqLocus u v) := by
235+
rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]
236+
237+
lemma equiv_iff_eqLocus_coFG [IsNoetherianRing K] {u v : V →ₗ[K] V₂} :
238+
u ≈ v ↔ (eqLocus u v).CoFG := by
239+
rw [eqLocus_eq_ker_sub, ker_coFG_iff_hasFiniteRange, equiv_iff_hasFiniteRange]
240+
241+
lemma equiv_of_eqOn_of_isNoetherian {u v : V →ₗ[K] V₂} (A : Submodule K V)
242+
[quot_A_noeth : IsNoetherian K (V ⧸ A)] (eqOn_A : Set.EqOn u v A) : u ≈ v := by
243+
have A_le : A ≤ eqLocus u v := le_eqLocus.mpr eqOn_A
244+
rw [equiv_iff_isNoetherian_quotient_eqLocus]
245+
refine isNoetherian_of_surjective (A.mapQ (eqLocus u v) id A_le) (by simp [range_mapQ])
246+
247+
lemma equiv_of_eqOn_coFG [IsNoetherianRing K] {u v : V →ₗ[K] V₂} {A : Submodule K V}
248+
(A_coFG : A.CoFG) (eqOn_A : Set.EqOn u v A) : u ≈ v :=
249+
equiv_iff_eqLocus_coFG.mpr <| A_coFG.of_le <| le_eqLocus.mpr eqOn_A
250+
251+
@[gcongr]
252+
lemma equiv_comp_right {u : V →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h' : v ≈ v') :
253+
v ∘ₗ u ≈ v' ∘ₗ u := by
254+
rw [equiv_iff_hasNoetherianRange] at *
255+
exact h'.comp_right u
256+
257+
@[gcongr]
258+
lemma equiv_comp_left {u v : V →ₗ[K] V₂} {u' : V₂ →ₗ[K] V₃} (h : u ≈ v) :
259+
u' ∘ₗ u ≈ u' ∘ₗ v := by
260+
rw [equiv_iff_hasNoetherianRange] at *
261+
simpa only [LinearMap.comp_sub] using h.comp_left u'
262+
263+
lemma equiv_comp {u v : V →ₗ[K] V₂} {u' v' : V₂ →ₗ[K] V₃} (h : u ≈ v) (h' : u' ≈ v') :
264+
u' ∘ₗ u ≈ v' ∘ₗ v := by
265+
grw [equiv_comp_right h', equiv_comp_left h]
266+
267+
end FiniteRangeSetoid
268+
269+
end Setoid
270+
271+
end LinearMap

‎Mathlib/Algebra/Module/Submodule/Ker.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -217,6 +217,17 @@ alias _root_.LinearMapClass.ker_eq_bot := ker_eq_bot
217217

218218
end Ring
219219

220+
section CommSemiring
221+
222+
variable [Semiring R] [CommSemiring R₂]
223+
variable [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂]
224+
variable {τ₁₂ : R →+* R₂}
225+
226+
theorem ker_le_ker_smul (f : M →ₛₗ[τ₁₂] M₂) (c : R₂) : ker f ≤ ker (c • f) := by
227+
simpa only [ker] using Submodule.comap_le_comap_smul _ _ _
228+
229+
end CommSemiring
230+
220231
section Semifield
221232

222233
variable [Semifield K]

‎Mathlib/Algebra/Module/Submodule/Map.lean‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -599,22 +599,25 @@ end Submodule
599599

600600
namespace Submodule
601601

602-
variable {N N₂ : Type*}
603-
variable [CommSemiring R] [CommSemiring R₂]
602+
variable {S N N₂ : Type*}
603+
variable [CommSemiring S] [Semiring R] [CommSemiring R₂]
604604
variable [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂]
605-
variable [AddCommMonoid N] [AddCommMonoid N₂] [Module R N] [Module R N₂]
606-
variable {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R}
607-
variable [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂]
605+
variable [AddCommMonoid N] [AddCommMonoid N₂] [Module S N] [Module S N₂]
606+
variable {τ₁₂ : R →+* R₂}
608607
variable (p : Submodule R M) (q : Submodule R₂ M₂)
609-
variable (pₗ : Submodule R N) (qₗ : Submodule R N₂)
608+
variable (pₗ : Submodule S N) (qₗ : Submodule S N₂)
610609

611-
theorem comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : comap fₗ qₗ ≤ comap (c • fₗ) qₗ := by
610+
theorem comap_le_comap_smul (f : M →ₛₗ[τ₁₂] M₂) (c : R₂) : comap f q ≤ comap (c • f) q := by
612611
simp only [SetLike.le_def, mem_comap, LinearMap.smul_apply]
613612
exact fun _ h ↦ smul_mem _ _ h
614613

614+
theorem map_smul_le_map [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (c : R₂) :
615+
map (c • f) p ≤ map f p := by
616+
grw [map_le_iff_le_comap, ← comap_le_comap_smul (map f p) f c, ← map_le_iff_le_comap]
617+
615618
/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
616619
the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of `Hom(M, M₂)`. -/
617-
def compatibleMaps : Submodule R (N →ₗ[R] N₂) where
620+
def compatibleMaps : Submodule S (N →ₗ[S] N₂) where
618621
carrier := { fₗ | pₗ ≤ comap fₗ qₗ }
619622
zero_mem' := by simp
620623
add_mem' {f₁ f₂} h₁ h₂ := by

‎Mathlib/Algebra/Module/Submodule/Range.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -261,6 +261,17 @@ theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} :
261261

262262
end Ring
263263

264+
section CommSemiring
265+
266+
variable [Semiring R] [CommSemiring R₂]
267+
variable [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂]
268+
variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
269+
270+
theorem range_smul_le_range (f : M →ₛₗ[τ₁₂] M₂) (c : R₂) : range (c • f) ≤ range f := by
271+
simpa only [range_eq_map] using Submodule.map_smul_le_map _ _ _
272+
273+
end CommSemiring
274+
264275
section Semifield
265276

266277
variable [Semifield K]

‎Mathlib/RingTheory/Noetherian/Basic.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,10 @@ theorem isNoetherian_of_surjective {σ : R →+* S} [RingHomSurjective σ] (f :
7575
have : (s.comap f).map f = s := Submodule.map_comap_eq_self <| hf.symm ▸ le_top
7676
this ▸ (IsNoetherian.noetherian _).map _⟩
7777

78+
instance isNoetherian_map {σ : R →+* S} [RingHomSurjective σ] {s : Submodule R M}
79+
(f : M →ₛₗ[σ] P) [IsNoetherian R s] : IsNoetherian S (Submodule.map f s) :=
80+
isNoetherian_of_surjective (f.submoduleMap s) (by simp [LinearMap.submoduleMap])
81+
7882
instance isNoetherian_range {σ : R →+* S} [RingHomSurjective σ] (f : M →ₛₗ[σ] P)
7983
[IsNoetherian R M] : IsNoetherian S (LinearMap.range f) :=
8084
isNoetherian_of_surjective _ f.range_rangeRestrict

0 commit comments

Comments
 (0)