ScalarExtension.lean

1 import KomorebiVerification.SeedRankOperations
2 set_option autoImplicit false
3 set_option linter.unusedSectionVars false
4 set_option linter.unnecessarySimpa false
5 noncomputable section
6 namespace Komorebi.PaperIRelease.ScalarExtension
7 open Komorebi.SeedRankBasics
8 open scoped TensorProduct
9 universe u
10 
11 -- Natural action construction retained from the verified tensor-operator interface.
12 section TensorProduct
13 
14 variable (k A B X Y : Type u)
15 variable [CommSemiring k]
16 variable [Semiring A] [Algebra k A]
17 variable [Semiring B] [Algebra k B]
18 variable [AddCommMonoid X] [Module k X] [Module A X]
19 variable [IsScalarTower k A X] [SMulCommClass k A X]
20 variable [AddCommMonoid Y] [Module k Y] [Module B Y]
21 variable [IsScalarTower k B Y] [SMulCommClass k B Y]
22 
23 /-- The action of `B` on the right tensor factor. -/
24 @[instance_reducible] def tensorRightModule :
25     Module B (TensorProduct k X Y) := by
26   let e : TensorProduct k X Y ≃ₗ[k] TensorProduct k Y X :=
27     TensorProduct.comm k X Y
28   letI : Module B (TensorProduct k Y X) := TensorProduct.leftModule
29   exact
30     { smul := fun b z ↦ e.symm (b • e z)
31       one_smul := fun z ↦ by
32         change e.symm ((1 : B) • e z) = z
33         rw [one_smul, e.symm_apply_apply]
34       mul_smul := fun b c z ↦ by
35         change e.symm ((b * c) • e z) =
36           e.symm (b • e (e.symm (c • e z)))
37         rw [mul_smul, e.apply_symm_apply]
38       smul_add := fun b z w ↦ by
39         change e.symm (b • e (z + w)) =
40           e.symm (b • e z) + e.symm (b • e w)
41         rw [e.map_add, smul_add, e.symm.map_add]
42       add_smul := fun b c z ↦ by
43         change e.symm ((b + c) • e z) =
44           e.symm (b • e z) + e.symm (c • e z)
45         rw [add_smul, e.symm.map_add]
46       zero_smul := fun z ↦ by
47         change e.symm ((0 : B) • e z) = 0
48         rw [zero_smul, map_zero]
49       smul_zero := fun b ↦ by
50         change e.symm (b • e 0) = 0
51         rw [map_zero, smul_zero, map_zero] }
52 
53 local instance (priority := 50) tensorRightModuleInstance :
54     Module B (TensorProduct k X Y) :=
55   tensorRightModule k B X Y
56 
57 @[simp] theorem tensorRight_smul_tmul (b : B) (x : X) (y : Y) :
58     b • (x ⊗ₜ[k] y) = x ⊗ₜ[k] (b • y) := by
59   change (TensorProduct.comm k X Y).symm
60       (b • (TensorProduct.comm k X Y) (x ⊗ₜ[k] y)) = _
61   rw [TensorProduct.comm_tmul, TensorProduct.smul_tmul',
62     TensorProduct.comm_symm_tmul]
63 
64 local instance tensorRightTower :
65     IsScalarTower k B (TensorProduct k X Y) where
66   smul_assoc r b z := by
67     induction z using TensorProduct.induction_on with
68     | zero => simp
69     | tmul x y => simp [smul_assoc]
70     | add z w hz hw => simp [smul_add, hz, hw]
71 
72 local instance tensorLeftTower :
73     IsScalarTower k A (TensorProduct k X Y) where
74   smul_assoc r a z := by
75     induction z using TensorProduct.induction_on with
76     | zero => simp
77     | tmul x y => simp [TensorProduct.smul_tmul', smul_assoc]
78     | add z w hz hw => simp [smul_add, hz, hw]
79 
80 local instance tensorActionsCommute :
81     SMulCommClass A B (TensorProduct k X Y) where
82   smul_comm a b z := by
83     induction z using TensorProduct.induction_on with
84     | zero => simp
85     | tmul x y => simp [TensorProduct.smul_tmul']
86     | add z w hz hw => simp [smul_add, hz, hw]
87 
88 attribute [local instance 2000] tensorLeftTower tensorRightTower tensorActionsCommute
89 
90 local instance tensorLeftTowerInstalled :
91     IsScalarTower k A (TensorProduct k X Y) :=
92   tensorLeftTower k A X Y
93 
94 local instance tensorRightTowerInstalled :
95     IsScalarTower k B (TensorProduct k X Y) :=
96   tensorRightTower k B X Y
97 
98 local instance tensorActionsCommuteInstalled :
99     SMulCommClass A B (TensorProduct k X Y) :=
100   tensorActionsCommute k A B X Y
101 
102 /-- The natural `(A ⊗[k] B)` action on `X ⊗[k] Y`. -/
103 local instance tensorOperatorModule :
104     Module (A ⊗[k] B) (TensorProduct k X Y) :=
105   TensorProduct.Algebra.module
106 
107 /-- Pure operator tensors act componentwise on pure vector tensors. -/
108 @[simp] theorem tensorOperator_smul_tmul
109     (a : A) (b : B) (x : X) (y : Y) :
110     (a ⊗ₜ[k] b : A ⊗[k] B) • (x ⊗ₜ[k] y) =
111       (a • x) ⊗ₜ[k] (b • y) := by
112   change TensorProduct.Algebra.moduleAux (a ⊗ₜ[k] b) (x ⊗ₜ[k] y) = _
113   rw [TensorProduct.Algebra.moduleAux_apply]
114   simp [TensorProduct.smul_tmul']
115 
116 
117 end TensorProduct
118 
119 section ScalarExtension
120 variable (k K A M : Type u) [Field k] [Field K] [Algebra k K]
121 variable [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M]
122 variable [IsScalarTower k A M] [SMulCommClass k A M]
123 
124 local instance (priority := 2000) : Module K (K ⊗[k] M) := TensorProduct.leftModule
125 local instance (priority := 50) : Module A (K ⊗[k] M) := tensorRightModule k A K M
126 local instance : IsScalarTower k A (K ⊗[k] M) := tensorRightTower k A K M
127 local instance (priority := 2000) : IsScalarTower k K (K ⊗[k] M) := tensorLeftTower k K K M
128 local instance : SMulCommClass K A (K ⊗[k] M) := tensorActionsCommute k K A K M
129 local instance : Module (K ⊗[k] A) (K ⊗[k] M) := TensorProduct.Algebra.module
130 
131 /-- The literal family `1 tensor S` generates after extension of scalars. -/
132 theorem one_tmul_generates (s : Set M) (hs : Generates A M s) :
133     Generates (K ⊗[k] A) (K ⊗[k] M) ((fun m => (1 : K) ⊗ₜ[k] m) '' s) := by
134   let p : Submodule (K ⊗[k] A) (K ⊗[k] M) :=
135     Submodule.span (K ⊗[k] A) ((fun m => (1 : K) ⊗ₜ[k] m) '' s)
136   change p = ⊤
137   have hunit : ∀ m : M, (1 : K) ⊗ₜ[k] m ∈ p := by
138     intro m
139     have hm : m ∈ Submodule.span A s := by rw [hs]; trivial
140     refine Submodule.span_induction (p := fun m _ => (1 : K) ⊗ₜ[k] m ∈ p) ?_ ?_ ?_ ?_ hm
141     · intro x hx
142       exact Submodule.subset_span ⟨x, hx, rfl⟩
143     · simpa using p.zero_mem
144     · intro x y _ _ hx hy
145       simpa [TensorProduct.tmul_add] using p.add_mem hx hy
146     · intro a x _ hx
147       have h := p.smul_mem ((1 : K) ⊗ₜ[k] a) hx
148       simpa only [tensorOperator_smul_tmul, smul_eq_mul, one_mul] using h
149   apply top_unique
150   intro z _
151   refine TensorProduct.induction_on z p.zero_mem ?_ (fun _ _ hx hy => p.add_mem hx hy)
152   intro c m
153   have h := p.smul_mem (c ⊗ₜ[k] (1 : A)) (hunit m)
154   simpa only [tensorOperator_smul_tmul, smul_eq_mul, mul_one, one_smul] using h
155 
156 /-- Scalar extension cannot increase the cardinal seed rank. -/
157 theorem scalar_extension_seedRank_le :
158     seedRank (K ⊗[k] A) (K ⊗[k] M) ≤ seedRank A M := by
159   obtain ⟨s, hs, hc⟩ := exists_generating_set_card_eq_seedRank A M
160   calc
161     seedRank (K ⊗[k] A) (K ⊗[k] M) ≤ Cardinal.mk ((fun m => (1 : K) ⊗ₜ[k] m) '' s) :=
162       seedRank_le_mk_of_generates _ _ (one_tmul_generates k K A M s hs)
163     _ ≤ Cardinal.mk s := Cardinal.mk_image_le
164     _ = seedRank A M := hc
165 
166 end ScalarExtension
167 end Komorebi.PaperIRelease.ScalarExtension

Back to source controls