feat: Hom(N, M) is Noetherian when M is Noetherian and N is fin…

…itely-generated. (#7276)





Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Module/LinearMap.lean

@@ -576,14 +576,24 @@ theorem comp_assoc
 
 variable {f g} {f' : M₂ →ₛₗ[σ₂₃] M₃} {g' : M₁ →ₛₗ[σ₁₂] M₂}
 
+/-- The linear map version of `Function.Surjective.injective_comp_right` -/
+lemma _root_.Function.Surjective.injective_linearMapComp_right (hg : Surjective g) :
+    Injective fun f : M₂ →ₛₗ[σ₂₃] M₃ ↦ f.comp g :=
+  fun _ _ h ↦ ext <| hg.forall.2 (ext_iff.1 h)
+
 @[simp]
-theorem cancel_right (hg : Function.Surjective g) : f.comp g = f'.comp g ↔ f = f' :=
-  ⟨fun h ↦ ext <| hg.forall.2 (ext_iff.1 h), fun h ↦ h ▸ rfl⟩
+theorem cancel_right (hg : Surjective g) : f.comp g = f'.comp g ↔ f = f' :=
+  hg.injective_linearMapComp_right.eq_iff
 #align linear_map.cancel_right LinearMap.cancel_right
 
+/-- The linear map version of `Function.Injective.comp_left` -/
+lemma _root_.Function.Injective.injective_linearMapComp_left (hf : Injective f) :
+    Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g :=
+  fun g₁ g₂ (h : f.comp g₁ = f.comp g₂) ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply]
+
 @[simp]
-theorem cancel_left (hf : Function.Injective f) : f.comp g = f.comp g' ↔ g = g' :=
-  ⟨fun h ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply], fun h ↦ h ▸ rfl⟩
+theorem cancel_left (hf : Injective f) : f.comp g = f.comp g' ↔ g = g' :=
+  hf.injective_linearMapComp_left.eq_iff
 #align linear_map.cancel_left LinearMap.cancel_left
 
 end

Mathlib/LinearAlgebra/Basis.lean

@@ -649,7 +649,7 @@ theorem constr_self (f : M →ₗ[R] M') : (constr (M' := M') b S fun i => f (b
   b.constr_eq S fun _ => rfl
 #align basis.constr_self Basis.constr_self
 
-theorem constr_range [Nonempty ι] {f : ι → M'} :
+theorem constr_range {f : ι → M'} :
     LinearMap.range (constr (M' := M') b S f) = span R (range f) := by
   rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
     Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -30,7 +30,6 @@ commuting actions, and `ρ₁₂ : R →+* R₂` and `σ₁₂ : S →+* S₂`.
 bilinear
 -/
 
-
 namespace LinearMap
 
 section Semiring

Mathlib/LinearAlgebra/Finsupp.lean

@@ -471,10 +471,11 @@ theorem supported_comap_lmapDomain (f : α → α') (s : Set α') :
   exact Set.Subset.trans mapDomain_support hl
 #align finsupp.supported_comap_lmap_domain Finsupp.supported_comap_lmapDomain
 
-theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) :
+theorem lmapDomain_supported (f : α → α') (s : Set α) :
     (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := by
   classical
-  inhabit α
+  cases isEmpty_or_nonempty α
+  · simp [s.eq_empty_of_isEmpty]
   refine
     le_antisymm
       (map_le_iff_le_comap.2 <|

Mathlib/LinearAlgebra/StdBasis.lean

@@ -35,7 +35,7 @@ this is a basis over `Fin 3 → R`.
 -/
 
 
-open Function Submodule
+open Function Set Submodule
 
 open BigOperators
 
@@ -297,6 +297,29 @@ end Module
 
 end Pi
 
+namespace Module
+
+variable (ι R M N : Type*) [Fintype ι] [CommSemiring R]
+  [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N]
+
+/-- The natural linear equivalence: `Mⁱ ≃ Hom(Rⁱ, M)` for an `R`-module `M`. -/
+noncomputable def piEquiv : (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M) := Basis.constr (Pi.basisFun R ι) R
+
+lemma piEquiv_apply_apply (v : ι → M) (w : ι → R) :
+    piEquiv ι R M v w = ∑ i, w i • v i := by
+  simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]
+  congr
+
+@[simp] lemma range_piEquiv (v : ι → M) :
+    LinearMap.range (piEquiv ι R M v) = span R (range v) :=
+  Basis.constr_range _ _
+
+@[simp] lemma surjective_piEquiv_apply_iff (v : ι → M) :
+    Surjective (piEquiv ι R M v) ↔ span R (range v) = ⊤ := by
+  rw [← LinearMap.range_eq_top, range_piEquiv]
+
+end Module
+
 namespace Matrix
 
 variable (R : Type*) (m n : Type*) [Fintype m] [Fintype n] [Semiring R]

Mathlib/RingTheory/Finiteness.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.RingTheory.Ideal.Operations
 
@@ -550,10 +551,16 @@ theorem iff_addGroup_fg {G : Type*} [AddCommGroup G] : Module.Finite ℤ G ↔ A
 
 variable {R M N}
 
+/-- See also `Module.Finite.exists_fin'`. -/
 theorem exists_fin [Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (range s) = ⊤ :=
   Submodule.fg_iff_exists_fin_generating_family.mp out
 #align module.finite.exists_fin Module.Finite.exists_fin
 
+lemma exists_fin' (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] [Finite R M] :
+    ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f := by
+  have ⟨n, s, hs⟩ := exists_fin (R := R) (M := M)
+  exact ⟨n, piEquiv (Fin n) R M s, by simpa⟩
+
 theorem of_surjective [hM : Finite R M] (f : M →ₗ[R] N) (hf : Surjective f) : Finite R N :=
   ⟨by
     rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top]

Mathlib/RingTheory/Noetherian.lean

@@ -286,6 +286,21 @@ instance isNoetherian_pi' {R ι M : Type*} [Ring R] [AddCommGroup M] [Module R M
 
 end
 
+section CommRing
+
+variable (R M N : Type*) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+  [IsNoetherian R M] [Module.Finite R N]
+
+instance isNoetherian_linearMap_pi {ι : Type*} [Finite ι] : IsNoetherian R ((ι → R) →ₗ[R] M) :=
+  let _i : Fintype ι := Fintype.ofFinite ι; isNoetherian_of_linearEquiv (Module.piEquiv ι R M)
+
+instance isNoetherian_linearMap : IsNoetherian R (N →ₗ[R] M) := by
+  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N
+  let g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M := (LinearMap.llcomp R (Fin n → R) N M).flip f
+  exact isNoetherian_of_injective g hf.injective_linearMapComp_right
+
+end CommRing
+
 open IsNoetherian Submodule Function
 
 section