feat: finitely related modules

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -53,33 +53,91 @@
 in file `Mathlib.RingTheory.FinitePresentation`.
 -/
 
+universe u v
+
 open Finsupp
 
+namespace Module
+variable {R : Type u} {M : Type v} {N : Type*}
+
 section Semiring
-variable (R M) [Semiring R] [AddCommMonoid M] [Module R M]
+variable [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- A module is finitely related if there exists a presentation of it with finitely many relations.
+
+A module is finitely presented iff it is finite and finitely related. See ???.
+-/
+class IsFinitelyRelated (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
+    Prop where
+  exists_span_eq_top_fg_ker (R M) :
+    ∃ (I : Type v) (f : I → M), Submodule.span R (.range f) = ⊤ ∧
+      (LinearMap.ker (Finsupp.linearCombination R f)).FG
+
+lemma IsFinitelyRelated.exists_set [IsFinitelyRelated R M] :
+    ∃ s : Set M, Submodule.span R s = ⊤ ∧
+      (LinearMap.ker (Finsupp.linearCombination R (Subtype.val : s → M))).FG := by
+  obtain ⟨I, f, hfspan, hfker⟩ := exists_span_eq_top_fg_ker R M
+  refine ⟨Set.range f, by simpa using hfspan, ?_⟩
+  sorry
+  -- convert hfker using 1
+
+lemma IsFinitelyRelated.of_set {s : Set M} (hsspan : Submodule.span R s = ⊤)
+    (hsker : (LinearMap.ker (Finsupp.linearCombination R (Subtype.val : s → M))).FG) :
+    IsFinitelyRelated R M := by
+  refine ⟨s, Subtype.val, by simpa using hsspan, ?_⟩
+  sorry
+
+lemma isFinitelyRelated_iff_exists_set :
+    IsFinitelyRelated R M ↔ ∃ s : Set M, Submodule.span R s = ⊤ ∧
+      (LinearMap.ker (Finsupp.linearCombination R (Subtype.val : s → M))).FG :=
+  ⟨fun _ ↦ IsFinitelyRelated.exists_set .., fun ⟨_s, hsspan, hsker⟩ ↦ .of_set hsspan hsker⟩
+
+instance Free.to_isFinitelyRelated [Free R M] : IsFinitelyRelated R M where
+  exists_span_eq_top_fg_ker := by
+    let ⟨I, b⟩ := Free.exists_basis R M
+    refine ⟨I, b, b.span_eq, ?_⟩
+    rw [← Basis.coe_repr_symm, LinearMap.ker_eq_bot_of_injective]
+    exacts [Submodule.fg_bot, b.repr.symm.injective]
 
 /--
 A module is finitely presented if it is finitely generated by some set `s`
 and the kernel of the presentation `Rˢ → M` is also finitely generated.
 -/
-class Module.FinitePresentation : Prop where
-  out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
+class FinitePresentation (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
+    Prop where
+  out (R M) : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
     (LinearMap.ker (Finsupp.linearCombination R ((↑) : s → M))).FG
 
-instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
-  obtain ⟨s, hs₁, _⟩ := h
-  exact ⟨s, hs₁⟩
+instance (priority := 100) FinitePresentation.to_isFinitelyRelated [FinitePresentation R M] :
+    IsFinitelyRelated R M where
+  exists_span_eq_top_fg_ker :=
+    let ⟨s, hs⟩ := out (R := R) (M := M); ⟨s, Subtype.val, by simpa using hs⟩
+
+instance (priority := 100) FinitePresentation.to_finite [h : FinitePresentation R M] :
+    Module.Finite R M := let ⟨s, hs₁, _⟩ := out R M; ⟨s, hs₁⟩
 
 end Semiring
 
 section Ring
+variable [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+
+/-- A finite finitely related module is finitely presented. -/
+lemma FinitePresentation.of_finite_isFinitelyRelated [Module.Finite R M] [IsFinitelyRelated R M] :
+    FinitePresentation R M := by
+  obtain ⟨I, f, hfspan, hfker⟩ := IsFinitelyRelated.exists_span_eq_top_fg_ker R M
+  have := Submodule.fg_of_fg_map_of_fg_inf_ker (s := ⊤) (f := linearCombination R f)
+    (by simp [Finsupp.range_linearCombination, hfspan, Module.Finite.fg_top]) (by simpa)
+  simp [← finite_def] at this
+  sorry
+
+/-- A module is finitely presented iff it is finite and finitely related. -/
+lemma finitePresentation_iff_finite_isFinitelyRelated :
+    FinitePresentation R M ↔ Module.Finite R M ∧ IsFinitelyRelated R M where
+  mp _ := ⟨inferInstance, inferInstance⟩
+  mpr := by rintro ⟨_, _⟩; exact .of_finite_isFinitelyRelated
 
-section
-
-universe u v
-variable (R : Type u) (M : Type*) [Ring R] [AddCommGroup M] [Module R M]
-
-theorem Module.FinitePresentation.exists_fin [fp : Module.FinitePresentation R M] :
+variable (R M) in
+theorem FinitePresentation.exists_fin [fp : FinitePresentation R M] :
     ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (_ : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG := by
   have ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp
   refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
@@ -88,33 +146,33 @@
   · simpa [range_linearCombination] using hι₁
   · simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _
 
+variable (R M) in
 /-- A finitely presented module is isomorphic to the quotient of a finite free module by a finitely
 generated submodule. -/
-theorem Module.FinitePresentation.equiv_quotient [Module.FinitePresentation R M] [Small.{v} R] :
+theorem FinitePresentation.equiv_quotient [FinitePresentation R M] [Small.{v} R] :
     ∃ (L : Type v) (_ : AddCommGroup L) (_ : Module R L) (K : Submodule R L)
       (_ : M ≃ₗ[R] L ⧸ K), Module.Free R L ∧ Module.Finite R L ∧ K.FG :=
   have ⟨_n, _K, e, fg⟩ := Module.FinitePresentation.exists_fin R M
   let es := linearEquivShrink
   ⟨_, inferInstance, inferInstance, _, e ≪≫ₗ Submodule.Quotient.equiv _ _ (es ..) rfl,
     .of_equiv (es ..), .equiv (es ..), fg.map (es ..).toLinearMap⟩
 
-end
-
-variable (R M N) [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
-
+variable (R M N) in
 -- Ideally this should be an instance but it makes mathlib much slower.
-lemma Module.finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
-    Module.FinitePresentation R M := by
+lemma FinitePresentation.of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
+    FinitePresentation R M := by
   obtain ⟨s, hs⟩ := h
   exact ⟨s, hs, IsNoetherian.noetherian _⟩
 
-lemma Module.finitePresentation_iff_finite [IsNoetherianRing R] :
-    Module.FinitePresentation R M ↔ Module.Finite R M :=
-  ⟨fun _ ↦ inferInstance, fun _ ↦ finitePresentation_of_finite R M⟩
+@[deprecated (since := "2025-04-13")]
+alias finitePresentation_of_finite := FinitePresentation.of_finite
 
-variable {R M N}
+variable (R M N) in
+lemma finitePresentation_iff_finite [IsNoetherianRing R] :
+    FinitePresentation R M ↔ Module.Finite R M :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ .of_finite R M⟩
 
-lemma Module.finitePresentation_of_free_of_surjective [Module.Free R M] [Module.Finite R M]
+lemma finitePresentation_of_free_of_surjective [Module.Free R M] [Module.Finite R M]
     (l : M →ₗ[R] N)
     (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
     Module.FinitePresentation R N := by
@@ -147,31 +205,31 @@
 
 -- Ideally this should be an instance but it makes mathlib much slower.
 variable (R M) in
-lemma Module.finitePresentation_of_projective [Projective R M] [Module.Finite R M] :
+lemma finitePresentation_of_projective [Projective R M] [Module.Finite R M] :
     FinitePresentation R M :=
   have ⟨_n, _f, _g, surj, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
-  Module.finitePresentation_of_free_of_surjective _ surj
+  finitePresentation_of_free_of_surjective _ surj
     (Finite.iff_fg.mp <| LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ inferInstance)
 
 @[deprecated (since := "2024-11-06")]
-alias Module.finitePresentation_of_free := Module.finitePresentation_of_projective
+alias finitePresentation_of_free := finitePresentation_of_projective
 
 variable {ι} [Finite ι]
 
-instance : Module.FinitePresentation R R := Module.finitePresentation_of_projective _ _
-instance : Module.FinitePresentation R (ι →₀ R) := Module.finitePresentation_of_projective _ _
-instance : Module.FinitePresentation R (ι → R) := Module.finitePresentation_of_projective _ _
+instance : FinitePresentation R R := finitePresentation_of_projective _ _
+instance : FinitePresentation R (ι →₀ R) := finitePresentation_of_projective _ _
+instance : FinitePresentation R (ι → R) := finitePresentation_of_projective _ _
 
-lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M] (l : M →ₗ[R] N)
+lemma finitePresentation_of_surjective [h : FinitePresentation R M] (l : M →ₗ[R] N)
     (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
-    Module.FinitePresentation R N := by
+    FinitePresentation R N := by
   classical
   obtain ⟨s, hs, hs'⟩ := h
   obtain ⟨t, ht⟩ := hl'
   have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
     LinearMap.range_eq_top.mp
       (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
-  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
+  apply finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
     (hl.comp H)
   choose σ hσ using (show _ from H)
   have : Finsupp.linearCombination R Subtype.val '' (σ '' t) = t := by
@@ -180,9 +238,8 @@
     ← Finset.coe_image]
   exact Submodule.FG.sup ⟨_, rfl⟩ hs'
 
-lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
-    [h : Module.FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective l) :
-    (LinearMap.ker l).FG := by
+lemma FinitePresentation.fg_ker [Module.Finite R M] [h : FinitePresentation R N] (l : M →ₗ[R] N)
+    (hl : Function.Surjective l) : (LinearMap.ker l).FG := by
   classical
   obtain ⟨s, hs, hs'⟩ := h
   have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
@@ -200,18 +257,18 @@
     exact ⟨_, hy, by simp⟩
   apply Submodule.fg_of_fg_map_of_fg_inf_ker f.range.mkQ
   · rw [this]
-    exact Module.Finite.fg_top
+    exact Finite.fg_top
   · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
     exact hs'.map f
 
-lemma Module.FinitePresentation.fg_ker_iff [Module.FinitePresentation R M]
+lemma FinitePresentation.fg_ker_iff [Module.FinitePresentation R M]
     (l : M →ₗ[R] N) (hl : Function.Surjective l) :
     Submodule.FG (LinearMap.ker l) ↔ Module.FinitePresentation R N :=
   ⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩
 
-lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
-    (l : M →ₗ[R] N) (hl : Function.Surjective l) [Module.FinitePresentation R (LinearMap.ker l)] :
-    Module.FinitePresentation R M := by
+lemma finitePresentation_of_ker [Module.FinitePresentation R N]
+    (l : M →ₗ[R] N) (hl : Function.Surjective l) [FinitePresentation R (LinearMap.ker l)] :
+    FinitePresentation R M := by
   obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG := by
     apply Submodule.fg_of_fg_map_of_fg_inf_ker l
     · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.fg_top
@@ -243,42 +300,41 @@
 
 /-- Given a split exact sequence `0 → M → N → P → 0` with `N` finitely presented,
 then `M` is also finitely presented. -/
-lemma Module.finitePresentation_of_split_exact
-    {P : Type*} [AddCommGroup P] [Module R P]
-    [Module.FinitePresentation R N]
+lemma finitePresentation_of_split_exact {P : Type*} [AddCommGroup P] [Module R P]
+    [FinitePresentation R N]
     (f : M →ₗ[R] N) (g : N →ₗ[R] P) (l : P →ₗ[R] N) (hl : g ∘ₗ l = .id)
     (hf : Function.Injective f) (H : Function.Exact f g) :
-    Module.FinitePresentation R M := by
+    FinitePresentation R M := by
   have hg : Function.Surjective g := Function.LeftInverse.surjective (DFunLike.congr_fun hl)
-  have := Module.Finite.of_surjective g hg
+  have := Finite.of_surjective g hg
   obtain ⟨e, rfl, rfl⟩ := ((Function.Exact.split_tfae' H).out 0 2 rfl rfl).mp
     ⟨hf, l, hl⟩
-  refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
+  refine finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
     (Prod.fst_surjective.comp e.surjective) ?_
   rw [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm,
     LinearMap.exact_iff.mp Function.Exact.inr_fst, ← Submodule.map_top]
   exact .map _ (.map _ (Module.Finite.fg_top))
 
 /-- Given an exact sequence `0 → M → N → P → 0`
 with `N` finitely presented and `P` projective, then `M` is also finitely presented. -/
-lemma Module.finitePresentation_of_projective_of_exact
+lemma finitePresentation_of_projective_of_exact
     {P : Type*} [AddCommGroup P] [Module R P]
-    [Module.FinitePresentation R N] [Module.Projective R P]
+    [FinitePresentation R N] [Projective R P]
     (f : M →ₗ[R] N) (g : N →ₗ[R] P)
     (hf : Function.Injective f) (hg : Function.Surjective g) (H : Function.Exact f g) :
-    Module.FinitePresentation R M :=
-  have ⟨l, hl⟩ := Module.projective_lifting_property g .id hg
-  Module.finitePresentation_of_split_exact f g l hl hf H
+    FinitePresentation R M :=
+  have ⟨l, hl⟩ := projective_lifting_property g .id hg
+  finitePresentation_of_split_exact f g l hl hf H
 
-lemma Module.FinitePresentation.of_equiv (e : M ≃ₗ[R] N) [Module.FinitePresentation R M] :
-    Module.FinitePresentation R N := by
-  simp [← Module.FinitePresentation.fg_ker_iff e.toLinearMap e.surjective, Submodule.fg_bot]
+lemma FinitePresentation.of_equiv (e : M ≃ₗ[R] N) [FinitePresentation R M] :
+    FinitePresentation R N := by
+  simp [← FinitePresentation.fg_ker_iff e.toLinearMap e.surjective, Submodule.fg_bot]
 
-lemma LinearEquiv.finitePresentation_iff (e : M ≃ₗ[R] N) :
-    Module.FinitePresentation R M ↔ Module.FinitePresentation R N :=
+lemma _root_.LinearEquiv.finitePresentation_iff (e : M ≃ₗ[R] N) :
+    FinitePresentation R M ↔ FinitePresentation R N :=
   ⟨fun _ ↦ .of_equiv e, fun _ ↦ .of_equiv e.symm⟩
 
-namespace Module.FinitePresentation
+namespace FinitePresentation
 
 variable (M) in
 instance (priority := 900) of_subsingleton [Subsingleton M] :
@@ -305,9 +361,9 @@
   · introv hN hN'
     infer_instance
 
-end Module.FinitePresentation
-
+end FinitePresentation
 end Ring
+end Module
 
 section CommRing
 

Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

@@ -245,6 +245,11 @@ theorem linearCombination_restrict (s : Set α) :
       linearCombinationOn α M R v s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap := by
   classical ext; simp [linearCombinationOn]
 
+lemma linearCombination_subtypeVal (s : Set M) :
+    linearCombination R (Subtype.val : s → M) = Submodule.subtype _ ∘ₗ
+      linearCombinationOn M M R _root_.id s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap := by
+  classical ext; simp [linearCombinationOn]
+
 theorem linearCombination_comp (f : α' → α) :
     linearCombination R (v ∘ f) = (linearCombination R v).comp (lmapDomain R R f) := by
   ext