MoritaCornerRank110.lean

1 import PaperXI.MoritaLattice110
2 import Mathlib.NumberTheory.LocalField.Basic
3 import Mathlib.LinearAlgebra.FreeModule.PID
4 import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
5 import Mathlib.RingTheory.Localization.Module
6 
7 /-! Genuine finite/full submodules of the endomorphism ring acquire their
8 rank from the ambient field extension. No numerical index is a hypothesis. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MoritaCornerRank110
12 open Module Submodule Matrix ValuativeRel
13 open PaperXI.MoritaLattice110
14 
15 section FullSubmodule
16 variable {R K M : Type*} [CommRing R] [IsDomain R] [Field K]
17   [Algebra R K] [IsFractionRing R K] [IsPrincipalIdealRing R]
18   [AddCommGroup M] [Module R M] [Module K M] [IsScalarTower R K M]
19 
20 /-- A finite full submodule over a PID has a basis whose size is derived
21 from the dimension of its actual ambient vector space. -/
22 theorem exists_basis_full_submodule (Λ : Submodule R M) (hfg : Λ.FG)
23     (hfull : Submodule.span K (Λ : Set M) = ⊤) :
24     ∃ n : ℕ, ∃ _b : Basis (Fin n) R Λ, n = Module.finrank K M := by
25   let : Module.Finite R Λ := Module.Finite.of_fg hfg
26   let : Module.IsTorsionFree R M := Module.IsTorsionFree.of_smul_eq_zero <| by
27     intro r x h
28     have h' : algebraMap R K r • x = 0 := by simpa only [algebraMap_smul] using h
29     rcases smul_eq_zero.mp h' with hr | hx
30     · exact Or.inl (IsFractionRing.injective R K (by simpa using hr))
31     · exact Or.inr hx
32   obtain ⟨n, b⟩ := Module.basisOfFiniteTypeTorsionFree' (R := R) (M := Λ)
33   have hli : LinearIndependent R (fun i => (b i : M)) :=
34     b.linearIndependent.map' Λ.subtype (by simp)
35   have hliK : LinearIndependent K (fun i => (b i : M)) :=
36     hli.localization K (nonZeroDivisors R)
37   have hspanR : Submodule.span R (Set.range fun i => (b i : M)) = Λ := by
38     calc
39       _ = (Submodule.span R (Set.range b)).map Λ.subtype := by
40         rw [Submodule.map_span]
41         congr 1
42         ext x
43         constructor
44         · rintro ⟨i, rfl⟩
45           exact ⟨b i, ⟨i, rfl⟩, rfl⟩
46         · rintro ⟨z, ⟨i, rfl⟩, rfl⟩
47           exact ⟨i, rfl⟩
48       _ = Λ := by rw [b.span_eq, Submodule.map_top, Submodule.range_subtype]
49   have hspanK : Submodule.span K (Set.range fun i => (b i : M)) = ⊤ := by
50     rw [← Submodule.span_span_of_tower R K, hspanR, hfull]
51   let bK : Basis (Fin n) K M := Basis.mk hliK hspanK.ge
52   exact ⟨n, b, by simpa using (Module.finrank_eq_card_basis bK).symm⟩
53 
54 end FullSubmodule
55 
56 section ActualEndomorphismCorner
57 variable (F E : Type*) [Field F] [Field E] [Algebra F E]
58   [Module.Finite F E] [ValuativeRel E] [TopologicalSpace E]
59   [IsNonarchimedeanLocalField E]
60 variable {m : Type*} [Fintype m] [DecidableEq m]
61 
62 /-- Actual multiplication by extension-field integers as F-linear maps. -/
63 def coefficientMap : 𝒪[E] →+* Module.End F E :=
64   (Algebra.lmul F E).toRingHom.comp (valuation E).integer.subtype
65 
66 /-- The actual corner with its inherited left integer-ring module structure. -/
67 def cornerSubmodule (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
68     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m) :
69     Submodule 𝒪[E] (Module.End F E) where
70   __ := corner L.toAddSubgroup p
71   smul_mem' a x hx := by
72     have he : a • x = coefficientMap F E a * x := by ext v; rfl
73     rw [he]
74     exact (corner_bimodule (coefficientMap F E) L.toAddSubgroup hL p a hx).1
75 
76 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
77 /-- Entry projection identifies this corner with the image of the original
78 integer-ring submodule. -/
79 theorem cornerSubmodule_eq_map
80     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
81     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m) :
82     cornerSubmodule F E L hL p = L.map (entryLinearMap 𝒪[E] (Module.End F E) p p) := by
83   ext x
84   constructor
85   · intro hx
86     exact ⟨single p p x, hx, by simp⟩
87   · rintro ⟨z, hz, rfl⟩
88     exact entry_mem_corner (coefficientMap F E) L.toAddSubgroup hL p hz p p
89 
90 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
91 /-- Finiteness is transported from the actual whole lattice to its corner. -/
92 theorem corner_fg (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
93     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m)
94     (hfg : L.FG) : (cornerSubmodule F E L hL p).FG := by
95   rw [cornerSubmodule_eq_map]
96   exact hfg.map _
97 
98 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
99 /-- Fullness of the whole F-lattice gives fullness of the actual corner. -/
100 theorem corner_full (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
101     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m)
102     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤) :
103     Submodule.span E (cornerSubmodule F E L hL p : Set (Module.End F E)) = ⊤ := by
104   have hfullE := Submodule.span_eq_top_of_span_eq_top F E _ hfull
105   have hset : (cornerSubmodule F E L hL p : Set (Module.End F E)) =
106       (entryLinearMap E (Module.End F E) p p) '' (L : Set _) := by
107     ext x
108     constructor
109     · intro hx
110       exact ⟨single p p x, hx, by simp⟩
111     · rintro ⟨z, hz, rfl⟩
112       exact entry_mem_corner (coefficientMap F E) L.toAddSubgroup hL p hz p p
113   rw [hset, ← Submodule.map_span, hfullE, Submodule.map_top]
114   apply LinearMap.range_eq_top.mpr
115   intro x
116   exact ⟨single p p x, by simp⟩
117 
118 /-- The rank coefficient is the actual extension degree, derived from full
119 span and finite generation rather than supplied as a numerical assumption. -/
120 theorem exists_corner_basis_degree
121     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
122     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m)
123     (hfg : L.FG)
124     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤) :
125     ∃ n : ℕ, ∃ _b : Basis (Fin n) 𝒪[E] (cornerSubmodule F E L hL p),
126       n = Module.finrank F E := by
127   obtain ⟨n, b, hn⟩ := exists_basis_full_submodule (cornerSubmodule F E L hL p)
128     (corner_fg F E L hL p hfg) (corner_full F E L hL p hfull)
129   exact ⟨n, b, hn.trans (Module.finrank_linearMap_self F E E)⟩
130 
131 end ActualEndomorphismCorner
132 end PaperXI.MoritaCornerRank110

Back to source controls