MatrixSpanBound.lean

1 import PaperX.CertificateIsomorphisms
2 import PaperX.PrimitiveMatrix
3 import PaperX.IntegralActionSpan
4 import Mathlib.RingTheory.DiscreteValuationRing.Basic
5 import Mathlib.Data.Matrix.Basis
6 
7 /-! A full integral matrix span controls the denominator of a primitive
8 comparison uniformly across the representations compared with a fixed template. -/
9 set_option autoImplicit false
10 namespace PaperX.MatrixSpanBound
11 open PaperX.RepresentationLimits
12 variable {R G ι : Type*} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
13 
14 /-- Intertwining extends from the group action to its integral linear span. -/
15 theorem intertwining_on_span (ρ τ : MatrixRep R G ι) (P : Matrix ι ι R)
16     (hP : ∀ g, ρ g * P = P * τ g)
17     {A : Matrix ι ι R} (hA : A ∈ Submodule.span R (Set.range τ)) :
18     ∃ C : Matrix ι ι R, C * P = P * A := by
19   induction hA using Submodule.span_induction with
20   | mem A hA =>
21       obtain ⟨g, rfl⟩ := hA
22       exact ⟨ρ g, hP g⟩
23   | zero => exact ⟨0, by simp⟩
24   | add A B _ _ hA hB =>
25       obtain ⟨C, hC⟩ := hA
26       obtain ⟨D, hD⟩ := hB
27       exact ⟨C + D, by simp [add_mul, mul_add, hC, hD]⟩
28   | smul a A _ hA =>
29       obtain ⟨C, hC⟩ := hA
30       exact ⟨a • C, by rw [Matrix.smul_mul, hC, Matrix.mul_smul]⟩
31 
32 /-- A unit entry and a scalar-full matrix span give an integral left
33 comparison. This constructs the matrix rather than assuming a bounded inverse. -/
34 theorem factorization_of_unit_entry (ρ τ : MatrixRep R G ι)
35     (P : Matrix ι ι R) (hP : ∀ g, ρ g * P = P * τ g)
36     (a : R) (hspan : ∀ M : Matrix ι ι R,
37       a • M ∈ Submodule.span R (Set.range τ))
38     (i₀ j₀ : ι) (hu : IsUnit (P i₀ j₀)) :
39     ∃ B : Matrix ι ι R, B * P = a • (1 : Matrix ι ι R) := by
40   classical
41   obtain ⟨u, hu⟩ := hu
42   have hC : ∀ k : ι, ∃ C : Matrix ι ι R,
43       C * P = P * (a • Matrix.single j₀ k 1) := fun k =>
44     intertwining_on_span ρ τ P hP (hspan _)
45   choose C hC using hC
46   let B : Matrix ι ι R := fun k l => (↑(u⁻¹) : R) * C k i₀ l
47   refine ⟨B, ?_⟩
48   ext k l
49   have hc := congrArg (fun M : Matrix ι ι R => M i₀ l) (hC k)
50   have hb : (B * P) k l = (↑(u⁻¹) : R) * (C k * P) i₀ l := by
51     change (∑ j, ((↑(u⁻¹) : R) * (C k) i₀ j) * P j l) =
52       (↑(u⁻¹) : R) * ∑ j, (C k) i₀ j * P j l
53     simp only [Finset.mul_sum, mul_assoc]
54   rw [hb, hc, Matrix.mul_smul]
55   by_cases hl : l = k
56   · subst l
57     simp [Matrix.mul_single_apply_same, ← hu, mul_assoc, mul_comm]
58   · simp [Matrix.mul_single_apply_of_ne (1 : R) j₀ k i₀ l hl P, Ne.symm hl]
59 
60 /-- Taking determinants gives the uniform divisibility bound. -/
61 theorem det_dvd_scalar_power (P B : Matrix ι ι R) (a : R)
62     (h : B * P = a • (1 : Matrix ι ι R)) :
63     P.det ∣ a ^ Fintype.card ι := by
64   refine ⟨B.det, ?_⟩
65   have hd := congrArg Matrix.det h
66   simpa only [Matrix.det_mul, Matrix.det_smul, Matrix.det_one, mul_one, mul_comm] using hd.symm
67 
68 /-- A primitive integral comparison has determinant dividing the scalar
69 matrix-span bound to the matrix rank. -/
70 theorem primitive_det_dvd (ρ τ : MatrixRep R G ι) (P : Matrix ι ι R)
71     (hP : ∀ g, ρ g * P = P * τ g) (a : R)
72     (hspan : ∀ M : Matrix ι ι R, a • M ∈ Submodule.span R (Set.range τ))
73     (hunit : ∃ i j, IsUnit (P i j)) : P.det ∣ a ^ Fintype.card ι := by
74   obtain ⟨i, j, hij⟩ := hunit
75   obtain ⟨B, hB⟩ := factorization_of_unit_entry ρ τ P hP a hspan i j hij
76   exact det_dvd_scalar_power P B a hB
77 
78 section Detector
79 variable [IsDomain R]
80 
81 /-- Dividing a fixed power gives nonvanishing one precision higher.
82 This implication needs only a nonzero nonunit, not the DVR hypothesis. -/
83 theorem nonzero_reduction_of_dvd_power (π x : R) (hπ : π ≠ 0)
84     (hnunit : ¬ IsUnit π) (m : ℕ) (hdiv : x ∣ π ^ m) :
85     Ideal.Quotient.mk ((Ideal.span {π}) ^ (m + 1)) x ≠ 0 := by
86   intro hzero
87   have hmem := Ideal.Quotient.eq_zero_iff_mem.mp hzero
88   rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hmem
89   obtain ⟨b, hb⟩ := hmem.trans hdiv
90   have hc : (1 : R) = π * b :=
91     mul_left_cancel₀ (pow_ne_zero m hπ) (by simpa [pow_succ, mul_assoc] using hb)
92   exact hnunit (isUnit_iff_dvd_one.mpr ⟨b, hc⟩)
93 
94 /-- A fixed scalar matrix-span exponent produces one determinant detector
95 for every primitive integral comparison with the template. -/
96 theorem primitive_comparison_detector (ρ τ : MatrixRep R G ι)
97     (P : Matrix ι ι R) (hP : ∀ g, ρ g * P = P * τ g)
98     (π : R) (hπ : π ≠ 0) (hnunit : ¬ IsUnit π) (c : ℕ)
99     (hspan : ∀ M : Matrix ι ι R,
100       π ^ c • M ∈ Submodule.span R (Set.range τ))
101     (hunit : ∃ i j, IsUnit (P i j)) :
102     (P.map (Ideal.Quotient.mk
103       ((Ideal.span {π}) ^ (c * Fintype.card ι + 1)))).det ≠ 0 := by
104   have hd : P.det ∣ π ^ (c * Fintype.card ι) := by
105     simpa only [pow_mul] using primitive_det_dvd ρ τ P hP (π ^ c) hspan hunit
106   have hz := nonzero_reduction_of_dvd_power π P.det hπ hnunit
107     (c * Fintype.card ι) hd
108   change ((Ideal.Quotient.mk
109     ((Ideal.span {π}) ^ (c * Fintype.card ι + 1))).mapMatrix P).det ≠ 0
110   rwa [← RingHom.map_det]
111 
112 end Detector
113 section Uniform
114 variable [IsDomain R] [IsDiscreteValuationRing R]
115 variable {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
116 
117 /-- Starting from a nonzero field intertwiner, both primitive normalization
118 and the bounded determinant certificate are constructed. -/
119 theorem exists_bounded_comparison (ρ τ : MatrixRep R G ι)
120     (π : R) (hπ : Irreducible π) (c : ℕ)
121     (hspan : ∀ M : Matrix ι ι R,
122       π ^ c • M ∈ Submodule.span R (Set.range τ))
123     (Q : Matrix ι ι K) (hQ : Q ≠ 0)
124     (hinter : ∀ g, (ρ g).map (algebraMap R K) * Q =
125       Q * (τ g).map (algebraMap R K)) :
126     ∃ P : Matrix ι ι R, (∀ g, ρ g * P = P * τ g) ∧
127       (P.map (Ideal.Quotient.mk
128         ((Ideal.span {π}) ^ (c * Fintype.card ι + 1)))).det ≠ 0 := by
129   obtain ⟨s, P, _, _, hunit, hP⟩ :=
130     PrimitiveMatrix.intertwiner_normalization (R := R) ρ τ Q hQ hinter
131   refine ⟨P, hP, primitive_comparison_detector ρ τ P hP π
132     hπ.ne_zero hπ.not_isUnit c hspan ?_⟩
133   obtain ⟨i, j, hij⟩ := hunit
134   exact ⟨i, j, by rw [hij]; exact isUnit_one⟩
135 
136 /-- One depth works uniformly across all integral representations admitting
137 a nonzero field comparison with a fixed template whose field action spans
138 all matrices. The exponent is obtained from the template alone. -/
139 theorem exists_uniform_detector (τ : MatrixRep R G ι) (π : R)
140     (hπ : Irreducible π)
141     (hspan : Submodule.span K
142       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤) :
143     ∃ c : ℕ, ∀ (ρ : MatrixRep R G ι) (Q : Matrix ι ι K), Q ≠ 0 →
144       (∀ g, (ρ g).map (algebraMap R K) * Q =
145         Q * (τ g).map (algebraMap R K)) →
146       ∃ P : Matrix ι ι R, (∀ g, ρ g * P = P * τ g) ∧
147         (P.map (Ideal.Quotient.mk
148           ((Ideal.span {π}) ^ (c * Fintype.card ι + 1)))).det ≠ 0 := by
149   obtain ⟨c, hc⟩ := IntegralActionSpan.exists_uniformizer_power_matrix_subset_span
150     π hπ τ hspan
151   exact ⟨c, fun ρ Q hQ hinter => exists_bounded_comparison ρ τ π hπ c hc Q hQ hinter⟩
152 
153 open PaperX.RepresentationClasses in
154 /-- Every integral representation in the field-isomorphism class of a
155 fixed full-span template admits a comparison with one common detecting depth.
156 The empty-rank case is included. -/
157 theorem uniform_detector_for_conjugates (τ : MatrixRep R G ι) (π : R)
158     (hπ : Irreducible π)
159     (hspan : Submodule.span K
160       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤) :
161     ∃ c : ℕ, ∀ ρ : MatrixRep R G ι,
162       Conjugate (changeCoefficients (algebraMap R K) τ)
163         (changeCoefficients (algebraMap R K) ρ) →
164       ∃ P : Matrix ι ι R, (∀ g, ρ g * P = P * τ g) ∧
165         (P.map (Ideal.Quotient.mk
166           ((Ideal.span {π}) ^ (c * Fintype.card ι + 1)))).det ≠ 0 := by
167   classical
168   cases isEmpty_or_nonempty ι with
169   | inl hempty =>
170       let := hempty
171       refine ⟨0, fun ρ _ => ⟨1, ?_, ?_⟩⟩
172       · intro g
173         ext i
174         exact isEmptyElim i
175       · change ((Ideal.Quotient.mk
176           ((Ideal.span {π}) ^ (0 * Fintype.card ι + 1))).mapMatrix
177           (1 : Matrix ι ι R)).det ≠ 0
178         rw [← RingHom.map_det, Matrix.det_one]
179         rw [Nat.zero_mul]
180         exact nonzero_reduction_of_dvd_power π 1 hπ.ne_zero hπ.not_isUnit 0
181           (by simp)
182   | inr hnonempty =>
183       let := hnonempty
184       obtain ⟨c, hc⟩ := exists_uniform_detector τ π hπ hspan
185       refine ⟨c, fun ρ hρ => ?_⟩
186       obtain ⟨u, hu⟩ := hρ
187       apply hc ρ (u : Matrix ι ι K) u.ne_zero
188       intro g
189       have he := congrArg (fun r : MatrixRep K G ι => r g) hu
190       change (u : Matrix ι ι K) * (τ g).map (algebraMap R K) *
191         (↑(u⁻¹) : Matrix ι ι K) = (ρ g).map (algebraMap R K) at he
192       rw [← he, mul_assoc, mul_assoc]
193       simp
194 
195 end Uniform
196 end PaperX.MatrixSpanBound

Back to source controls