finish CompositionSeries

Mathlib/RingTheory/FiniteLength.lean

@@ -10,12 +10,13 @@ import Mathlib.RingTheory.Artinian
 # Modules of finite length
 
 We define modules of finite length (`IsFiniteLength`) to be finite iterated extensions of
-simple modules, and show that a module is of finite length iff it is both Noetherian and Artinian.
+simple modules, and show that a module is of finite length iff it is both Noetherian and Artinian,
+iff it admits a composition series.
 We do not make `IsFiniteLength` a class, instead we use `[IsNoetherian R M] [IsArtinian R M]`.
 
 ## Tag
 
-Finite length
+Finite length, Composition series
 -/
 
 universe u
@@ -38,24 +39,39 @@ theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N)
   · have := IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
     exact .of_simple_quotient (ih <| e.submoduleMap S)
 
+variable (R M) in
+theorem exists_compositionSeries_of_isNoetherian_isArtinian [IsNoetherian R M] [IsArtinian R M] :
+    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by
+  obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)
+  exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩
+
+theorem isFiniteLength_of_exists_compositionSeries
+    (h : ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤) :
+    IsFiniteLength R M :=
+  Submodule.topEquiv.isFiniteLength <| by
+    obtain ⟨s, s_head, s_last⟩ := h
+    rw [← s_last]
+    suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
+    intro i
+    induction' i using Fin.induction with i ih
+    · change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
+    let cov := s.step i
+    have := (covBy_iff_quot_is_simple cov.le).mp cov
+    have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
+      _ (Submodule.injective_subtype _)
+    rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
+    exact .of_simple_quotient (this.symm.isFiniteLength ih)
+
 theorem isFiniteLength_iff_isNoetherian_isArtinian :
     IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M :=
   ⟨fun h ↦ h.rec (fun {M} _ _ _ ↦ ⟨inferInstance, inferInstance⟩) fun M _ _ {N} _ _ ⟨_, _⟩ ↦
     ⟨(isNoetherian_iff_submodule_quotient N).mpr ⟨‹_›, isNoetherian_iff'.mpr inferInstance⟩,
       (isArtinian_iff_submodule_quotient N).mpr ⟨‹_›, inferInstance⟩⟩,
-    fun ⟨_, _⟩ ↦ Submodule.topEquiv.isFiniteLength <| by
-      obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)
-      rw [← hn.1.eq_top]
-      suffices ∀ i ≤ n, IsFiniteLength R (f i) from this n le_rfl
-      intro i hi
-      induction' i with i ih
-      · rw [f0.eq_bot]; exact .of_subsingleton
-      let cov := hn.2 i hi
-      have := (covBy_iff_quot_is_simple cov.le).mp cov
-      have := ((f i).comap (f i.succ).subtype).equivMapOfInjective _ (Submodule.injective_subtype _)
-      rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
-      exact .of_simple_quotient (this.symm.isFiniteLength <| ih <| le_of_lt hi)⟩
+    fun ⟨_, _⟩ ↦ isFiniteLength_of_exists_compositionSeries
+      (exists_compositionSeries_of_isNoetherian_isArtinian R M)⟩
 
 theorem isFiniteLength_iff_exists_compositionSeries :
-    IsFiniteLength R M ↔ ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by
-  _
+    IsFiniteLength R M ↔ ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ :=
+  ⟨fun h ↦ have ⟨_, _⟩ := isFiniteLength_iff_isNoetherian_isArtinian.mp h
+    exists_compositionSeries_of_isNoetherian_isArtinian R M,
+    isFiniteLength_of_exists_compositionSeries⟩