Linear maps into Noetherian modules

Let A be a semiring and R a ring acting on an A-module M through A-linear maps. If P is finitely generated over A and M is Noetherian over R, then the R-module Hom_A(P, M) is Noetherian, hence finitely generated: a surjection A ^ n → P embeds it in M ^ n (TauCeti.isNoetherian_linearMap_of_finite). In particular, this applies when R is a Noetherian ring and M is finitely generated over R. For example, for a finite group G the ℤ_p-module of ℤ_p[G]-linear maps between finitely generated ℤ_p[G]-modules is finitely generated. No freeness or projectivity is assumed, unlike Mathlib's Module.Finite.linearMap, and A need not be commutative, unlike Mathlib's isNoetherian_linearMap.

For any indexed family v : ι → M in a Noetherian R-module M, finitely many indices already generate the full R-linear span of the family (TauCeti.exists_finset_span_image_eq).

When R is a commutative ring, N is a finitely generated R-module, and M is a Noetherian R-module, N →ₗ[R] M is itself Noetherian (isNoetherian_linearMap). Applying finite-index span stabilization to a family φ : ι → N →ₗ[R] M shows that the joint kernel of the whole family already equals the joint kernel of finitely many of its members (TauCeti.exists_finset_iInf_ker_eq). In particular, if the family separates points of N, a finite subfamily already separates points of N (TauCeti.exists_finset_eq_zero_of_forall_apply_eq_zero), and on any finitely generated submodule P of a product ι → M into a Noetherian module, vanishing at a fixed finite set of coordinates forces vanishing everywhere (Submodule.exists_finset_eq_zero_of_apply_eq_zero). Commutativity of R is essential: over the first Weyl algebra A₁(k) in characteristic zero, k[t] is a simple (hence Noetherian) left module while the evaluation maps P ↦ P(tⁿ) on the cyclic module A₁(k) have trivial common kernel with every finite subintersection nonzero.

References

• K. Buzzard, Eigenvarieties, in L-functions and Galois representations, London Math. Soc. Lecture Note Ser. 320 (2007), Lemma 2.2.

theorem TauCeti.exists_finset_span_image_eq (R : Type u_1) {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (v : ι → M) : ∃ (S : Finset ι), Submodule.span R (v '' ↑S) = Submodule.span R (Set.range v)

In a Noetherian module, the span of the range of an indexed family equals the span of its image on some finite set of indices.

instance TauCeti.isNoetherian_linearMap_of_finite {R : Type u_1} {A : Type u_2} {P : Type u_3} {M : Type u_4} [Ring R] [Semiring A] [AddCommMonoid P] [Module A P] [AddCommGroup M] [Module A M] [Module R M] [SMulCommClass A R M] [Module.Finite A P] [IsNoetherian R M] : IsNoetherian R (P →ₗ[A] M)

For P finitely generated over a semiring A and M Noetherian over a ring R whose action commutes with A, the R-module of A-linear maps P → M is Noetherian.

theorem TauCeti.exists_finset_iInf_ker_eq {R : Type u_1} {N : Type u_2} {M : Type u_3} {ι : Type u_4} [CommRing R] [AddCommGroup N] [AddCommGroup M] [Module R N] [Module R M] [Module.Finite R N] [IsNoetherian R M] (φ : ι → N →ₗ[R] M) : ∃ (S : Finset ι), ⨅ i ∈ S, (φ i).ker = ⨅ (i : ι), (φ i).ker

Joint-kernel stabilization: for an indexed family of linear maps out of a finitely generated module into a Noetherian module over a commutative ring, the intersection of all kernels equals the intersection over a finite subset of indices (Buzzard, Eigenvarieties, Lemma 2.2).

theorem TauCeti.exists_finset_eq_zero_of_forall_apply_eq_zero {R : Type u_1} {N : Type u_2} {M : Type u_3} {ι : Type u_4} [CommRing R] [AddCommGroup N] [AddCommGroup M] [Module R N] [Module R M] [Module.Finite R N] [IsNoetherian R M] (φ : ι → N →ₗ[R] M) (hsep : ∀ (x : N), (∀ (i : ι), (φ i) x = 0) → x = 0) : ∃ (S : Finset ι), ∀ (x : N), (∀ i ∈ S, (φ i) x = 0) → x = 0

If a family of linear maps out of a finitely generated module into a Noetherian module over a commutative ring separates points, some finite subfamily already separates points.

theorem Submodule.exists_finset_eq_zero_of_apply_eq_zero {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (P : Submodule R (ι → M)) [Module.Finite R ↥P] : ∃ (S : Finset ι), ∀ f ∈ P, (∀ i ∈ S, f i = 0) → f = 0

Finite-coordinate detection (Buzzard, Eigenvarieties, Lemma 2.2): on a finitely generated submodule of a product of copies of a Noetherian module over a commutative ring, some finite set of coordinates detects zero.