feat(Algebra/Colimit): the directed system of finitely generated submodules

Mathlib.lean

@@ -182,6 +182,7 @@ import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.CharZero.Quotient
 import Mathlib.Algebra.Colimit.DirectLimit
+import Mathlib.Algebra.Colimit.Finiteness
 import Mathlib.Algebra.Colimit.Module
 import Mathlib.Algebra.Colimit.Ring
 import Mathlib.Algebra.ContinuedFractions.Basic

Mathlib/Algebra/Colimit/Finiteness.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2024 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Colimit.Module
+import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
+import Mathlib.RingTheory.Finiteness.Basic
+
+/-!
+# Modules as direct limits of finitely generated submodules
+
+We show that every module is the direct limit of its finitely generated submodules.
+
+As a consequence of this and the fact that tensor products preserves colimits,
+we show that if `M` and `P` are arbitrary modules and `N` is a finitely generated submodule
+of a module `P`, then two elements of `N ⊗ M` have the same image in `P ⊗ M` if and only if
+they already have the same image in `N' ⊗ M` for some finitely generated submodule `N' ≥ N`.
+This is the theorem `Submodule.FG.exists_rTensor_fg_inclusion_eq`.
+
+## Main definition
+
+* `Module.fgSystem`: the directed system of finitely generated submodules of a module.
+-/
+
+namespace Module
+
+variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- The directed system of finitely generated submodules of a module. -/
+def fgSystem (N₁ N₂ : {N : Submodule R M // N.FG}) (le : N₁ ≤ N₂) : N₁ →ₗ[R] N₂ :=
+  Submodule.inclusion le
+
+open DirectLimit
+
+namespace fgSystem
+
+instance : IsDirected {N : Submodule R M // N.FG} (· ≤ ·) where
+  directed N₁ N₂ :=
+    ⟨⟨_, N₁.2.sup N₂.2⟩, Subtype.coe_le_coe.mp le_sup_left, Subtype.coe_le_coe.mp le_sup_right⟩
+
+instance : DirectedSystem _ (fgSystem R M · · · ·) where
+  map_self _ _ := rfl
+  map_map _ _ _ _ _ _ := rfl
+
+variable [DecidableEq (Submodule R M)]
+
+open Submodule in
+/-- Every module is the direct limit of its finitely generated submodules. -/
+noncomputable def equiv : DirectLimit _ (fgSystem R M) ≃ₗ[R] M :=
+  .ofBijective (lift _ _ _ _ (fun _ ↦ Submodule.subtype _) fun _ _ _ _ ↦ rfl)
+    ⟨lift_injective _ _ fun _ ↦ Subtype.val_injective, fun x ↦
+      ⟨of _ _ _ _ ⟨_, fg_span_singleton x⟩ ⟨x, subset_span <| by rfl⟩, lift_of ..⟩⟩
+
+variable {R M}
+
+lemma equiv_comp_of (N : {N : Submodule R M // N.FG}) :
+    (equiv R M).toLinearMap ∘ₗ of _ _ _ _ N = N.1.subtype := by
+  ext; simp [equiv]
+
+end fgSystem
+
+end Module
+
+open TensorProduct
+
+variable {R M P : Type*} [CommSemiring R]
+variable [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P]
+
+theorem Submodule.FG.exists_rTensor_fg_inclusion_eq {N : Submodule R P} (hN : N.FG)
+    {x y : N ⊗[R] M} (eq : N.subtype.rTensor M x = N.subtype.rTensor M y) :
+    ∃ N', N'.FG ∧ ∃ h : N ≤ N', (N.inclusion h).rTensor M x = (N.inclusion h).rTensor M y := by
+  classical
+  lift N to {N : Submodule R P // N.FG} using hN
+  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
+  apply_fun directLimitLeft _ _ at eq
+  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
+    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
+  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
+  exact ⟨_, N'.2, le, eq⟩

Mathlib/Algebra/Colimit/Module.lean

@@ -247,16 +247,22 @@ theorem linearEquiv_symm_mk {g} : (linearEquiv _ _).symm ⟦g⟧ = of _ _ G f g.
 
 end equiv
 
-variable {G f}
+variable {G f} [DirectedSystem G (f · · ·)] [IsDirected ι (· ≤ ·)]
+
+theorem exists_eq_of_of_eq {i x y} (h : of R ι G f i x = of R ι G f i y) :
+    ∃ j hij, f i j hij x = f i j hij y := by
+  have := Nonempty.intro i
+  apply_fun linearEquiv _ _ at h
+  simp_rw [linearEquiv_of] at h
+  have ⟨j, h⟩ := Quotient.exact h
+  exact ⟨j, h.1, h.2.2⟩
 
 /-- A component that corresponds to zero in the direct limit is already zero in some
 bigger module in the directed system. -/
-theorem of.zero_exact [DirectedSystem G (f · · ·)] [IsDirected ι (· ≤ ·)]
-    {i x} (H : of R ι G f i x = 0) :
+theorem of.zero_exact {i x} (H : of R ι G f i x = 0) :
     ∃ j hij, f i j hij x = (0 : G j) := by
-  haveI : Nonempty ι := ⟨i⟩
-  apply_fun linearEquiv _ _ at H
-  rwa [map_zero, linearEquiv_of, DirectLimit.exists_eq_zero] at H
+  convert exists_eq_of_of_eq (H.trans (map_zero <| _).symm)
+  rw [map_zero]
 
 end DirectLimit
 

Mathlib/Algebra/Colimit/Ring.lean

@@ -158,7 +158,7 @@ theorem lift_unique (F : DirectLimit G f →+* P) (x) :
     F x = lift G f P (fun i ↦ F.comp <| of G f i) (fun i j hij x ↦ by simp) x := by
   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
   exact x.induction_on (by simp) (fun _ ↦ .symm <| lift_of ..)
-    (by simp +contextual) (by simp+contextual)
+    (by simp+contextual) (by simp+contextual)
 
 lemma lift_injective [Nonempty ι] [IsDirected ι (· ≤ ·)]
     (injective : ∀ i, Function.Injective <| g i) :
@@ -193,7 +193,7 @@ variable {G f'}
 bigger module in the directed system. -/
 theorem of.zero_exact {i x} (hix : of G (f' · · ·) i x = 0) :
     ∃ (j : _) (hij : i ≤ j), f' i j hij x = 0 := by
-  haveI := Nonempty.intro i
+  have := Nonempty.intro i
   apply_fun ringEquiv _ _ at hix
   rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix
 
@@ -206,7 +206,7 @@ from the components to the direct limits are injective. -/
 theorem of_injective [IsDirected ι (· ≤ ·)] [DirectedSystem G fun i j h ↦ f' i j h]
     (hf : ∀ i j hij, Function.Injective (f' i j hij)) (i) :
     Function.Injective (of G (fun i j h ↦ f' i j h) i) :=
-  haveI := Nonempty.intro i
+  have := Nonempty.intro i
   ((ringEquiv _ _).comp_injective _).mp
     fun _ _ eq ↦  DirectLimit.mk_injective f' hf _ (by simpa only [← ringEquiv_of])
 

Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean

@@ -89,6 +89,10 @@ noncomputable def directLimitLeft :
     (directLimitLeft f M).symm (of _ _ _ _ _ (g ⊗ₜ m)) = of _ _ _ f _ g ⊗ₜ m :=
   fromDirectLimit_of_tmul f g m
 
+lemma directLimitLeft_rTensor_of {i : ι} (x : G i ⊗[R] M) :
+    directLimitLeft f M (LinearMap.rTensor M (of ..) x) = of _ _ _ (f ▷ M) _ x :=
+  x.induction_on (by simp) (by simp+contextual) (by simp+contextual)
+
 /--
 `M ⊗ (limᵢ Gᵢ)` and `limᵢ (M ⊗ Gᵢ)` are isomorphic as modules
 -/
@@ -106,4 +110,18 @@ noncomputable def directLimitRight :
     (directLimitRight f M).symm (of _ _ _ _ _ (m ⊗ₜ g)) = m ⊗ₜ of _ _ _ f _ g := by
   simp [directLimitRight, congr_symm_apply_of]
 
+variable [DirectedSystem G (f · · ·)]
+
+instance : DirectedSystem (G · ⊗[R] M) (f ▷ M) where
+  map_self i x := by
+    convert LinearMap.rTensor_id_apply M (G i) x; ext; apply DirectedSystem.map_self'
+  map_map _ _ _ _ _ x := by
+    convert ← (LinearMap.rTensor_comp_apply M _ _ x).symm; ext; apply DirectedSystem.map_map' f
+
+instance : DirectedSystem (M ⊗[R] G ·) (M ◁ f) where
+  map_self i x := by
+    convert LinearMap.lTensor_id_apply M _ x; ext; apply DirectedSystem.map_self'
+  map_map _ _ _ h₁ h₂ x := by
+    convert ← (LinearMap.lTensor_comp_apply M _ _ x).symm; ext; apply DirectedSystem.map_map' f
+
 end TensorProduct