DivisionProduct.lean

1 import PaperICompletion8.DivisionBlock
2 
3 /-! Finite products of matrix rings over a dependent family of division rings.
4 All scalar actions are actual left multiplication. No Algebra over a
5 noncommutative division ring is requested. -/
6 set_option autoImplicit false
7 set_option linter.unnecessarySimpa false
8 
9 namespace Komorebi.PaperICompletion8.DivisionProduct
10 
11 open scoped BigOperators
12 open Komorebi.SeedRankBasics Komorebi.SeedRankOperations
13 open Komorebi.PaperICompletion8.DivisionRows
14 open Komorebi.PaperICompletion8.DivisionBlock
15 open Komorebi.SemisimpleCompletion (seedFinrank_eq_of_exists_fin_family_iff)
16 
17 universe u v w
18 variable {I : Type v} [Fintype I] [DecidableEq I]
19 variable {D : I → Type u} [∀ i, DivisionRing (D i)]
20 variable (d m : I → ℕ)
21 
22 local instance (priority := 100) blockModuleAction (i : I) :
23     Module (BlockAlgebra (k := D i) (d i)) (BlockModule (k := D i) (d i) (m i)) :=
24   Matrix.Module.matrixModule
25 
26 /-- The literal finite product ring in the nonsplit Wedderburn hypothesis. -/
27 abbrev DivisionProductAlgebra :=
28   ∀ i : I, BlockAlgebra (k := D i) (d i)
29 
30 /-- The literal product of the corresponding isotypic matrix modules. -/
31 abbrev DivisionProductModule :=
32   ∀ i : I, BlockModule (k := D i) (d i) (m i)
33 
34 /-- The maximum of the blockwise ceiling requirements.  `Finset.sup` gives
35 value zero for an empty product; Paper I assumes a nonempty block set. -/
36 def maxCeilDiv : ℕ :=
37   Finset.univ.sup (fun i : I ↦ m i ⌈/⌉ d i)
38 
39 omit [Fintype I] in
40 /-- A family generates the literal product module exactly when its projection
41 to every isotypic block generates that block.  The proof assembles the
42 blockwise coefficient matrices into elements of the product algebra. -/
43 theorem divisionProduct_familyGenerates_iff {r : ℕ}
44     (v : Fin r → DivisionProductModule (D := D) d m) :
45     FamilyGenerates (DivisionProductAlgebra (D := D) d)
46         (DivisionProductModule (D := D) d m) v ↔
47       ∀ i : I, LeftGenerates (fun j ↦ v j i) := by
48   classical
49   rw [FamilyGenerates, Generates, eq_top_iff,
50     Submodule.top_le_span_range_iff_forall_exists_fun]
51   constructor
52   · intro h i X
53     obtain ⟨c, hc⟩ := h (Pi.single i X)
54     refine ⟨fun j ↦ c j i, ?_⟩
55     calc
56       X = (Pi.single i X : DivisionProductModule (D := D) d m) i := by simp
57       _ = (∑ j, c j • v j) i := by rw [hc]
58       _ = ∑ j, (c j i) * (v j i) := by
59         simp only [Finset.sum_apply, Pi.smul_apply', block_smul_eq_mul]
60   · intro h X
61     choose c hc using fun i ↦ h i (X i)
62     let a : Fin r → DivisionProductAlgebra (D := D) d :=
63       fun j i ↦ c i j
64     refine ⟨a, ?_⟩
65     funext i
66     simpa only [Finset.sum_apply, Pi.smul_apply', block_smul_eq_mul, a]
67       using (hc i).symm
68 
69 omit [Fintype I] in
70 /-- Existence of `r` product generators is equivalent to the simultaneous
71 row-dimension inequalities on all simple blocks. -/
72 theorem exists_divisionProduct_generators_iff_coordinate_bounds
73     {r : ℕ} (hd : ∀ i, 0 < d i) :
74     (∃ v : Fin r → DivisionProductModule (D := D) d m,
75       FamilyGenerates (DivisionProductAlgebra (D := D) d)
76         (DivisionProductModule (D := D) d m) v) ↔
77       ∀ i : I, m i ≤ r * d i := by
78   constructor
79   · rintro ⟨v, hv⟩ i
80     exact multiplicity_le_of_leftGenerates (k := D i) (hd i)
81       ((divisionProduct_familyGenerates_iff d m v).mp hv i)
82   · intro h
83     choose w hw using fun i ↦
84       exists_leftGenerators_of_le (k := D i) (hd i) (h i)
85     let v : Fin r → DivisionProductModule (D := D) d m :=
86       fun j i ↦ w i j
87     refine ⟨v, (divisionProduct_familyGenerates_iff d m v).mpr ?_⟩
88     intro i
89     simpa only [v] using hw i
90 
91 /-- The finite-product assembly criterion: `r` seeds exist exactly when `r`
92 is at least the maximum blockwise ceiling. -/
93 theorem exists_divisionProduct_generators_iff_maxCeilDiv_le
94     {r : ℕ} (hd : ∀ i, 0 < d i) :
95     (∃ v : Fin r → DivisionProductModule (D := D) d m,
96       FamilyGenerates (DivisionProductAlgebra (D := D) d)
97         (DivisionProductModule (D := D) d m) v) ↔
98       maxCeilDiv d m ≤ r := by
99   rw [exists_divisionProduct_generators_iff_coordinate_bounds d m hd]
100   constructor
101   · intro h
102     apply Finset.sup_le
103     intro i hi
104     apply (ceilDiv_le_iff_le_mul (hd i)).mpr
105     simpa [Nat.mul_comm] using h i
106   · intro h i
107     have hblock : m i ⌈/⌉ d i ≤ maxCeilDiv d m :=
108       Finset.le_sup (f := fun j : I ↦ m j ⌈/⌉ d j) (Finset.mem_univ i)
109     have hceil : m i ⌈/⌉ d i ≤ r := hblock.trans h
110     have hm : m i ≤ d i * r := (ceilDiv_le_iff_le_mul (hd i)).mp hceil
111     simpa [Nat.mul_comm] using hm
112 
113 /-- The displayed maximum is the least possible size of a finite generating
114 family for the split product module. -/
115 theorem maxCeilDiv_isLeast_product_generatorCount
116     (hd : ∀ i, 0 < d i) :
117     IsLeast
118       {r : ℕ |
119         ∃ v : Fin r → DivisionProductModule (D := D) d m,
120           FamilyGenerates (DivisionProductAlgebra (D := D) d)
121             (DivisionProductModule (D := D) d m) v}
122       (maxCeilDiv d m) := by
123   constructor
124   · exact (exists_divisionProduct_generators_iff_maxCeilDiv_le
125       (D := D) d m hd).mpr le_rfl
126   · intro r hr
127     exact (exists_divisionProduct_generators_iff_maxCeilDiv_le
128       (D := D) d m hd).mp hr
129 
130 /-- Paper I's finite semisimple multiplicity formula for the literal
131 decomposition displayed above. -/
132 theorem divisionProduct_seedFinrank_eq_maxCeilDiv
133     (hd : ∀ i, 0 < d i) :
134     seedFinrank (DivisionProductAlgebra (D := D) d)
135         (DivisionProductModule (D := D) d m) =
136       maxCeilDiv d m := by
137   apply seedFinrank_eq_of_exists_fin_family_iff
138   intro r
139   exact exists_divisionProduct_generators_iff_maxCeilDiv_le (D := D) d m hd
140 
141 /-- Cardinal-valued form of the finite semisimple multiplicity
142 formula. -/
143 theorem divisionProduct_seedRank_eq_maxCeilDiv
144     (hd : ∀ i, 0 < d i) :
145     seedRank (DivisionProductAlgebra (D := D) d)
146         (DivisionProductModule (D := D) d m) =
147       ((maxCeilDiv d m : ℕ) : Cardinal) := by
148   classical
149   obtain ⟨v, hv⟩ :=
150     (exists_divisionProduct_generators_iff_maxCeilDiv_le (D := D) d m hd).mpr le_rfl
151   let : Module.Finite (DivisionProductAlgebra (D := D) d)
152       (DivisionProductModule (D := D) d m) :=
153     Module.Finite.of_surjective
154       (multiSeedMap (DivisionProductAlgebra (D := D) d)
155         (DivisionProductModule (D := D) d m) v)
156       ((familyGenerates_iff_surjective _ _ v).mp hv)
157   rw [seedRank_eq_seedFinrank,
158     divisionProduct_seedFinrank_eq_maxCeilDiv d m hd]
159 
160 /-- Transport of the formula to any module supplied with an explicit linear
161 decomposition over the literal product algebra.  This is the exact hypothesis
162 needed after transporting an abstract semisimple algebra along a chosen
163 Wedderburn isomorphism. -/
164 theorem seedRank_eq_maxCeilDiv_of_divisionProduct_decomposition
165     {X : Type (max u v)} [AddCommMonoid X]
166     [Module (DivisionProductAlgebra (D := D) d) X]
167     (e : X ≃ₗ[DivisionProductAlgebra (D := D) d]
168       DivisionProductModule (D := D) d m)
169     (hd : ∀ i, 0 < d i) :
170     seedRank (DivisionProductAlgebra (D := D) d) X =
171       ((maxCeilDiv d m : ℕ) : Cardinal) := by
172   rw [seedRank_linearEquiv e,
173     divisionProduct_seedRank_eq_maxCeilDiv d m hd]
174 
175 end Komorebi.PaperICompletion8.DivisionProduct

Back to source controls