SeedRankOperations.lean

1 import KomorebiVerification.SeedRankBasics
2 
3 /-!
4 # Seed-rank operations for Paper I
5 
6 This file completes the finite algebraic seed-rank operations used in Paper I:
7 the finite free-presentation minimum, unrestricted cyclicity, semilinear
8 quotient monotonicity and image-algebra invariance, shared and independent
9 direct sums, the tensor-product bound for the natural operator action, and the
10 scalar-quotient obstruction.
11 -/
12 
13 set_option autoImplicit false
14 
15 -- Keep theorem bodies stable in this audit release while making the build warning-fatal.
16 set_option linter.unnecessarySimpa false
17 set_option linter.style.haveILetI false
18 set_option linter.unusedSectionVars false
19 
20 namespace Komorebi.SeedRankOperations
21 
22 open Cardinal Set
23 open Komorebi.SeedRankBasics
24 open scoped TensorProduct
25 
26 universe u
27 
28 section FiniteFreePresentation
29 
30 variable (A M : Type u)
31 variable [Semiring A] [AddCommMonoid M] [Module A M]
32 
33 /-- A finite module admits a generating family indexed by its seed finrank. -/
34 theorem exists_minimal_fin_family [Module.Finite A M] :
35     ∃ v : Fin (seedFinrank A M) → M, FamilyGenerates A M v := by
36   classical
37   obtain ⟨s, hsCard, hsSpan⟩ :=
38     Submodule.FG.exists_span_finset_card_eq_spanFinrank
39       (R := A) (M := M) Module.Finite.fg_top
40   have hcard : seedFinrank A M = s.card := by
41     simpa [seedFinrank] using hsCard.symm
42   let e : Fin (seedFinrank A M) ≃ s :=
43     (Equiv.cast (congrArg Fin hcard)).trans s.equivFin.symm
44   refine ⟨fun i ↦ (e i : M), ?_⟩
45   rw [FamilyGenerates, Generates]
46   have hrange : Set.range (fun i ↦ (e i : M)) = (s : Set M) := by
47     ext x
48     constructor
49     · rintro ⟨i, rfl⟩
50       exact (e i).property
51     · intro hx
52       have hx' : x ∈ s := by simpa using hx
53       let sx : s := ⟨x, hx'⟩
54       exact ⟨e.symm sx, by simp [sx]⟩
55   rw [hrange]
56   simpa using hsSpan
57 
58 /--
59 The seed finrank is the least finite rank of a free module admitting a
60 surjective presentation map onto a finite module.
61 -/
62 theorem seedFinrank_isLeast_free_surjection [Module.Finite A M] :
63     IsLeast
64       {n : ℕ | ∃ f : (Fin n →₀ A) →ₗ[A] M, Function.Surjective f}
65       (seedFinrank A M) := by
66   constructor
67   · obtain ⟨v, hv⟩ := exists_minimal_fin_family A M
68     exact ⟨multiSeedMap A M v, (familyGenerates_iff_surjective A M v).mp hv⟩
69   · intro n hn
70     obtain ⟨f, hf⟩ := hn
71     have hrank : seedRank A M ≤ seedRank A (Fin n →₀ A) :=
72       seedRank_le_of_surjective f hf
73     have hfree : seedRank A (Fin n →₀ A) ≤ n := by
74       let v : Fin n → (Fin n →₀ A) :=
75         (Finsupp.basisSingleOne : Module.Basis (Fin n) A (Fin n →₀ A))
76       have hv : FamilyGenerates A (Fin n →₀ A) v := by
77         rw [FamilyGenerates, Generates]
78         simpa [v] using
79           (Finsupp.basisSingleOne : Module.Basis (Fin n) A (Fin n →₀ A)).span_eq
80       simpa using seedRank_le_mk_of_familyGenerates A (Fin n →₀ A) hv
81     have hcard : (seedFinrank A M : Cardinal) ≤ n := by
82       rw [← seedRank_eq_seedFinrank A M]
83       exact hrank.trans hfree
84     exact_mod_cast hcard
85 
86 end FiniteFreePresentation
87 
88 section Cyclicity
89 
90 variable (A M : Type u)
91 variable [Semiring A] [AddCommMonoid M] [Module A M] [Nontrivial M]
92 
93 /-- For every nonzero module, cardinal seed rank one is exactly cyclicity. -/
94 theorem cyclic_iff_seedRank_eq_one :
95     Cyclic A M ↔ seedRank A M = 1 := by
96   constructor
97   · intro hcyc
98     have hle : seedRank A M ≤ 1 := by
99       obtain ⟨x, hx⟩ := hcyc
100       simpa using seedRank_le_mk_of_generates A M hx
101     have hne : seedRank A M ≠ 0 := by
102       intro hzero
103       have hs : Subsingleton M := (seedRank_eq_zero_iff A M).mp hzero
104       exact not_subsingleton M hs
105     exact hle.antisymm (Cardinal.one_le_iff_ne_zero.mpr hne)
106   · intro hrank
107     have hfinite : Module.Finite A M :=
108       (seedRank_lt_aleph0_iff A M).mp (by simpa [hrank])
109     letI : Module.Finite A M := hfinite
110     exact (seedRank_eq_one_iff_cyclic A M).mp hrank
111 
112 end Cyclicity
113 
114 section SemilinearFunctoriality
115 
116 variable {A B M N : Type u}
117 variable [Semiring A] [Semiring B]
118 variable [AddCommMonoid M] [Module A M]
119 variable [AddCommMonoid N] [Module B N]
120 variable {σ : A →+* B}
121 
122 /--
123 Seed rank cannot increase under a surjective semilinear map, with no
124 surjectivity hypothesis on the scalar homomorphism.  The image of a minimal
125 generating set already spans the target over `B` because its `B`-span contains
126 all finite combinations whose coefficients lie in the image of `σ`.
127 -/
128 theorem seedRank_le_of_surjective_semilinear (f : M →ₛₗ[σ] N)
129     (hf : Function.Surjective f) :
130     seedRank B N ≤ seedRank A M := by
131   classical
132   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A M
133   have himage : Generates B N (f '' s) := by
134     rw [Generates]
135     apply top_unique
136     intro y _
137     obtain ⟨x, rfl⟩ := hf y
138     have hx : x ∈ Submodule.span A s := by
139       rw [hs]
140       trivial
141     refine Submodule.span_induction
142       (p := fun x _ ↦ f x ∈ Submodule.span B (f '' s)) ?_ ?_ ?_ ?_ hx
143     · intro x hxs
144       exact Submodule.subset_span ⟨x, hxs, rfl⟩
145     · simpa using (Submodule.zero_mem (Submodule.span B (f '' s)))
146     · intro x y _ _ hx' hy'
147       simpa using (Submodule.add_mem (Submodule.span B (f '' s)) hx' hy')
148     · intro a x _ hx'
149       simpa using (Submodule.smul_mem (Submodule.span B (f '' s)) (σ a) hx')
150   calc
151     seedRank B N ≤ Cardinal.mk (f '' s) :=
152       seedRank_le_mk_of_generates B N himage
153     _ ≤ Cardinal.mk s := Cardinal.mk_image_le
154     _ = seedRank A M := hsCard
155 
156 /--
157 If the scalar map is onto and the semilinear intertwiner is bijective, seed
158 rank is invariant.  Taking `B` to be the image of an algebra map is the
159 image-algebra form of Paper I's invariance statement.
160 -/
161 theorem seedRank_eq_of_bijective_semilinear (f : M →ₛₗ[σ] N)
162     [RingHomSurjective σ]
163     (hf : Function.Bijective f) :
164     seedRank A M = seedRank B N := by
165   rw [seedRank, seedRank]
166   calc
167     (⊤ : Submodule A M).spanRank = (Submodule.map f ⊤).spanRank :=
168       (Submodule.spanRank_map_eq_of_injective f hf.injective ⊤).symm
169     _ = (⊤ : Submodule B N).spanRank := by
170       rw [Submodule.map_top, LinearMap.range_eq_top.mpr hf.surjective]
171 
172 end SemilinearFunctoriality
173 
174 section ImageAlgebraInvariance
175 
176 variable {k A B M N : Type u}
177 variable [CommSemiring k]
178 variable [Semiring A] [Algebra k A]
179 variable [Semiring B] [Algebra k B]
180 variable [AddCommMonoid M] [Module A M]
181 variable [AddCommMonoid N] [Module B N]
182 
183 /--
184 Literal image-algebra invariance from Paper I.  The target is restricted from
185 `B` to the subalgebra `φ.range`; a bijective `φ`-semilinear intertwiner then
186 preserves seed rank exactly.  No surjectivity of `φ : A →ₐ[k] B` is assumed.
187 -/
188 theorem seedRank_imageAlgebra_eq
189     (φ : A →ₐ[k] B) (f : M →ₛₗ[φ.toRingHom] N)
190     (hf : Function.Bijective f) :
191     letI : Module φ.range N := Module.compHom N φ.range.val.toRingHom
192     seedRank A M = seedRank φ.range N := by
193   letI : Module φ.range N := Module.compHom N φ.range.val.toRingHom
194   let fRange : M →ₛₗ[φ.rangeRestrict.toRingHom] N :=
195     { toFun := f
196       map_add' := f.map_add
197       map_smul' := fun a x ↦ by
198         change f (a • x) = (↑(φ.rangeRestrict a) : B) • f x
199         simpa using f.map_smulₛₗ a x }
200   letI : RingHomSurjective φ.rangeRestrict.toRingHom :=
201     ⟨φ.rangeRestrict_surjective⟩
202   exact seedRank_eq_of_bijective_semilinear fRange hf
203 
204 end ImageAlgebraInvariance
205 
206 section SharedDirectSum
207 
208 variable (A M N : Type u)
209 variable [Semiring A]
210 variable [AddCommMonoid M] [Module A M]
211 variable [AddCommMonoid N] [Module A N]
212 
213 private theorem sharedSum_familyGenerates
214     {ι κ : Type u} {v : ι → M} {w : κ → N}
215     (hv : FamilyGenerates A M v) (hw : FamilyGenerates A N w) :
216     FamilyGenerates A (M × N)
217       (Sum.elim (fun i ↦ (v i, 0)) (fun j ↦ (0, w j))) := by
218   rw [FamilyGenerates, Generates] at hv hw
219   let z : ι ⊕ κ → M × N :=
220     Sum.elim (fun i ↦ (v i, 0)) (fun j ↦ (0, w j))
221   let p : Submodule A (M × N) := Submodule.span A (Set.range z)
222   change p = ⊤
223   have hleft : ∀ x : M, (x, 0) ∈ p := by
224     intro x
225     have hx : x ∈ Submodule.span A (Set.range v) := by simpa [hv]
226     refine Submodule.span_induction (p := fun x _ ↦ (x, 0) ∈ p) ?_ ?_ ?_ ?_ hx
227     · intro x hxv
228       obtain ⟨i, rfl⟩ := hxv
229       exact Submodule.subset_span ⟨Sum.inl i, rfl⟩
230     · exact p.zero_mem
231     · intro x y _ _ hx' hy'
232       simpa using p.add_mem hx' hy'
233     · intro a x _ hx'
234       simpa using p.smul_mem a hx'
235   have hright : ∀ y : N, (0, y) ∈ p := by
236     intro y
237     have hy : y ∈ Submodule.span A (Set.range w) := by simpa [hw]
238     refine Submodule.span_induction (p := fun y _ ↦ (0, y) ∈ p) ?_ ?_ ?_ ?_ hy
239     · intro y hyw
240       obtain ⟨j, rfl⟩ := hyw
241       exact Submodule.subset_span ⟨Sum.inr j, rfl⟩
242     · exact p.zero_mem
243     · intro x y _ _ hx' hy'
244       simpa using p.add_mem hx' hy'
245     · intro a y _ hy'
246       simpa using p.smul_mem a hy'
247   apply top_unique
248   rintro ⟨x, y⟩ _
249   simpa using p.add_mem (hleft x) (hright y)
250 
251 /-- One diagonally acting algebra gives the shared direct-sum upper bound. -/
252 theorem seedRank_prod_le_add :
253     seedRank A (M × N) ≤ seedRank A M + seedRank A N := by
254   classical
255   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A M
256   obtain ⟨t, ht, htCard⟩ := exists_generating_set_card_eq_seedRank A N
257   let v : s → M := Subtype.val
258   let w : t → N := Subtype.val
259   have hv : FamilyGenerates A M v := by
260     simpa [FamilyGenerates, Generates, v] using hs
261   have hw : FamilyGenerates A N w := by
262     simpa [FamilyGenerates, Generates, w] using ht
263   have hgen := sharedSum_familyGenerates A M N hv hw
264   have hbound := seedRank_le_mk_of_familyGenerates A (M × N) hgen
265   simpa [Cardinal.mk_sum, hsCard, htCard] using hbound
266 
267 end SharedDirectSum
268 
269 section IndependentDirectSum
270 
271 variable (A B M N : Type u)
272 variable [Semiring A] [Semiring B]
273 variable [AddCommMonoid M] [Module A M]
274 variable [AddCommMonoid N] [Module B N]
275 
276 /-- The coordinatewise action of `A × B` on `M × N`. -/
277 local instance productModule : Module (A × B) (M × N) where
278   smul r x := (r.1 • x.1, r.2 • x.2)
279   one_smul x := by
280     change ((1 : A) • x.1, (1 : B) • x.2) = x
281     ext <;> simp
282   mul_smul r s x := by
283     change ((r.1 * s.1) • x.1, (r.2 * s.2) • x.2) =
284       (r.1 • s.1 • x.1, r.2 • s.2 • x.2)
285     ext <;> simp [mul_smul]
286   smul_add r x y := by
287     change (r.1 • (x.1 + y.1), r.2 • (x.2 + y.2)) =
288       (r.1 • x.1 + r.1 • y.1, r.2 • x.2 + r.2 • y.2)
289     ext <;> simp [smul_add]
290   add_smul r s x := by
291     change ((r.1 + s.1) • x.1, (r.2 + s.2) • x.2) =
292       (r.1 • x.1 + s.1 • x.1, r.2 • x.2 + s.2 • x.2)
293     ext <;> simp [add_smul]
294   zero_smul x := by
295     change ((0 : A) • x.1, (0 : B) • x.2) = 0
296     ext <;> simp
297   smul_zero r := by
298     change (r.1 • (0 : M), r.2 • (0 : N)) = 0
299     ext <;> simp
300 
301 @[simp] private theorem product_smul_mk (a : A) (b : B) (x : M) (y : N) :
302     (a, b) • (x, y) = (a • x, b • y) := rfl
303 
304 /-- First projection as a semilinear map along `(A × B) → A`. -/
305 def prodFstSemilinear :
306     (M × N) →ₛₗ[RingHom.fst A B] M where
307   toFun := Prod.fst
308   map_add' _ _ := rfl
309   map_smul' _ _ := rfl
310 
311 /-- Second projection as a semilinear map along `(A × B) → B`. -/
312 def prodSndSemilinear :
313     (M × N) →ₛₗ[RingHom.snd A B] N where
314   toFun := Prod.snd
315   map_add' _ _ := rfl
316   map_smul' _ _ := rfl
317 
318 private theorem product_familyGenerates
319     {ι : Type u} {v : ι → M} {w : ι → N}
320     (hv : FamilyGenerates A M v) (hw : FamilyGenerates B N w) :
321     FamilyGenerates (A × B) (M × N) (fun i ↦ (v i, w i)) := by
322   rw [FamilyGenerates, Generates] at hv hw
323   let z : ι → M × N := fun i ↦ (v i, w i)
324   let p : Submodule (A × B) (M × N) := Submodule.span (A × B) (Set.range z)
325   change p = ⊤
326   have hleft : ∀ x : M, (x, 0) ∈ p := by
327     intro x
328     have hx : x ∈ Submodule.span A (Set.range v) := by simpa [hv]
329     refine Submodule.span_induction (p := fun x _ ↦ (x, 0) ∈ p) ?_ ?_ ?_ ?_ hx
330     · intro x hxv
331       obtain ⟨i, rfl⟩ := hxv
332       have hz : z i ∈ p := Submodule.subset_span (Set.mem_range_self i)
333       have hmem := p.smul_mem (1, 0) hz
334       simpa [z] using hmem
335     · exact p.zero_mem
336     · intro x y _ _ hx' hy'
337       simpa using p.add_mem hx' hy'
338     · intro a x _ hx'
339       have hmem := p.smul_mem (a, 0) hx'
340       simpa using hmem
341   have hright : ∀ y : N, (0, y) ∈ p := by
342     intro y
343     have hy : y ∈ Submodule.span B (Set.range w) := by simpa [hw]
344     refine Submodule.span_induction (p := fun y _ ↦ (0, y) ∈ p) ?_ ?_ ?_ ?_ hy
345     · intro y hyw
346       obtain ⟨i, rfl⟩ := hyw
347       have hz : z i ∈ p := Submodule.subset_span (Set.mem_range_self i)
348       have hmem := p.smul_mem (0, 1) hz
349       simpa [z] using hmem
350     · exact p.zero_mem
351     · intro x y _ _ hx' hy'
352       simpa using p.add_mem hx' hy'
353     · intro b y _ hy'
354       have hmem := p.smul_mem (0, b) hy'
355       simpa using hmem
356   apply top_unique
357   rintro ⟨x, y⟩ _
358   simpa using p.add_mem (hleft x) (hright y)
359 
360 private theorem seedRank_prod_le_right_of_le
361     (hMN : seedRank A M ≤ seedRank B N) :
362     seedRank (A × B) (M × N) ≤ seedRank B N := by
363   classical
364   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A M
365   obtain ⟨t, ht, htCard⟩ := exists_generating_set_card_eq_seedRank B N
366   have hst : Cardinal.mk s ≤ Cardinal.mk t := by simpa [hsCard, htCard] using hMN
367   let e : s ↪ t := Classical.choice (Cardinal.lift_mk_le'.mp (by simpa using hst))
368   let v : t → M := Function.extend e (fun i : s ↦ (i : M)) (fun _ ↦ 0)
369   let w : t → N := fun j ↦ (j : N)
370   have hv : FamilyGenerates A M v := by
371     rw [FamilyGenerates, Generates]
372     apply top_unique
373     rw [← hs]
374     apply Submodule.span_mono
375     intro x hx
376     let i : s := ⟨x, hx⟩
377     refine ⟨e i, ?_⟩
378     simpa [v, i] using
379       e.injective.extend_apply (fun i : s ↦ (i : M)) (fun _ : t ↦ 0) i
380   have hw : FamilyGenerates B N w := by
381     simpa [FamilyGenerates, Generates, w] using ht
382   have hgen := product_familyGenerates A B M N hv hw
383   have hbound := seedRank_le_mk_of_familyGenerates (A × B) (M × N) hgen
384   simpa [htCard] using hbound
385 
386 private theorem seedRank_prod_le_left_of_le
387     (hNM : seedRank B N ≤ seedRank A M) :
388     seedRank (A × B) (M × N) ≤ seedRank A M := by
389   classical
390   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A M
391   obtain ⟨t, ht, htCard⟩ := exists_generating_set_card_eq_seedRank B N
392   have hts : Cardinal.mk t ≤ Cardinal.mk s := by simpa [hsCard, htCard] using hNM
393   let e : t ↪ s := Classical.choice (Cardinal.lift_mk_le'.mp (by simpa using hts))
394   let v : s → M := fun i ↦ (i : M)
395   let w : s → N := Function.extend e (fun j : t ↦ (j : N)) (fun _ ↦ 0)
396   have hv : FamilyGenerates A M v := by
397     simpa [FamilyGenerates, Generates, v] using hs
398   have hw : FamilyGenerates B N w := by
399     rw [FamilyGenerates, Generates]
400     apply top_unique
401     rw [← ht]
402     apply Submodule.span_mono
403     intro y hy
404     let j : t := ⟨y, hy⟩
405     refine ⟨e j, ?_⟩
406     simpa [w, j] using
407       e.injective.extend_apply (fun j : t ↦ (j : N)) (fun _ : s ↦ 0) j
408   have hgen := product_familyGenerates A B M N hv hw
409   have hbound := seedRank_le_mk_of_familyGenerates (A × B) (M × N) hgen
410   simpa [hsCard] using hbound
411 
412 /-- Under the independent product action, seed rank is the maximum. -/
413 theorem seedRank_prod_productAlgebra :
414     seedRank (A × B) (M × N) = max (seedRank A M) (seedRank B N) := by
415   apply le_antisymm
416   · rcases le_total (seedRank A M) (seedRank B N) with hMN | hNM
417     · simpa [max_eq_right hMN] using
418         seedRank_prod_le_right_of_le A B M N hMN
419     · simpa [max_eq_left hNM] using
420         seedRank_prod_le_left_of_le A B M N hNM
421   · apply max_le
422     · exact seedRank_le_of_surjective_semilinear
423         (prodFstSemilinear A B M N) (fun x ↦ ⟨(x, 0), rfl⟩)
424     · exact seedRank_le_of_surjective_semilinear
425         (prodSndSemilinear A B M N) (fun y ↦ ⟨(0, y), rfl⟩)
426 
427 end IndependentDirectSum
428 
429 section TensorProduct
430 
431 variable (k A B X Y : Type u)
432 variable [CommSemiring k]
433 variable [Semiring A] [Algebra k A]
434 variable [Semiring B] [Algebra k B]
435 variable [AddCommMonoid X] [Module k X] [Module A X]
436 variable [IsScalarTower k A X] [SMulCommClass k A X]
437 variable [AddCommMonoid Y] [Module k Y] [Module B Y]
438 variable [IsScalarTower k B Y] [SMulCommClass k B Y]
439 
440 /-- The action of `B` on the right tensor factor. -/
441 @[instance_reducible] private def tensorRightModule :
442     Module B (TensorProduct k X Y) := by
443   let e : TensorProduct k X Y ≃ₗ[k] TensorProduct k Y X :=
444     TensorProduct.comm k X Y
445   letI : Module B (TensorProduct k Y X) := TensorProduct.leftModule
446   exact
447     { smul := fun b z ↦ e.symm (b • e z)
448       one_smul := fun z ↦ by
449         change e.symm ((1 : B) • e z) = z
450         rw [one_smul, e.symm_apply_apply]
451       mul_smul := fun b c z ↦ by
452         change e.symm ((b * c) • e z) =
453           e.symm (b • e (e.symm (c • e z)))
454         rw [mul_smul, e.apply_symm_apply]
455       smul_add := fun b z w ↦ by
456         change e.symm (b • e (z + w)) =
457           e.symm (b • e z) + e.symm (b • e w)
458         rw [e.map_add, smul_add, e.symm.map_add]
459       add_smul := fun b c z ↦ by
460         change e.symm ((b + c) • e z) =
461           e.symm (b • e z) + e.symm (c • e z)
462         rw [add_smul, e.symm.map_add]
463       zero_smul := fun z ↦ by
464         change e.symm ((0 : B) • e z) = 0
465         rw [zero_smul, map_zero]
466       smul_zero := fun b ↦ by
467         change e.symm (b • e 0) = 0
468         rw [map_zero, smul_zero, map_zero] }
469 
470 local instance (priority := 50) tensorRightModuleInstance :
471     Module B (TensorProduct k X Y) :=
472   tensorRightModule k B X Y
473 
474 @[simp] private theorem tensorRight_smul_tmul (b : B) (x : X) (y : Y) :
475     b • (x ⊗ₜ[k] y) = x ⊗ₜ[k] (b • y) := by
476   change (TensorProduct.comm k X Y).symm
477       (b • (TensorProduct.comm k X Y) (x ⊗ₜ[k] y)) = _
478   rw [TensorProduct.comm_tmul, TensorProduct.smul_tmul',
479     TensorProduct.comm_symm_tmul]
480 
481 local instance tensorRightTower :
482     IsScalarTower k B (TensorProduct k X Y) where
483   smul_assoc r b z := by
484     induction z using TensorProduct.induction_on with
485     | zero => simp
486     | tmul x y => simp [smul_assoc]
487     | add z w hz hw => simp [smul_add, hz, hw]
488 
489 local instance tensorLeftTower :
490     IsScalarTower k A (TensorProduct k X Y) where
491   smul_assoc r a z := by
492     induction z using TensorProduct.induction_on with
493     | zero => simp
494     | tmul x y => simp [TensorProduct.smul_tmul', smul_assoc]
495     | add z w hz hw => simp [smul_add, hz, hw]
496 
497 local instance tensorActionsCommute :
498     SMulCommClass A B (TensorProduct k X Y) where
499   smul_comm a b z := by
500     induction z using TensorProduct.induction_on with
501     | zero => simp
502     | tmul x y => simp [TensorProduct.smul_tmul']
503     | add z w hz hw => simp [smul_add, hz, hw]
504 
505 attribute [local instance 2000] tensorLeftTower tensorRightTower tensorActionsCommute
506 
507 local instance tensorLeftTowerInstalled :
508     IsScalarTower k A (TensorProduct k X Y) :=
509   tensorLeftTower k A X Y
510 
511 local instance tensorRightTowerInstalled :
512     IsScalarTower k B (TensorProduct k X Y) :=
513   tensorRightTower k B X Y
514 
515 local instance tensorActionsCommuteInstalled :
516     SMulCommClass A B (TensorProduct k X Y) :=
517   tensorActionsCommute k A B X Y
518 
519 /-- The natural `(A ⊗[k] B)` action on `X ⊗[k] Y`. -/
520 local instance tensorOperatorModule :
521     Module (A ⊗[k] B) (TensorProduct k X Y) :=
522   TensorProduct.Algebra.module
523 
524 /-- Pure operator tensors act componentwise on pure vector tensors. -/
525 @[simp] theorem tensorOperator_smul_tmul
526     (a : A) (b : B) (x : X) (y : Y) :
527     (a ⊗ₜ[k] b : A ⊗[k] B) • (x ⊗ₜ[k] y) =
528       (a • x) ⊗ₜ[k] (b • y) := by
529   change TensorProduct.Algebra.moduleAux (a ⊗ₜ[k] b) (x ⊗ₜ[k] y) = _
530   rw [TensorProduct.Algebra.moduleAux_apply]
531   simp [TensorProduct.smul_tmul']
532 
533 private theorem tensor_familyGenerates
534     {ι κ : Type u} {v : ι → X} {w : κ → Y}
535     (hv : FamilyGenerates A X v) (hw : FamilyGenerates B Y w) :
536     FamilyGenerates (A ⊗[k] B) (TensorProduct k X Y)
537       (fun p : ι × κ ↦ v p.1 ⊗ₜ[k] w p.2) := by
538   rw [FamilyGenerates, Generates] at hv hw
539   let z : ι × κ → TensorProduct k X Y :=
540     fun p ↦ v p.1 ⊗ₜ[k] w p.2
541   let p : Submodule (A ⊗[k] B) (TensorProduct k X Y) :=
542     Submodule.span (A ⊗[k] B) (Set.range z)
543   change p = ⊤
544   have hpure : ∀ x : X, ∀ y : Y, x ⊗ₜ[k] y ∈ p := by
545     intro x
546     have hx : x ∈ Submodule.span A (Set.range v) := by simpa [hv]
547     refine Submodule.span_induction
548       (p := fun x _ ↦ ∀ y : Y, x ⊗ₜ[k] y ∈ p) ?_ ?_ ?_ ?_ hx
549     · intro x hxv y
550       obtain ⟨i, rfl⟩ := hxv
551       have hy : y ∈ Submodule.span B (Set.range w) := by simpa [hw]
552       refine Submodule.span_induction
553         (p := fun y _ ↦ v i ⊗ₜ[k] y ∈ p) ?_ ?_ ?_ ?_ hy
554       · intro y hyw
555         obtain ⟨j, rfl⟩ := hyw
556         exact Submodule.subset_span ⟨(i, j), rfl⟩
557       · simpa using p.zero_mem
558       · intro y₁ y₂ _ _ h₁ h₂
559         simpa [TensorProduct.tmul_add] using p.add_mem h₁ h₂
560       · intro b y _ hy'
561         have hmem := p.smul_mem (1 ⊗ₜ[k] b : A ⊗[k] B) hy'
562         simpa using hmem
563     · intro y
564       simpa using p.zero_mem
565     · intro x₁ x₂ _ _ h₁ h₂ y
566       simpa [TensorProduct.add_tmul] using p.add_mem (h₁ y) (h₂ y)
567     · intro a x _ hx' y
568       have hmem := p.smul_mem (a ⊗ₜ[k] 1 : A ⊗[k] B) (hx' y)
569       simpa using hmem
570   apply top_unique
571   intro q _
572   exact TensorProduct.induction_on q p.zero_mem hpure
573     (fun _ _ hq hr ↦ p.add_mem hq hr)
574 
575 /--
576 For the natural operator-tensor action, tensor-product seed rank is bounded by
577 the product of the two seed ranks.
578 -/
579 theorem seedRank_tensorProduct_le_mul :
580     seedRank (A ⊗[k] B) (TensorProduct k X Y) ≤
581       seedRank A X * seedRank B Y := by
582   classical
583   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A X
584   obtain ⟨t, ht, htCard⟩ := exists_generating_set_card_eq_seedRank B Y
585   let v : s → X := Subtype.val
586   let w : t → Y := Subtype.val
587   have hv : FamilyGenerates A X v := by
588     simpa [FamilyGenerates, Generates, v] using hs
589   have hw : FamilyGenerates B Y w := by
590     simpa [FamilyGenerates, Generates, w] using ht
591   have hgen := tensor_familyGenerates k A B X Y hv hw
592   have hbound := seedRank_le_mk_of_familyGenerates
593     (A ⊗[k] B) (TensorProduct k X Y) hgen
594   simpa [Cardinal.mk_prod, hsCard, htCard] using hbound
595 
596 end TensorProduct
597 
598 section ScalarQuotient
599 
600 variable (k A X Y : Type u)
601 variable [Field k] [Semiring A] [Algebra k A]
602 variable [AddCommMonoid X] [Module A X]
603 variable [AddCommGroup Y] [Module k Y] [Module.Finite k Y]
604 
605 /-- Every algebra character onto its base field is surjective. -/
606 private theorem character_surjective (χ : A →ₐ[k] k) :
607     Function.Surjective χ := by
608   intro y
609   refine ⟨algebraMap k A y, ?_⟩
610   exact χ.commutes y
611 
612 /--
613 Scalar quotient obstruction.  A character `χ : A →ₐ[k] k` records that every
614 operator acts on the quotient through a scalar.  Any surjective intertwiner
615 onto a finite-dimensional scalar module forces its dimension to be a lower
616 bound for the seed rank upstairs.
617 -/
618 theorem finrank_le_seedRank_of_scalar_quotient
619     (χ : A →ₐ[k] k) (f : X →ₛₗ[χ.toRingHom] Y)
620     (hf : Function.Surjective f) :
621     (Module.finrank k Y : Cardinal) ≤ seedRank A X := by
622   letI : RingHomSurjective χ.toRingHom :=
623     ⟨character_surjective k A χ⟩
624   have hquot : seedRank k Y ≤ seedRank A X :=
625     seedRank_le_of_surjective_semilinear f hf
626   have hrank : seedRank k Y = Module.finrank k Y := by
627     rw [seedRank_eq_seedFinrank k Y, seedFinrank,
628       ← Module.finrank_eq_spanFinrank_of_free]
629   simpa [hrank] using hquot
630 
631 end ScalarQuotient
632 
633 end Komorebi.SeedRankOperations
634 
635 #print axioms Komorebi.SeedRankOperations.seedFinrank_isLeast_free_surjection
636 #print axioms Komorebi.SeedRankOperations.cyclic_iff_seedRank_eq_one
637 #print axioms Komorebi.SeedRankOperations.seedRank_le_of_surjective_semilinear
638 #print axioms Komorebi.SeedRankOperations.seedRank_eq_of_bijective_semilinear
639 #print axioms Komorebi.SeedRankOperations.seedRank_imageAlgebra_eq
640 #print axioms Komorebi.SeedRankOperations.seedRank_prod_le_add
641 #print axioms Komorebi.SeedRankOperations.seedRank_prod_productAlgebra
642 #print axioms Komorebi.SeedRankOperations.seedRank_tensorProduct_le_mul
643 #print axioms Komorebi.SeedRankOperations.finrank_le_seedRank_of_scalar_quotient

Back to source controls