MatrixWitnessLimits.lean

1 import PaperX.RepresentationLimits
2 
3 /-! Compatible finite matrices reconstruct to actual integral matrices.  Matrix
4 equations are proved after reconstruction using separatedness, independently
5 of any invertibility condition. -/
6 set_option autoImplicit false
7 
8 namespace PaperX.MatrixWitnessLimits
9 open PaperX.RepresentationLimits
10 
11 variable {R : Type*} [CommRing R] (I : Ideal R)
12 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
13 
14 /-- An actual compatible family of finite matrices, including precision zero. -/
15 structure MatrixFamily (R : Type*) [CommRing R] (I : Ideal R)
16     (ι : Type*) [Fintype ι] [DecidableEq ι] where
17   maps : ∀ k : ℕ, Matrix ι ι (R ⧸ I ^ k)
18   compatible : ∀ {j k : ℕ} (h : j ≤ k),
19     (maps k).map (Ideal.Quotient.factorPow I h) = maps j
20 
21 omit [Fintype ι] [DecidableEq ι] in
22 /-- Adjacent compatibility implies compatibility at every pair of precisions. -/
23 theorem matrix_compatible_of_succ
24     (a : ∀ k : ℕ, Matrix ι ι (R ⧸ I ^ k))
25     (ha : ∀ k, (a (k + 1)).map (Ideal.Quotient.factorPow I (Nat.le_succ k)) = a k)
26     {j k : ℕ} (h : j ≤ k) :
27     (a k).map (Ideal.Quotient.factorPow I h) = a j := by
28   ext i l
29   apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
30     (fun _ _ h => Ideal.pow_le_pow_right h) (fun m => a m i l) ?_ h).symm
31   intro m
32   exact (congrArg (fun M => M i l) (ha m)).symm
33 
34 def matrix_family_of_succ
35     (a : ∀ k : ℕ, Matrix ι ι (R ⧸ I ^ k))
36     (ha : ∀ k, (a (k + 1)).map (Ideal.Quotient.factorPow I (Nat.le_succ k)) = a k) :
37     MatrixFamily R I ι where
38   maps := a
39   compatible := matrix_compatible_of_succ I a ha
40 
41 noncomputable def reconstructMatrix [IsAdicComplete I R]
42     (f : MatrixFamily R I ι) : Matrix ι ι R :=
43   fun i j => scalarLift I (fun k => f.maps k i j)
44     (fun h => congrArg (fun M => M i j) (f.compatible h))
45 
46 @[simp] theorem reconstructMatrix_reduces [IsAdicComplete I R]
47     (f : MatrixFamily R I ι) (k : ℕ) :
48     (reconstructMatrix I f).map (Ideal.Quotient.mk (I ^ k)) = f.maps k := by
49   ext i j
50   exact scalarLift_reduces I (fun k => f.maps k i j)
51     (fun h => congrArg (fun M => M i j) (f.compatible h)) k
52 
53 /-- The lifted matrix is uniquely determined by its finite reductions. -/
54 theorem reconstructMatrix_unique [IsAdicComplete I R]
55     (f : MatrixFamily R I ι) (P : Matrix ι ι R)
56     (hP : ∀ k, P.map (Ideal.Quotient.mk (I ^ k)) = f.maps k) :
57     P = reconstructMatrix I f := by
58   apply matrix_ext I
59   intro k
60   rw [reconstructMatrix_reduces, hP]
61 
62 /-- Products of reconstructed matrices satisfy every compatible finite product
63 identity.  Invertibility is not supplied as a premise. -/
64 theorem reconstructMatrix_mul_eq [IsAdicComplete I R]
65     (a b c d : MatrixFamily R I ι)
66     (h : ∀ k, a.maps k * b.maps k = c.maps k * d.maps k) :
67     reconstructMatrix I a * reconstructMatrix I b =
68       reconstructMatrix I c * reconstructMatrix I d := by
69   apply matrix_ext I
70   intro k
71   simp only [Matrix.map_mul, reconstructMatrix_reduces]
72   exact h k
73 
74 variable {G : Type*} [Group G]
75 
76 /-- Actual finite intertwining equations survive reconstruction. -/
77 theorem reconstructMatrix_intertwines [IsAdicComplete I R]
78     (f g : Family R I G ι) (P : MatrixFamily R I ι)
79     (h : ∀ k x, f.maps k x * P.maps k = P.maps k * g.maps k x) (x : G) :
80     reconstruct I f x * reconstructMatrix I P =
81       reconstructMatrix I P * reconstruct I g x := by
82   apply matrix_ext I
83   intro k
84   simp only [Matrix.map_mul, reconstructMatrix_reduces]
85   change (liftMatrix I f x).map _ * P.maps k =
86     P.maps k * (liftMatrix I g x).map _
87   rw [liftMatrix_reduces, liftMatrix_reduces]
88   exact h k x
89 
90 /-- Local comparison uses a specified group homomorphism and a fixed actual
91 integral comparison representation. -/
92 theorem reconstructMatrix_local_intertwines {H : Type*} [Group H]
93     [IsAdicComplete I R] (f : Family R I G ι) (τ : MatrixRep R H ι)
94     (φ : H →* G) (P : MatrixFamily R I ι)
95     (h : ∀ k x, f.maps k (φ x) * P.maps k = P.maps k * reduce I τ k x) (x : H) :
96     reconstruct I f (φ x) * reconstructMatrix I P = reconstructMatrix I P * τ x := by
97   apply matrix_ext I
98   intro k
99   simp only [Matrix.map_mul, reconstructMatrix_reduces]
100   change (liftMatrix I f (φ x)).map _ * P.maps k =
101     P.maps k * reduce I τ k x
102   rw [liftMatrix_reduces]
103   exact h k x
104 
105 end PaperX.MatrixWitnessLimits

Back to source controls