RegularMultiplicity.lean

1 import PaperICompletion8.DivisionProduct
2 import Mathlib.Algebra.DirectSum.Module
3 import Mathlib.RingTheory.SimpleModule.Basic
4 
5 /-! Literal natural modules, column decompositions, and regular multiplicities.
6 The matrices act on the LEFT. Taking columns is an A-linear rearrangement of
7 coordinates, not the false assertion that transpose preserves multiplication. -/
8 set_option autoImplicit false
9 set_option linter.unusedSectionVars false
10 
11 namespace Komorebi.PaperICompletion8.RegularMultiplicity
12 
13 open scoped BigOperators DirectSum
14 open Komorebi.SeedRankBasics Komorebi.SeedRankOperations
15 open Komorebi.PaperICompletion8.DivisionProduct
16 
17 universe u v
18 
19 section Natural
20 variable {D : Type u} [DivisionRing D]
21 variable {n : ℕ}
22 
23 /-- A nonzero vector generates the natural module over a division ring. -/
24 theorem natural_nonzero_generates {x : Fin n → D} (hx : x ≠ 0) :
25     Generates (Matrix (Fin n) (Fin n) D) (Fin n → D) {x} := by
26   rw [generates_singleton_iff_surjective]
27   obtain ⟨j, hj⟩ : ∃ j, x j ≠ 0 := by
28     by_contra h
29     apply hx
30     funext i
31     by_contra hi
32     exact h ⟨i, hi⟩
33   intro y
34   let A : Matrix (Fin n) (Fin n) D := fun i k ↦ if k = j then y i / x j else 0
35   refine ⟨A, ?_⟩
36   funext i
37   change (Matrix.mulVec A x) i = y i
38   simp [A, Matrix.mulVec, dotProduct, hj]
39 
40 /-- The exact canonical seed rank on a positive-dimensional natural module. -/
41 theorem natural_seedRank_eq_one (hn : 0 < n) :
42     seedRank (Matrix (Fin n) (Fin n) D) (Fin n → D) = 1 := by
43   classical
44   let : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
45   let x : Fin n → D := Pi.single ⟨0, hn⟩ 1
46   have hx : x ≠ 0 := by
47     intro h
48     have hh := congrFun h ⟨0, hn⟩
49     simp [x] at hh
50   have hsurj := (generates_singleton_iff_surjective _ _ x).mp (natural_nonzero_generates hx)
51   let : Module.Finite (Matrix (Fin n) (Fin n) D) (Fin n → D) :=
52     Module.Finite.of_surjective (oneSeedMap _ _ x) hsurj
53   exact (seedRank_eq_one_iff_cyclic _ _).mpr ⟨x, natural_nonzero_generates hx⟩
54 
55 section SingleMultiplicity
56 variable (d m : ℕ)
57 local instance (priority := 100) singleBlockAction :
58     Module (Matrix (Fin d) (Fin d) D) (Matrix (Fin d) (Fin m) D) :=
59   Matrix.Module.matrixModule
60 
61 /-- A single rectangular multiplicity block is its family of natural columns. -/
62 def singleColumnsEquiv :
63     Matrix (Fin d) (Fin m) D ≃ₗ[Matrix (Fin d) (Fin d) D]
64       (Fin m → Fin d → D) where
65   toFun a j i := a i j
66   invFun x i j := x j i
67   left_inv _ := rfl
68   right_inv _ := rfl
69   map_add' _ _ := rfl
70   map_smul' a x := by
71     funext j i
72     change (∑ s, a i s • x s) j = ∑ s, a i s * x s j
73     simp
74 
75 /-- Literal multiplicity formula for finite copies of a division-ring natural module. -/
76 theorem naturalCopies_seedRank (hd : 0 < d) :
77     seedRank (Matrix (Fin d) (Fin d) D) (Fin m → Fin d → D) =
78       ((m ⌈/⌉ d : ℕ) : Cardinal) := by
79   rw [← seedRank_linearEquiv (singleColumnsEquiv (D := D) d m)]
80   exact Komorebi.PaperICompletion8.DivisionBlock.oneBlock_seedRank_eq_ceilDiv hd
81 
82 /-- The same exact formula with the printed finite direct sum rather than a product. -/
83 theorem naturalDirectSum_seedRank (hd : 0 < d) :
84     seedRank (Matrix (Fin d) (Fin d) D) (⨁ _ : Fin m, (Fin d → D)) =
85       ((m ⌈/⌉ d : ℕ) : Cardinal) := by
86   rw [seedRank_linearEquiv (DirectSum.linearEquivFunOnFintype
87     (Matrix (Fin d) (Fin d) D) (Fin m) (fun _ ↦ Fin d → D))]
88   exact naturalCopies_seedRank d m hd
89 
90 end SingleMultiplicity
91 
92 end Natural
93 
94 section Product
95 variable {I : Type v} [Fintype I] [DecidableEq I]
96 variable {D : I → Type u} [∀ i, DivisionRing (D i)]
97 variable (d m : I → ℕ)
98 
99 /-- The natural module of factor i, inflated along the actual coordinate projection. -/
100 abbrev Simple (i : I) := Fin (d i) → D i
101 
102 /-- Scalar restriction along the coordinate ring homomorphism, not a central action. -/
103 scoped instance simpleModule (i : I) :
104     Module (DivisionProductAlgebra (D := D) d) (Simple (D := D) d i) :=
105   Module.compHom (Simple (D := D) d i)
106     (Pi.evalRingHom (fun j ↦ Matrix (Fin (d j)) (Fin (d j)) (D j)) i)
107 
108 /-- The scalar action selects exactly the ith matrix factor. -/
109 theorem simple_smul (a : DivisionProductAlgebra (D := D) d)
110     (i : I) (x : Simple (D := D) d i) : a • x = Matrix.mulVec (a i) x := rfl
111 
112 /-- The literal product of multiplicity copies of natural modules. -/
113 abbrev MultiplicityModule := ∀ i : I, Fin (m i) → Simple (D := D) d i
114 
115 /-- Every nonzero vector of an inflated simple factor generates it. -/
116 theorem simple_nonzero_generates (i : I) {x : Simple (D := D) d i} (hx : x ≠ 0) :
117     Generates (DivisionProductAlgebra (D := D) d) (Simple (D := D) d i) {x} := by
118   rw [generates_singleton_iff_surjective]
119   have h := (generates_singleton_iff_surjective _ _ x).mp (natural_nonzero_generates hx)
120   intro y
121   obtain ⟨a, ha⟩ := h y
122   refine ⟨Pi.single i a, ?_⟩
123   simpa only [oneSeedMap_apply, simple_smul, Pi.single_eq_same, Matrix.smul_eq_mulVec] using ha
124 
125 /-- The inflated natural module is genuinely simple when its matrix size is positive. -/
126 theorem simple_isSimple (i : I) (hd : 0 < d i) :
127     IsSimpleModule (DivisionProductAlgebra (D := D) d) (Simple (D := D) d i) := by
128   let : Nonempty (Fin (d i)) := ⟨⟨0, hd⟩⟩
129   apply isSimpleModule_iff_toSpanSingleton_surjective.mpr
130   refine ⟨inferInstance, ?_⟩
131   intro x hx
132   exact (generates_singleton_iff_surjective _ _ x).mp (simple_nonzero_generates d i hx)
133 
134 /-- Other product factors act by zero on the ith simple module. -/
135 theorem other_factor_smul_zero (i j : I) (hji : j ≠ i)
136     (a : Matrix (Fin (d j)) (Fin (d j)) (D j)) (x : Simple (D := D) d i) :
137     (Pi.single j a : DivisionProductAlgebra (D := D) d) • x = 0 := by
138   rw [simple_smul]
139   simp [Pi.single_eq_of_ne hji.symm]
140 
141 /-- Regular matrix-ring coordinates are literally its columns. -/
142 def regularColumnsEquiv :
143     DivisionProductAlgebra (D := D) d ≃ₗ[DivisionProductAlgebra (D := D) d]
144       MultiplicityModule (D := D) d d where
145   toFun a i j r := a i r j
146   invFun x i r j := x i j r
147   left_inv _ := rfl
148   right_inv _ := rfl
149   map_add' _ _ := rfl
150   map_smul' a b := by
151     funext i j r
152     change (a i * b i) r j = (Matrix.mulVec (a i) (fun s ↦ b i s j)) r
153     rfl
154 
155 /-- The regular equivalence is a column rearrangement on every entry. -/
156 theorem regularColumnsEquiv_apply (a : DivisionProductAlgebra (D := D) d)
157     (i : I) (j r : Fin (d i)) : regularColumnsEquiv d a i j r = a i r j := rfl
158 
159 /-- The product-to-finite-direct-sum equivalence keeps the inflated actions. -/
160 noncomputable def multiplicityDirectSumEquiv :
161     MultiplicityModule (D := D) d m ≃ₗ[DivisionProductAlgebra (D := D) d]
162       ⨁ i : I, (Fin (m i) → Simple (D := D) d i) :=
163   (DirectSum.linearEquivFunOnFintype (DivisionProductAlgebra (D := D) d) I
164     (fun i ↦ Fin (m i) → Simple (D := D) d i)).symm
165 
166 /-- The printed regular-module multiplicity equivalence over arbitrary division rings. -/
167 noncomputable def regularDirectSumEquiv :
168     DivisionProductAlgebra (D := D) d ≃ₗ[DivisionProductAlgebra (D := D) d]
169       ⨁ i : I, (Fin (d i) → Simple (D := D) d i) :=
170   (regularColumnsEquiv d).trans (multiplicityDirectSumEquiv d d)
171 
172 section Rectangular
173 local instance (priority := 100) blockModuleAction (i : I) :
174     Module (Matrix (Fin (d i)) (Fin (d i)) (D i))
175       (Matrix (Fin (d i)) (Fin (m i)) (D i)) := Matrix.Module.matrixModule
176 
177 /-- Rectangular matrices are the literal multiplicity copies by columns. -/
178 def columnsEquiv :
179     DivisionProductModule (D := D) d m ≃ₗ[DivisionProductAlgebra (D := D) d]
180       MultiplicityModule (D := D) d m where
181   toFun a i j r := a i r j
182   invFun x i r j := x i j r
183   left_inv _ := rfl
184   right_inv _ := rfl
185   map_add' _ _ := rfl
186   map_smul' a x := by
187     funext i j r
188     change (∑ s, a i r s • x i s) j = ∑ s, a i r s * x i s j
189     simp
190 
191 /-- The multiplicity seed formula is about natural-module copies, not just a matrix alias. -/
192 theorem multiplicity_seedRank (hd : ∀ i, 0 < d i) :
193     seedRank (DivisionProductAlgebra (D := D) d) (MultiplicityModule (D := D) d m) =
194       (maxCeilDiv d m : Cardinal) := by
195   rw [← seedRank_linearEquiv (columnsEquiv (D := D) d m)]
196   exact divisionProduct_seedRank_eq_maxCeilDiv d m hd
197 
198 /-- The exact finite-direct-sum form of the multiplicity formula. -/
199 theorem directSum_seedRank (hd : ∀ i, 0 < d i) :
200     seedRank (DivisionProductAlgebra (D := D) d)
201       (⨁ i : I, (Fin (m i) → Simple (D := D) d i)) =
202         (maxCeilDiv d m : Cardinal) := by
203   rw [← seedRank_linearEquiv (multiplicityDirectSumEquiv (D := D) d m)]
204   exact multiplicity_seedRank d m hd
205 
206 end Rectangular
207 end Product
208 end Komorebi.PaperICompletion8.RegularMultiplicity

Back to source controls