IntegralActionSpan.lean

1 import Mathlib.RingTheory.Localization.FractionRing
2 import Mathlib.RingTheory.Localization.Integer
3 import Mathlib.RingTheory.Finiteness.Basic
4 import Mathlib.RingTheory.DiscreteValuationRing.Basic
5 import Mathlib.LinearAlgebra.Matrix.ToLin
6 import Mathlib.RepresentationTheory.Irreducible
7 
8 /-! Clearing denominators in a full field-valued action span. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.IntegralActionSpan
12 open scoped BigOperators
13 
14 variable {R K M V : Type*} [CommRing R] [IsDomain R] [Field K]
15   [Algebra R K] [IsFractionRing R K]
16   [AddCommGroup M] [Module R M]
17   [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V]
18 
19 /-- Every vector in a field span has a nonzero integral multiple in the integral span. -/
20 theorem exists_integral_multiple_of_mem_span (f : M →ₗ[R] V) (s : Set M)
21     {x : V} (hx : x ∈ Submodule.span K (f '' s)) :
22     ∃ d : R, d ≠ 0 ∧ ∃ y ∈ Submodule.span R s, f y = d • x := by
23   induction hx using Submodule.span_induction with
24   | mem x hx =>
25       obtain ⟨y, hy, rfl⟩ := hx
26       exact ⟨1, one_ne_zero, y, Submodule.subset_span hy, by simp⟩
27   | zero => exact ⟨1, one_ne_zero, 0, Submodule.zero_mem _, by simp⟩
28   | add x z _ _ hx hz =>
29       obtain ⟨d, hd, y, hy, hfy⟩ := hx
30       obtain ⟨e, he, w, hw, hfw⟩ := hz
31       refine ⟨d * e, mul_ne_zero hd he, e • y + d • w,
32         Submodule.add_mem _ (Submodule.smul_mem _ e hy) (Submodule.smul_mem _ d hw), ?_⟩
33       simp only [map_add, map_smul, hfy, hfw, smul_add, smul_smul, mul_comm e d]
34   | smul c x _ hx =>
35       obtain ⟨d, hd, y, hy, hfy⟩ := hx
36       obtain ⟨e, r, hr⟩ := IsLocalization.exists_integer_multiple (nonZeroDivisors R) c
37       refine ⟨(e : R) * d, mul_ne_zero (nonZeroDivisors.ne_zero e.property) hd,
38         r • y, Submodule.smul_mem _ r hy, ?_⟩
39       rw [map_smul, hfy]
40       calc
41         r • (d • x) = d • ((algebraMap R K r) • x) := by
42           rw [algebraMap_smul, smul_comm]
43         _ = d • (((e : R) • c) • x) := by rw [hr]
44         _ = ((e : R) * d) • (c • x) := by rw [smul_assoc, smul_smul, mul_comm d]
45 
46 /-- Finite generation permits one nonzero denominator for the entire integral module. -/
47 theorem exists_nonzero_smul_subset_of_span_eq_top [Module.Finite R M]
48     (f : M →ₗ[R] V) (hf : Function.Injective f) (s : Set M)
49     (hspan : Submodule.span K (f '' s) = ⊤) :
50     ∃ d : R, d ≠ 0 ∧ ∀ x : M, d • x ∈ Submodule.span R s := by
51   classical
52   obtain ⟨t, ht⟩ := Module.Finite.fg_top (R := R) (M := M)
53   have hlocal (x : M) : ∃ d : R, d ≠ 0 ∧ d • x ∈ Submodule.span R s := by
54     obtain ⟨d, hd, y, hy, he⟩ := exists_integral_multiple_of_mem_span f s
55       (x := f x) (by rw [hspan]; exact Submodule.mem_top)
56     have he' : y = d • x := hf (by simpa only [map_smul] using he)
57     exact ⟨d, hd, he' ▸ hy⟩
58   choose d hd hmem using hlocal
59   refine ⟨∏ x ∈ t, d x, Finset.prod_ne_zero_iff.mpr (fun x _ => hd x), ?_⟩
60   intro x
61   have hx : x ∈ Submodule.span R (t : Set M) := by rw [ht]; exact Submodule.mem_top
62   induction hx using Submodule.span_induction with
63   | mem y hy =>
64       have hm := (Submodule.span R s).smul_mem (∏ z ∈ t.erase y, d z) (hmem y)
65       simpa only [smul_smul, Finset.prod_erase_mul _ _ hy] using hm
66   | zero => simp
67   | add y z _ _ hy hz => simpa only [smul_add] using Submodule.add_mem _ hy hz
68   | smul a y _ hy => simpa only [smul_comm (∏ x ∈ t, d x) a] using
69       Submodule.smul_mem (Submodule.span R s) a hy
70 
71 /-- The entrywise coefficient embedding, as an integral linear map. -/
72 def matrixCoefficientMap {n : Type*} : Matrix n n R →ₗ[R] Matrix n n K where
73   toFun A := A.map (algebraMap R K)
74   map_add' A B := by ext i j; simp
75   map_smul' a A := by ext i j; simp [Algebra.smul_def]
76 
77 variable {n G : Type*} [Fintype n]
78 
79 /-- A full rational action span contains a fixed nonzero multiple of every integral matrix. -/
80 theorem exists_nonzero_smul_matrix_subset_span (τ : G → Matrix n n R)
81     (hspan : Submodule.span K
82       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤) :
83     ∃ d : R, d ≠ 0 ∧ ∀ A : Matrix n n R, d • A ∈ Submodule.span R (Set.range τ) := by
84   apply exists_nonzero_smul_subset_of_span_eq_top (K := K) (matrixCoefficientMap (K := K))
85   · intro A B h
86     ext i j
87     exact IsFractionRing.injective R K (congrFun (congrFun h i) j)
88   · rw [← Set.range_comp]
89     exact hspan
90 
91 /-- Over a DVR, the denominator can be chosen to be a power of a uniformizer. -/
92 theorem exists_uniformizer_power_matrix_subset_span [IsDiscreteValuationRing R]
93     (π : R) (hπ : Irreducible π) (τ : G → Matrix n n R)
94     (hspan : Submodule.span K
95       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤) :
96     ∃ c : ℕ, ∀ A : Matrix n n R, π ^ c • A ∈ Submodule.span R (Set.range τ) := by
97   obtain ⟨d, hd, hmem⟩ := exists_nonzero_smul_matrix_subset_span τ hspan
98   obtain ⟨c, u, hu⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hd hπ
99   refine ⟨c, fun A => ?_⟩
100   have hm := (Submodule.span R (Set.range τ)).smul_mem (↑(u⁻¹) : R) (hmem A)
101   simpa only [hu, smul_smul, ← mul_assoc, Units.inv_mul, one_mul] using hm
102 
103 section Density
104 
105 variable {F A W : Type*} [Field F] [Ring A] [Algebra F A]
106   [AddCommGroup W] [Module F W] [Module A W] [IsScalarTower F A W]
107   [IsSimpleModule A W] [FiniteDimensional F W]
108 
109 /-- Jacobson density becomes surjectivity when the commutant consists of scalars. -/
110 theorem surjective_module_action_of_scalar_commutant
111     (hscalar : Function.Surjective (algebraMap F (Module.End A W))) :
112     Function.Surjective (Module.toModuleEnd F (S := A) W) := by
113   classical
114   intro T
115   let T' : Module.End (Module.End A W) W :=
116     { T.toAddMonoidHom with
117       map_smul' := fun e x => by
118         obtain ⟨a, rfl⟩ := hscalar e
119         exact T.map_smul a x }
120   let b := Module.finBasis F W
121   obtain ⟨a, ha⟩ := jacobson_density T' (Finset.univ.image b)
122   refine ⟨a, b.ext fun i => ?_⟩
123   exact (ha (b i) (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩)).symm
124 
125 end Density
126 
127 section Representations
128 open scoped MonoidAlgebra
129 variable {F H W : Type*} [Field F] [Monoid H]
130   [AddCommGroup W] [Module F W] [FiniteDimensional F W]
131 
132 /-- Split irreducibility is recorded by irreducibility and an explicitly scalar commutant.
133 No algebraic-closure assumption is placed on a DVR fraction field. -/
134 theorem span_range_eq_top_of_split_irreducible (ρ : Representation F H W)
135     [Representation.IsIrreducible ρ]
136     (hscalar : Function.Surjective (algebraMap F (Module.End F[H] ρ.asModule))) :
137     Submodule.span F (Set.range ρ) = ⊤ := by
138   classical
139   apply top_unique
140   intro T _
141   let e := ρ.asModuleEquiv
142   let T' : Module.End F ρ.asModule := e.symm.toLinearMap.comp (T.comp e.toLinearMap)
143   obtain ⟨a, ha⟩ := surjective_module_action_of_scalar_commutant hscalar T'
144   have he : ρ.asAlgebraHom a = T := by
145     apply LinearMap.ext
146     intro x
147     have hx := LinearMap.congr_fun ha (e.symm x)
148     apply e.symm.injective
149     exact hx
150   rw [← he, Representation.asAlgebraHom_def, MonoidAlgebra.lift_apply, Finsupp.sum]
151   exact Submodule.sum_mem _ (fun g _ => Submodule.smul_mem _ _
152     (Submodule.subset_span (Set.mem_range_self g)))
153 
154 end Representations
155 
156 section MatrixRepresentations
157 open scoped MonoidAlgebra
158 variable {F H m : Type*} [Field F] [Monoid H] [Fintype m] [DecidableEq m]
159 
160 /-- The ordinary representation associated to actual action matrices. -/
161 def matrixRepresentation (τ : H →* Matrix m m F) : Representation F H (m → F) :=
162   Matrix.toLinAlgEquiv'.toMonoidHom.comp τ
163 
164 /-- Split irreducibility supplies the full matrix span required by denominator clearing. -/
165 theorem matrix_span_eq_top_of_split_irreducible (τ : H →* Matrix m m F)
166     [Representation.IsIrreducible (matrixRepresentation τ)]
167     (hscalar : Function.Surjective
168       (algebraMap F (Module.End F[H] (matrixRepresentation τ).asModule))) :
169     Submodule.span F (Set.range τ) = ⊤ := by
170   have hs := span_range_eq_top_of_split_irreducible (matrixRepresentation τ) hscalar
171   apply top_unique
172   intro A _
173   apply (Submodule.apply_mem_span_image_iff_mem_span
174     (f := Matrix.toLinAlgEquiv'.toLinearMap) Matrix.toLinAlgEquiv'.injective).mp
175   rw [← Set.range_comp]
176   change Matrix.toLinAlgEquiv' A ∈ Submodule.span F (Set.range (matrixRepresentation τ))
177   rw [hs]
178   exact Submodule.mem_top
179 
180 end MatrixRepresentations
181 
182 end PaperX.IntegralActionSpan

Back to source controls