feat: the torsion submodule of an irreducible element is semisimple (#…

…9994)

(provided the coefficients are a principal ideal ring)

Mathlib/Algebra/Module/PID.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Module.DedekindDomain
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Category.ModuleCat.Biproducts
+import Mathlib.RingTheory.SimpleModule
 
 #align_import algebra.module.pid from "leanprover-community/mathlib"@"cdc34484a07418af43daf8198beaf5c00324bca8"
 
@@ -65,6 +66,14 @@ open Submodule
 
 open UniqueFactorizationMonoid
 
+theorem Submodule.isSemisimple_torsionBy_of_irreducible {a : R} (h : Irreducible a) :
+    IsSemisimpleModule R (torsionBy R M a) := by
+  rw [IsSemisimpleModule, ← (submodule_torsionBy_orderIso a).complementedLattice_iff]
+  set I : Ideal R := R ∙ a
+  have _i2 : I.IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible h
+  let _i3 : Field (R ⧸ I) := Ideal.Quotient.field I
+  exact Module.Submodule.complementedLattice
+
 /-- A finitely generated torsion module over a PID is an internal direct sum of its
 `p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.-/
 theorem Submodule.isInternal_prime_power_torsion_of_pid [Module.Finite R M]

Mathlib/Algebra/Module/Torsion.lean

@@ -568,7 +568,7 @@ instance (I : Ideal R) {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M]
   inferInstance
 
 /-- The `a`-torsion submodule as an `(R ⧸ R∙a)`-module. -/
-instance (a : R) : Module (R ⧸ R ∙ a) (torsionBy R M a) :=
+instance instModuleQuotientTorsionBy (a : R) : Module (R ⧸ R ∙ a) (torsionBy R M a) :=
   Module.IsTorsionBySet.module <|
     (Module.isTorsionBySet_span_singleton_iff a).mpr <| torsionBy_isTorsionBy a
 
@@ -591,6 +591,19 @@ instance (a : R) {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScal
     IsScalarTower S (R ⧸ R ∙ a) (torsionBy R M a) :=
   inferInstance
 
+/-- Given an `R`-module `M` and an element `a` in `R`, submodules of the `a`-torsion submodule of
+`M` do not depend on whether we take scalars to be `R` or `R ⧸ R ∙ a`. -/
+def submodule_torsionBy_orderIso (a : R) :
+    Submodule (R ⧸ R ∙ a) (torsionBy R M a) ≃o Submodule R (torsionBy R M a) :=
+  { restrictScalarsEmbedding R (R ⧸ R ∙ a) (torsionBy R M a) with
+    invFun := fun p ↦
+      { carrier := p
+        add_mem' := add_mem
+        zero_mem' := p.zero_mem
+        smul_mem' := by rintro ⟨b⟩; exact p.smul_mem b }
+    left_inv := by intro; ext; simp [restrictScalarsEmbedding]
+    right_inv := by intro; ext; simp [restrictScalarsEmbedding] }
+
 end Submodule
 
 end NeedsGroup