PrecisionAveraging.lean

1 import PaperX.FiniteGroupAveraging
2 import Mathlib.RingTheory.LocalRing.Quotient
3 import Mathlib.Tactic.LinearCombination
4 import Mathlib.Tactic.Ring
5 
6 /-! Finite-group averaging with a controlled loss of coefficient precision.
7 The group order may be a nonunit, but must be nonzero and divide a specified
8 power of the ideal generator.  Cancellation is performed in the integral domain,
9 without supplying a fraction-field comparison. -/
10 set_option autoImplicit false
11 
12 namespace PaperX.PrecisionAveraging
13 open PaperX.RepresentationLimits PaperX.RepresentationClasses
14 open PaperX.FiniteGroupAveraging
15 open scoped BigOperators
16 
17 variable {R : Type*} [CommRing R] [IsDomain R]
18 variable {Γ : Type*} [Group Γ] [Fintype Γ]
19 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
20 
21 omit [IsDomain R] in
22 /-- The unnormalized group sum is always an exact intertwiner. -/
23 theorem sum_intertwines (ρ τ : MatrixRep R Γ ι)
24     (A : Matrix ι ι R) (h : Γ) :
25     ρ h * (∑ g : Γ, ρ g * A * τ g⁻¹) =
26       (∑ g : Γ, ρ g * A * τ g⁻¹) * τ h := by
27   rw [Finset.mul_sum, Finset.sum_mul]
28   refine Fintype.sum_bijective (h * ·) (Group.mulLeft_bijective h) _ _ fun g => ?_
29   have hcancel : τ h⁻¹ * τ h = 1 := by rw [← map_mul, inv_mul_cancel, map_one]
30   simp only [mul_inv_rev, map_mul, mul_assoc, hcancel, mul_one]
31 
32 /-- An approximate intertwiner at depth `e+k` can be corrected to an exact
33 integral intertwiner while retaining its reduction at depth `k`. -/
34 theorem correct_intertwiner (π : R) (e k : ℕ)
35     (ρ τ : MatrixRep R Γ ι) (hΓ : (Fintype.card Γ : R) ≠ 0)
36     (hdiv : (Fintype.card Γ : R) ∣ π^e) (A : Matrix ι ι R)
37     (hA : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) *
38         A.map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) =
39       A.map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) *
40         (τ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
41     ∃ P : Matrix ι ι R,
42       P.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
43         A.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) ∧
44       ∀ g, ρ g * P = P * τ g := by
45   classical
46   let I : Ideal R := Ideal.span {π}
47   let f := Ideal.Quotient.mk (I^(e+k))
48   let a : R := Fintype.card Γ
49   let S : Matrix ι ι R := ∑ g : Γ, ρ g * A * τ g⁻¹
50   have hterm (g : Γ) : (ρ g * A * τ g⁻¹).map f = A.map f := by
51     rw [Matrix.map_mul, Matrix.map_mul, hA, mul_assoc, ← Matrix.map_mul,
52       ← map_mul, mul_inv_cancel, map_one, Matrix.map_one, mul_one] <;> simp
53   have hsum : S.map f = (a • A).map f := by
54     change f.mapMatrix (∑ g : Γ, ρ g * A * τ g⁻¹) = _
55     rw [map_sum]
56     simp only [RingHom.mapMatrix_apply, hterm, Finset.sum_const, Finset.card_univ]
57     ext i j
58     simp [a, Matrix.map_apply, nsmul_eq_mul]
59   have hentry (i j : ι) : π^(e+k) ∣ S i j - a * A i j := by
60     rw [← Ideal.mem_span_singleton, ← Ideal.span_singleton_pow]
61     apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp
62     exact congrArg (fun M => M i j) hsum
63   choose E hE using hentry
64   obtain ⟨b, hb⟩ := hdiv
65   let P : Matrix ι ι R := fun i j => A i j + (b * π^k) * E i j
66   have heq : a • P = S := by
67     ext i j
68     have H := hE i j
69     change S i j - a * A i j = π^(e+k) * E i j at H
70     change a * (A i j + (b * π^k) * E i j) = S i j
71     rw [pow_add, hb] at H
72     dsimp [a] at *
73     linear_combination -H
74   refine ⟨P, ?_, ?_⟩
75   · ext i j
76     apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
77     rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton]
78     refine ⟨b * E i j, ?_⟩
79     change A i j + (b * π^k) * E i j - A i j = π^k * (b * E i j)
80     ring
81   · intro g
82     have H := sum_intertwines ρ τ A g
83     change ρ g * S = S * τ g at H
84     rw [← heq, Matrix.mul_smul, Matrix.smul_mul] at H
85     ext i j
86     apply mul_left_cancel₀ hΓ
87     exact congrArg (fun M => M i j) H
88 
89 
90 /-- A prescribed quotient intertwiner lifts after losing at most `e` powers
91 of the principal ideal.  The higher-depth quotient matrix need not itself admit
92 an exact lift with its entire original reduction. -/
93 theorem exists_intertwiner_lift (π : R) (e k : ℕ)
94     (ρ τ : MatrixRep R Γ ι) (hΓ : (Fintype.card Γ : R) ≠ 0)
95     (hdiv : (Fintype.card Γ : R) ∣ π^e)
96     (B : Matrix ι ι (R ⧸ (Ideal.span {π})^(e+k)))
97     (hB : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) * B =
98       B * (τ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
99     ∃ P : Matrix ι ι R,
100       P.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
101         B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) ∧
102       ∀ g, ρ g * P = P * τ g := by
103   obtain ⟨A, hA⟩ := PaperX.FiniteGroupAveraging.exists_matrix_lift
104     (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) Ideal.Quotient.mk_surjective B
105   obtain ⟨P, hP, hρ⟩ := correct_intertwiner π e k ρ τ hΓ hdiv A
106     (by simpa only [hA] using hB)
107   refine ⟨P, hP.trans ?_, hρ⟩
108   rw [← hA]
109   ext i j
110   simp
111 
112 omit [IsDomain R] in
113 /-- Every positive quotient by a nonunit principal ideal has a unit-reflecting
114 quotient map over a local ring. -/
115 theorem positive_quotient_local [IsLocalRing R] (π : R)
116     (hπ : ¬ IsUnit π) (k : ℕ) (hk : 0 < k) :
117     IsLocalHom (Ideal.Quotient.mk ((Ideal.span {π})^k)) := by
118   have hI : (Ideal.span {π} : Ideal R)^k ≠ ⊤ := by
119     rw [Ideal.span_singleton_pow]
120     intro h
121     exact hπ ((isUnit_pow_iff hk.ne').mp (Ideal.span_singleton_eq_top.mp h))
122   let : Nontrivial (R ⧸ (Ideal.span {π})^k) := Ideal.Quotient.nontrivial_iff.mpr hI
123   exact IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
124 
125 /-- An invertible approximate comparison yields an integral isomorphism, with
126 its prescribed comparison retained at the lower positive precision. -/
127 theorem exists_isomorphism_lift [IsLocalRing R] (π : R) (e k : ℕ)
128     (ρ τ : MatrixRep R Γ ι) (hΓ : (Fintype.card Γ : R) ≠ 0)
129     (hdiv : (Fintype.card Γ : R) ∣ π^e) (hπ : ¬ IsUnit π) (hk : 0 < k)
130     (B : (Matrix ι ι (R ⧸ (Ideal.span {π})^(e+k)))ˣ)
131     (hB : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) *
132         (B : Matrix ι ι _) =
133       (B : Matrix ι ι _) * (τ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
134     ∃ P : (Matrix ι ι R)ˣ,
135       (P : Matrix ι ι R).map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
136         (B : Matrix ι ι _).map
137           (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) ∧
138       ∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g := by
139   obtain ⟨P, hP, hρ⟩ := exists_intertwiner_lift π e k ρ τ hΓ hdiv B hB
140   let f := Ideal.Quotient.mk ((Ideal.span {π})^k)
141   let : IsLocalHom f := positive_quotient_local π hπ k hk
142   have hu : IsUnit (P.map f) := by
143     rw [hP]
144     exact B.isUnit.map
145       (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)).mapMatrix
146   obtain ⟨u, hu⟩ := matrix_isUnit_of_map f P hu
147   exact ⟨u, by simpa only [hu] using hP, by simpa only [hu] using hρ⟩
148 
149 /-- Finite precision `e+k` detects integral isomorphism for every positive `k`.
150 The comparison matrix constructed from the finite isomorphism agrees with it
151 at precision `k`, rather than necessarily at the entire input precision. -/
152 theorem conjugacy_iff_reduction [IsLocalRing R] (π : R) (e k : ℕ)
153     (ρ τ : MatrixRep R Γ ι) (hΓ : (Fintype.card Γ : R) ≠ 0)
154     (hdiv : (Fintype.card Γ : R) ∣ π^e) (hπ : ¬ IsUnit π) (hk : 0 < k) :
155     Conjugate (reduce (Ideal.span {π}) τ (e+k))
156       (reduce (Ideal.span {π}) ρ (e+k)) ↔ Conjugate τ ρ := by
157   constructor
158   · rintro ⟨B, hB⟩
159     have hinter (g : Γ) :
160         (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) *
161             (B : Matrix ι ι _) =
162           (B : Matrix ι ι _) *
163             (τ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) := by
164       change reduce (Ideal.span {π}) ρ (e+k) g * (B : Matrix ι ι _) =
165         (B : Matrix ι ι _) * reduce (Ideal.span {π}) τ (e+k) g
166       rw [← hB]
167       simp only [conjugate_apply, mul_assoc, Units.inv_mul, mul_one]
168     obtain ⟨P, _, hP⟩ := exists_isomorphism_lift π e k ρ τ hΓ hdiv hπ hk B hinter
169     refine ⟨P, MonoidHom.ext fun g => ?_⟩
170     change (P : Matrix ι ι R) * τ g * (↑(P⁻¹) : Matrix ι ι R) = ρ g
171     rw [← hP, mul_assoc]
172     simp
173   · exact changeCoefficients_conjugacy (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))
174 
175 end PaperX.PrecisionAveraging

Back to source controls