Nakayama.lean

1 import Mathlib.RingTheory.Jacobson.Radical
2 import Mathlib.Algebra.Module.Torsion.Basic
3 
4 /-!
5 Noncommutative Nakayama lifting, with the actual ideal-times-module submodule.
6 Only finite generation of the ambient module is used. No commutativity,
7 Noetherian, semisimplicity or finite length assumption is imposed.
8 -/
9 set_option autoImplicit false
10 
11 namespace Komorebi.PaperICompletion7.Nakayama
12 
13 universe u v
14 variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
15 
16 /-- The radical of a finitely generated module is superfluous. -/
17 theorem eq_top_of_sup_module_jacobson [Module.Finite R M]
18     (N : Submodule R M) (h : N ⊔ Module.jacobson R M = ⊤) : N = ⊤ := by
19   by_contra hn
20   obtain ⟨P, hP, hNP⟩ := (eq_top_or_exists_le_coatom N).resolve_left hn
21   have hrad : Module.jacobson R M ≤ P := sInf_le hP
22   exact hP.1 (top_unique (h ▸ sup_le hNP hrad))
23 
24 /-- Nakayama with an arbitrary left ideal contained in the ring radical. -/
25 theorem eq_top_of_sup_ideal_smul [Module.Finite R M]
26     (I : Ideal R) (hI : I ≤ Ring.jacobson R) (N : Submodule R M)
27     (h : N ⊔ I • (⊤ : Submodule R M) = ⊤) : N = ⊤ := by
28   apply eq_top_of_sup_module_jacobson N
29   apply top_unique
30   rw [← h]
31   exact sup_le_sup_left
32     ((Submodule.smul_mono_left hI).trans (Ring.jacobson_smul_top_le R M)) N
33 
34 /-- The usual Jacobson-radical specialization of noncommutative Nakayama. -/
35 theorem eq_top_of_sup_jacobson_smul [Module.Finite R M]
36     (N : Submodule R M)
37     (h : N ⊔ Ring.jacobson R • (⊤ : Submodule R M) = ⊤) : N = ⊤ :=
38   eq_top_of_sup_ideal_smul (Ring.jacobson R) le_rfl N h
39 
40 /-- The quotient by the literal ideal image. -/
41 abbrev IdealTop (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] :=
42   M ⧸ I • (⊤ : Submodule R M)
43 
44 /-- The actual quotient map, semilinear over the scalar quotient homomorphism. -/
45 def idealTopMap (I : Ideal R) [I.IsTwoSided] :
46     M →ₛₗ[Ideal.Quotient.mk I] IdealTop I M where
47   toFun := (I • (⊤ : Submodule R M)).mkQ
48   map_add' := map_add _
49   map_smul' := fun _ _ ↦ rfl
50 
51 @[simp] theorem idealTopMap_apply (I : Ideal R) [I.IsTwoSided] (x : M) :
52     idealTopMap (M := M) I x = Submodule.Quotient.mk x := rfl
53 
54 @[simp] theorem idealTopMap_smul (I : Ideal R) [I.IsTwoSided] (a : R) (x : M) :
55     idealTopMap (M := M) I (a • x) =
56       Ideal.Quotient.mk I a • idealTopMap (M := M) I x := rfl
57 
58 /-- The quotient map is surjective, on the actual quotient representatives. -/
59 theorem idealTopMap_surjective (I : Ideal R) [I.IsTwoSided] :
60     Function.Surjective (idealTopMap (M := M) I) :=
61   (I • (⊤ : Submodule R M)).mkQ_surjective
62 
63 /-- The semilinear quotient map has exactly the ideal image as its kernel. -/
64 theorem idealTopMap_ker (I : Ideal R) [I.IsTwoSided] :
65     LinearMap.ker (idealTopMap (M := M) I) = I • (⊤ : Submodule R M) := by
66   ext x
67   exact Submodule.Quotient.mk_eq_zero _
68 
69 /-- Passing to the quotient detects whether a submodule is the whole module. -/
70 theorem map_eq_top_iff [Module.Finite R M]
71     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) (N : Submodule R M) :
72     N.map (idealTopMap (M := M) I) = ⊤ ↔ N = ⊤ := by
73   constructor
74   · intro h
75     have hc := congrArg (Submodule.comap (idealTopMap (M := M) I)) h
76     rw [Submodule.comap_map_eq, Submodule.comap_top, idealTopMap_ker] at hc
77     exact eq_top_of_sup_ideal_smul I hI N hc
78   · intro h
79     rw [h, Submodule.map_top, LinearMap.range_eq_top.mpr (idealTopMap_surjective I)]
80 
81 end Komorebi.PaperICompletion7.Nakayama

Back to source controls