Merge branch 'Raph-DG-ModuleLength' into xyzw12345_Raphel_module_length

Mathlib/Algebra/Module/Length.lean

@@ -68,15 +68,12 @@ theorem Module.length_additive {S : CategoryTheory.ShortComplex (ModuleCat R)} (
     intro rstemp rstemp'
     obtain ⟨rs, hrs⟩ := RelSeries.exists_ltSeries_ge_head_bot_last_top rstemp
     obtain ⟨rs', hrs'⟩ := RelSeries.exists_ltSeries_ge_head_bot_last_top rstemp'
-
     let gInv : RelSeries (fun (a : Submodule R S.X₂) (b : Submodule R S.X₂) => a < b) :=
       LTSeries.map rs' (Submodule.comap S.g.hom)
       (Submodule.comap_strictMono_of_surjective hS.moduleCat_surjective_g)
-
     let fIm : RelSeries (fun (a : Submodule R S.X₂) (b : Submodule R S.X₂) => a < b) :=
       LTSeries.map rs (Submodule.map S.f.hom)
       (Submodule.map_strictMono_of_injective hS.moduleCat_injective_f)
-
     have connect : fIm.last = gInv.head := by
       convert CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker hS.exact
       · simp only [RelSeries.last, LTSeries.map_length, LTSeries.map_toFun, fIm]
@@ -85,7 +82,6 @@ theorem Module.length_additive {S : CategoryTheory.ShortComplex (ModuleCat R)} (
       · simp only [RelSeries.head, LTSeries.map_toFun, gInv]
         have obv : rs'.toFun 0 = ⊥ := hrs'.2.1
         rw [obv]; exact rfl
-
     let smashfg := RelSeries.smash fIm gInv connect
     trans ↑smashfg.length
     · have this' : smashfg.length = rs.length + rs'.length := rfl
@@ -94,3 +90,40 @@ theorem Module.length_additive {S : CategoryTheory.ShortComplex (ModuleCat R)} (
       apply add_le_add
       all_goals simp only [Nat.cast_le, hrs.1, hrs'.1]
     · exact le_iSup_iff.mpr fun b a ↦ a smashfg
+
+
+theorem Module.length_additive_of_quotient {N : Submodule R M} :
+  Module.length R M = Module.length R N + Module.length R (M ⧸ N) := by
+  let quotientSeq : CategoryTheory.ShortComplex (ModuleCat R) := {
+    X₁ := ModuleCat.of R N
+    X₂ := ModuleCat.of R M
+    X₃ := ModuleCat.of R (M ⧸ N)
+    f := ModuleCat.ofHom <| Submodule.subtype N
+    g := ModuleCat.ofHom <| Submodule.mkQ N
+    zero := by
+      ext a
+      simp
+    }
+  let ex : quotientSeq.ShortExact := {
+    exact := by
+      simp[CategoryTheory.ShortComplex.moduleCat_exact_iff]
+      intro a b
+      have X2 : ↑quotientSeq.X₂ = M := rfl
+      have X1 : ↑quotientSeq.X₁ = @Subtype M fun x ↦ x ∈ N := rfl
+      let a'' : N := {
+        val := a
+        property := (Submodule.Quotient.mk_eq_zero N).mp b
+      }
+      use a''
+      aesop
+    mono_f := by
+      simp[quotientSeq]
+      have : Function.Injective (N.subtype) := by exact Submodule.injective_subtype N
+      exact (ModuleCat.mono_iff_injective (ModuleCat.ofHom N.subtype)).mpr this
+    epi_g := by
+      simp[quotientSeq]
+      have : Function.Surjective (N.mkQ) := by exact Submodule.mkQ_surjective N
+      exact (ModuleCat.epi_iff_surjective (ModuleCat.ofHom N.mkQ)).mpr this
+  }
+  have := Module.length_additive ex
+  aesop