ModuleTop.lean

1 import PaperICompletion7.Nakayama
2 import KomorebiVerification.SeedRankBasics
3 
4 /-!
5 Generator lifting and equality of the existing canonical seed ranks. The
6 quotient is the literal M / IM and the scalar ring is the literal R / I.
7 No semisimplicity of the quotient ring is assumed.
8 -/
9 set_option autoImplicit false
10 
11 namespace Komorebi.PaperICompletion7.ModuleTop
12 
13 open Komorebi.SeedRankBasics
14 open Komorebi.PaperICompletion7.Nakayama
15 
16 universe u v w
17 variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
18 
19 /-- A set generates exactly when its image generates modulo a radical ideal. -/
20 theorem image_generates_iff [Module.Finite R M]
21     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) (s : Set M) :
22     Generates (R ⧸ I) (IdealTop I M) (idealTopMap I '' s) ↔ Generates R M s := by
23   simpa only [Generates, Submodule.map_span] using
24     map_eq_top_iff I hI (Submodule.span R s)
25 
26 /-- The generating-family statement keeps exactly the original index set. -/
27 theorem family_generates_iff [Module.Finite R M]
28     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R)
29     {ι : Type w} (x : ι → M) :
30     FamilyGenerates (R ⧸ I) (IdealTop I M) (idealTopMap I ∘ x) ↔
31       FamilyGenerates R M x := by
32   simpa only [FamilyGenerates, Set.range_comp] using
33     image_generates_iff I hI (Set.range x)
34 
35 /-- Any choice of lifts of a generating quotient family generates upstairs. -/
36 theorem lifts_generate [Module.Finite R M]
37     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R)
38     {ι : Type w} (x : ι → IdealTop I M) (y : ι → M)
39     (hxy : ∀ i, idealTopMap I (y i) = x i)
40     (hx : FamilyGenerates (R ⧸ I) (IdealTop I M) x) :
41     FamilyGenerates R M y := by
42   apply (family_generates_iff I hI y).mp
43   have heq : idealTopMap I ∘ y = x := funext hxy
44   rwa [heq]
45 
46 /-- Both inequalities for the canonical cardinal minimum are proved. -/
47 theorem seedRank_eq_idealTop [Module.Finite R M]
48     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) :
49     seedRank R M = seedRank (R ⧸ I) (IdealTop I M) := by
50   classical
51   let f := idealTopMap (M := M) I
52   apply le_antisymm
53   · obtain ⟨s, hs, hcard⟩ := exists_generating_set_card_eq_seedRank
54       (R ⧸ I) (IdealTop I M)
55     let g : IdealTop I M → M := fun y ↦ Classical.choose (idealTopMap_surjective I y)
56     have hg (y : IdealTop I M) : f (g y) = y :=
57       Classical.choose_spec (idealTopMap_surjective I y)
58     have himage : f '' (g '' s) = s := by
59       ext y
60       constructor
61       · rintro ⟨x, ⟨z, hz, rfl⟩, rfl⟩
62         rwa [hg]
63       · intro hy
64         exact ⟨g y, ⟨y, hy, rfl⟩, hg y⟩
65     have hlift : Generates R M (g '' s) :=
66       (image_generates_iff I hI _).mp (by
67         change Generates (R ⧸ I) (IdealTop I M) (f '' (g '' s))
68         rw [himage]
69         exact hs)
70     calc
71       seedRank R M ≤ Cardinal.mk (g '' s) := seedRank_le_mk_of_generates R M hlift
72       _ ≤ Cardinal.mk s := Cardinal.mk_image_le
73       _ = seedRank (R ⧸ I) (IdealTop I M) := hcard
74   · obtain ⟨s, hs, hcard⟩ := exists_generating_set_card_eq_seedRank R M
75     have himage := (image_generates_iff I hI s).mpr hs
76     calc
77       seedRank (R ⧸ I) (IdealTop I M) ≤ Cardinal.mk (f '' s) :=
78         seedRank_le_mk_of_generates (R ⧸ I) (IdealTop I M) himage
79       _ ≤ Cardinal.mk s := Cardinal.mk_image_le
80       _ = seedRank R M := hcard
81 
82 /-- The natural-valued minimum agrees too, for the existing definitions. -/
83 theorem seedFinrank_eq_idealTop [Module.Finite R M]
84     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) :
85     seedFinrank R M = seedFinrank (R ⧸ I) (IdealTop I M) :=
86   congrArg Cardinal.toNat (seedRank_eq_idealTop I hI)
87 
88 /-- The quotient module over the quotient ring is genuinely finitely generated. -/
89 theorem idealTop_finite [Module.Finite R M]
90     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) :
91     Module.Finite (R ⧸ I) (IdealTop I M) := by
92   apply (seedRank_lt_aleph0_iff (R ⧸ I) (IdealTop I M)).mp
93   rw [← seedRank_eq_idealTop I hI]
94   exact (seedRank_lt_aleph0_iff R M).mpr inferInstance
95 
96 /-- The module top, without a semisimplicity assumption. -/
97 abbrev RadicalTop (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] :=
98   IdealTop (Ring.jacobson R) M
99 
100 /-- Manuscript-facing generator lifting modulo the Jacobson radical. -/
101 theorem generates_iff_radicalTop [Module.Finite R M] (s : Set M) :
102     Generates R M s ↔
103       Generates (R ⧸ Ring.jacobson R) (RadicalTop R M)
104         (idealTopMap (Ring.jacobson R) '' s) :=
105   (image_generates_iff (Ring.jacobson R) le_rfl s).symm
106 
107 /-- The printed cardinal seed-rank equality over an arbitrary unital ring. -/
108 theorem seedRank_eq_radicalTop [Module.Finite R M] :
109     seedRank R M = seedRank (R ⧸ Ring.jacobson R) (RadicalTop R M) :=
110   seedRank_eq_idealTop (Ring.jacobson R) le_rfl
111 
112 /-- Natural minimum version of the module-top equality. -/
113 theorem seedFinrank_eq_radicalTop [Module.Finite R M] :
114     seedFinrank R M = seedFinrank (R ⧸ Ring.jacobson R) (RadicalTop R M) :=
115   seedFinrank_eq_idealTop (Ring.jacobson R) le_rfl
116 
117 /-- Any lifts of a quotient basis generate over the original ring. -/
118 theorem quotient_basis_lifts_generate [Module.Finite R M]
119     (I : Ideal R) [I.IsTwoSided] (hI : I ≤ Ring.jacobson R) {ι : Type w}
120     (b : Module.Basis ι (R ⧸ I) (IdealTop I M)) (x : ι → M)
121     (hx : ∀ i, idealTopMap I (x i) = b i) : FamilyGenerates R M x :=
122   lifts_generate I hI b x hx b.span_eq
123 
124 end Komorebi.PaperICompletion7.ModuleTop

Back to source controls