CertificateBoundary.lean

1 import PaperX.CompletionExamples
2 import PaperX.RepresentationClasses
3 
4 /-! Exact comparison matrices can lose every fixed determinant certificate as
5 their precision grows.  This is an algebraic boundary, not a Galois example. -/
6 set_option autoImplicit false
7 namespace PaperX.CertificateBoundary
8 open scoped Matrix
9 open PaperX.CompletionBoundary PaperX.RepresentationLimits PaperX.RepresentationClasses
10 variable {R : Type*} [CommRing R]
11 
12 def nilpotent (a : R) : Matrix (Fin 2) (Fin 2) R := !![0,a;0,0]
13 
14 def comparison (a : R) : Matrix (Fin 2) (Fin 2) R := !![a,0;0,1]
15 
16 @[simp] theorem comparison_det (a : R) : (comparison a).det = a := by
17   simp [comparison, Matrix.det_fin_two]
18 
19 theorem comparison_intertwines (a : R) :
20     nilpotent a * comparison a = comparison a * nilpotent 1 := by
21   ext i j
22   fin_cases i <;> fin_cases j <;>
23     simp [nilpotent, comparison, Matrix.mul_apply, Fin.sum_univ_succ]
24 
25 theorem comparison_intertwines_representation (a : R) (g : Multiplicative ℤ) :
26     unipotent a g * comparison a = comparison a * unipotent 1 g := by
27   ext i j
28   fin_cases i <;> fin_cases j <;>
29     simp [unipotent, comparison, Matrix.mul_apply, Fin.sum_univ_succ]
30 
31 @[simp] theorem changeCoefficients_unipotent {S : Type*} [CommRing S]
32     (f : R →+* S) (a : R) : changeCoefficients f (unipotent a) = unipotent (f a) := by
33   apply MonoidHom.ext
34   intro g
35   ext i j
36   fin_cases i <;> fin_cases j <;> simp [changeCoefficients, unipotent]
37 
38 @[simp] theorem map_comparison {S : Type*} [CommRing S] (f : R →+* S) (a : R) :
39     (comparison a).map f = comparison (f a) := by
40   ext i j
41   fin_cases i <;> fin_cases j <;> simp [comparison]
42 
43 /-- All integral intertwiners have the forced determinant, including matrices
44 other than the displayed diagonal comparison. -/
45 theorem intertwiner_det (a : R) (P : Matrix (Fin 2) (Fin 2) R)
46     (h : nilpotent a * P = P * nilpotent 1) :
47     P.det = a * (P 1 1)^2 := by
48   have hc := congrArg (fun M : Matrix (Fin 2) (Fin 2) R => M 1 1) h
49   have ha := congrArg (fun M : Matrix (Fin 2) (Fin 2) R => M 0 1) h
50   simp [nilpotent, Matrix.mul_apply, Fin.sum_univ_succ] at hc ha
51   rw [Matrix.det_fin_two, ← ha, ← hc]
52   ring
53 
54 theorem representation_intertwiner_det (a : R) (P : Matrix (Fin 2) (Fin 2) R)
55     (h : ∀ g, unipotent a g * P = P * unipotent 1 g) :
56     P.det = a * (P 1 1)^2 := by
57   have H := h (Multiplicative.ofAdd (1 : ℤ))
58   have hc := congrArg (fun M : Matrix (Fin 2) (Fin 2) R => M 1 1) H
59   have ha := congrArg (fun M : Matrix (Fin 2) (Fin 2) R => M 0 1) H
60   simp [unipotent, Matrix.mul_apply, Fin.sum_univ_succ] at hc ha
61   have hc' : P 1 0 = 0 := hc
62   have ha' : P 0 0 = a * P 1 1 := by linear_combination -ha
63   rw [Matrix.det_fin_two, hc', ha']
64   ring
65 
66 /-- At every fixed precision, sufficiently deep approximants force every
67 integral comparison determinant to vanish, not just one chosen determinant. -/
68 theorem every_intertwiner_invisible (I : Ideal R) (π : R) (hπ : π ∈ I)
69     (k n : ℕ) (hkn : k ≤ n) (P : Matrix (Fin 2) (Fin 2) R)
70     (h : ∀ g, unipotent (π^n) g * P = P * unipotent 1 g) :
71     Ideal.Quotient.mk (I^k) P.det = 0 := by
72   rw [representation_intertwiner_det _ P h]
73   apply Ideal.Quotient.eq_zero_iff_mem.mpr
74   exact Ideal.mul_mem_right _ _ (Ideal.pow_le_pow_right hkn (Ideal.pow_mem_pow hπ n))
75 
76 theorem no_uniform_detecting_depth (I : Ideal R) (π : R) (hπ : π ∈ I) :
77     ¬ ∃ b : ℕ, ∀ n : ℕ, ∃ P : Matrix (Fin 2) (Fin 2) R,
78       (∀ g, unipotent (π^n) g * P = P * unipotent 1 g) ∧
79       Ideal.Quotient.mk (I^(b+1)) P.det ≠ 0 := by
80   rintro ⟨b, hb⟩
81   obtain ⟨P, hP, hdet⟩ := hb (b+1)
82   exact hdet (every_intertwiner_invisible I π hπ (b+1) (b+1) le_rfl P hP)
83 
84 theorem trivial_not_conjugate [Nontrivial R] :
85     ¬ Conjugate (unipotent (1 : R)) (unipotent 0) := by
86   intro h
87   obtain ⟨u, hu⟩ := conjugate_symm h
88   have H := congrArg
89     (fun ρ : MatrixRep R (Multiplicative ℤ) (Fin 2) =>
90       ρ (Multiplicative.ofAdd (1 : ℤ))) hu
91   simp only [conjugate_apply, trivial_apply, mul_one, Units.mul_inv] at H
92   have H01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) R => M 0 1) H
93   simp [unipotent] at H01
94 
95 section Field
96 variable {K : Type*} [Field K]
97 
98 /-- Every nonzero parameter gives an actual invertible change of basis over
99 the field. This does not give a bounded integral comparison determinant. -/
100 theorem field_conjugate (a : K) (ha : a ≠ 0) :
101     Conjugate (unipotent (1 : K)) (unipotent a) := by
102   let u := Matrix.nonsingInvUnit (comparison a)
103     (by simpa using (isUnit_iff_ne_zero.mpr ha : IsUnit a))
104   refine ⟨u, ?_⟩
105   apply MonoidHom.ext
106   intro g
107   change (u : Matrix (Fin 2) (Fin 2) K) * unipotent 1 g *
108     (↑(u⁻¹) : Matrix (Fin 2) (Fin 2) K) = _
109   have hu : (u : Matrix (Fin 2) (Fin 2) K) = comparison a := rfl
110   rw [hu, ← comparison_intertwines_representation]
111   rw [← hu, mul_assoc]
112   simp
113 
114 theorem every_nonzero_power_field_conjugate (π : K) (hπ : π ≠ 0) (n : ℕ) :
115     Conjugate (unipotent (1 : K)) (unipotent (π^n)) :=
116   field_conjugate _ (pow_ne_zero n hπ)
117 
118 end Field
119 end PaperX.CertificateBoundary

Back to source controls