From 1b8ed1dd99cd1c27b55a94e77838e1ffb335c438 Mon Sep 17 00:00:00 2001
From: syur2 <sif4delta0@mail.ustc.edu.cn>
Date: Sat, 19 Oct 2024 23:39:04 +0800
Subject: [PATCH] fix submodule

---
 .../MissingLemmas/Submodule.lean              | 62 ++++++++++++++++---
 ModuleLocalProperties/NoZeroSMulDivisors.lean | 30 +++------
 2 files changed, 63 insertions(+), 29 deletions(-)

diff --git a/ModuleLocalProperties/MissingLemmas/Submodule.lean b/ModuleLocalProperties/MissingLemmas/Submodule.lean
index 2543d47..3a9747b 100644
--- a/ModuleLocalProperties/MissingLemmas/Submodule.lean
+++ b/ModuleLocalProperties/MissingLemmas/Submodule.lean
@@ -4,8 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yi Song
 -/
 import Mathlib.Algebra.Module.Submodule.Localization
+import Mathlib.Algebra.Module.Torsion
 
-open Submodule IsLocalizedModule LocalizedModule Ideal
+open Submodule IsLocalizedModule LocalizedModule Ideal nonZeroDivisors
+
+section zero_mem_nonZeroDivisors
+
+lemma zero_mem_nonZeroDivisors {M : Type u_1} [MonoidWithZero M] [Subsingleton M] : 0 ∈ M⁰ :=
+  mem_nonZeroDivisors_iff.mp fun _ _ ↦ Subsingleton.eq_zero _
+
+end zero_mem_nonZeroDivisors
 
 namespace Submodule
 
@@ -16,6 +24,16 @@ variable {R M S_M : Type*} (S_R : Type*) [CommRing R] [CommRing S_R] [Algebra R
     [IsScalarTower R S_R S_M]
     (S : Submonoid R) [IsLocalization S S_R]
     (f : M →ₗ[R] S_M) [IsLocalizedModule S f]
+    {p q : Submodule R M}
+
+lemma localized'_of_trivial (h : 0 ∈ S) : localized' S_R S f p = ⊤  := by
+  apply eq_top_iff'.mpr
+  intro x
+  rw [mem_localized']
+  rcases mk'_surjective S f x with ⟨⟨m, r⟩, hmk⟩
+  rw [Function.uncurry_apply_pair] at hmk
+  refine ⟨0, ⟨Submodule.zero_mem p, ⟨⟨0, h⟩, ?_ ⟩⟩⟩
+  rw [mk'_eq_iff, map_zero, Submonoid.mk_smul, zero_smul]
 
 lemma localized'_bot : localized' S_R S f ⊥ = ⊥ := by
   have : ∃ x, x ∈ S := ⟨1, Submonoid.one_mem S⟩
@@ -35,7 +53,7 @@ lemma localized'_top : localized' S_R S f ⊤ = ⊤ := by
   use u, v
   rw [mk'_eq_iff, h]
 
-lemma localized'_sup {p q : Submodule R M} :
+lemma localized'_sup :
     localized' S_R S f (p ⊔ q) = localized' S_R S f p ⊔ localized' S_R S f q := by
   ext x
   rw [mem_localized', mem_sup]
@@ -48,7 +66,7 @@ lemma localized'_sup {p q : Submodule R M} :
     exact ⟨t • m1 + s • m2, mem_sup.mpr ⟨t • m1, smul_mem _ _ hm1, s • m2, smul_mem _ _ hm2, rfl⟩,
       ⟨s * t, by rw[← mk'_add_mk', hmk1, hmk2, hadd]⟩⟩
 
-lemma localized'_inf {p q : Submodule R M} :
+lemma localized'_inf :
     localized' S_R S f (p ⊓ q) = localized' S_R S f p ⊓ localized' S_R S f q := by
   ext x
   rw [mem_localized', mem_inf, mem_localized', mem_localized']
@@ -63,23 +81,53 @@ lemma localized'_inf {p q : Submodule R M} :
     · exact ⟨hu.symm ▸ smul_mem _ _ <| smul_mem _ _ hminp, smul_mem _ _ <| smul_mem _ _ hninq⟩
     · exact ⟨u * s * t, by rw [mul_assoc, mk'_cancel_left, mk'_cancel_left, hnmk]⟩
 
+#check span
+#check Submodule.map_span
+--this may be right when s is finite
+lemma localized'_span (s : Set M) : localized' S_R S f (span R s) = span S_R (f '' s) := by
+  ext x
+  rw [mem_localized', mem_span]
+  constructor
+  all_goals intro h
+  · intro S_p hsub
+    rcases h with ⟨m, hm, t, hmk⟩
+    rw [mem_span] at hm
+    sorry
+  ·
+    sorry
+
 end localized'_operation_commutativity
 
 section localized_operation_commutativity
 
 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
-    (S : Submonoid R)
+    (S : Submonoid R) {p q : Submodule R M}
+
+lemma localized_of_trivial (h : 0 ∈ S) : localized S p = ⊤ := localized'_of_trivial _ _ _ h
 
 lemma localized_bot : localized S (⊥ : Submodule R M) = ⊥ := localized'_bot _ _ _
 
 lemma localized_top : localized S (⊤ : Submodule R M) = ⊤ := localized'_top _ _ _
 
-lemma localized_sup {p q : Submodule R M} : localized S (p ⊔ q) = localized S p ⊔ localized S q :=
+lemma localized_sup : localized S (p ⊔ q) = localized S p ⊔ localized S q :=
   localized'_sup _ _ _
 
-lemma localized_inf {p q : Submodule R M} : localized S (p ⊓ q) = localized S p ⊓ localized S q :=
+lemma localized_inf : localized S (p ⊓ q) = localized S p ⊓ localized S q :=
   localized'_inf _ _ _
 
+end localized_operation_commutativity
+
+section torsion
 
+lemma torsion_of_subsingleton {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
+    (h : Subsingleton R) : torsion R M = ⊤ :=
+  eq_top_iff'.mpr <| fun x ↦ (mem_torsion_iff x).mp
+  ⟨⟨0, zero_mem_nonZeroDivisors⟩, by rw [Submonoid.mk_smul, zero_smul]⟩
 
-end localized_operation_commutativity
+end torsion
+
+section annihilator
+
+
+
+end annihilator
diff --git a/ModuleLocalProperties/NoZeroSMulDivisors.lean b/ModuleLocalProperties/NoZeroSMulDivisors.lean
index 3621de2..5ba96bf 100644
--- a/ModuleLocalProperties/NoZeroSMulDivisors.lean
+++ b/ModuleLocalProperties/NoZeroSMulDivisors.lean
@@ -3,14 +3,15 @@ Copyright (c) 2024 Yi Song. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yi Song
 -/
-import Mathlib.Algebra.Module.Submodule.Localization
-import Mathlib.Algebra.Module.Torsion
+
 import ModuleLocalProperties.Basic
 
 import ModuleLocalProperties.MissingLemmas.LocalizedModule
 
 open Submodule LocalizedModule IsLocalizedModule LinearMap nonZeroDivisors
 
+set_option linter.unusedVariables false
+
 section missinglemma
 
 lemma IsLocalization.mem_map_nonZeroDivisors {R : Type*} [CommSemiring R] (S : Submonoid R)
@@ -29,25 +30,6 @@ lemma Localization.mk_mem_nonZeroDivisors {R : Type*} [CommRing R] (S : Submonoi
   haveI := OreLocalization.nontrivial_iff.mpr nontrival
   exact IsLocalization.ne_zero_of_mk'_ne_zero <| mk_eq_mk' (R := R) ▸ nonZeroDivisors.ne_zero h
 
-lemma zero_mem_nonZeroDivisors {M : Type u_1} [MonoidWithZero M] [Subsingleton M] : 0 ∈ M⁰ :=
-  mem_nonZeroDivisors_iff.mp fun _ _ ↦ Subsingleton.eq_zero _
-
-lemma Submodule.torsion_of_subsingleton {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
-    (h : Subsingleton R) : torsion R M = ⊤ :=
-  eq_top_iff'.mpr <| fun x ↦ (mem_torsion_iff x).mp
-  ⟨⟨0, zero_mem_nonZeroDivisors⟩, by rw [Submonoid.mk_smul, zero_smul]⟩
-
-lemma Submodule.loclized_of_trivial {R M : Type*} [CommRing R] (S : Submonoid R) [AddCommGroup M]
-    [Module R M] {p : Submodule R M} (trivial : 0 ∈ S) : localized S p = ⊤ := by
-  apply eq_top_iff'.mpr
-  intro x
-  rw [mem_localized']
-  induction' x with m s
-  refine ⟨0, ⟨Submodule.zero_mem p, ⟨⟨0, trivial⟩, ?_⟩⟩⟩
-  rw [← mk_eq_mk',mk_eq]
-  use ⟨0, trivial⟩
-  simp only [smul_zero, Submonoid.mk_smul, zero_smul]
-
 end missinglemma
 
 section localized_torsion_commutivity
@@ -94,7 +76,7 @@ lemma localized_torsion_nontrival_ge [IsDomain R] (nontrivial : 0 ∉ S) :
 lemma localized_torsion_trival [IsDomain R] (trivial : 0 ∈ S) :
     localized S (torsion R M) = torsion (Localization S) (LocalizedModule S M) :=
   (torsion_of_subsingleton (M := LocalizedModule S M) <|
-  OreLocalization.subsingleton_iff.mpr trivial) ▸ loclized_of_trivial S trivial
+  OreLocalization.subsingleton_iff.mpr trivial) ▸ localized_of_trivial S trivial
 
 lemma localized_torsion [IsDomain R] :
     localized S (torsion R M) = torsion (Localization S) (LocalizedModule S M) := by
@@ -124,3 +106,7 @@ lemma noZeroSMulDivisors_of_localization_iff :
   fun h ↦ noZeroSMulDivisors_of_localization M h⟩
 
 end NoZeroSMulDivisors_local_property
+
+section annihilator
+
+end annihilator