CompletionBoundary.lean

1 import PaperX.CommonSpine
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 import Mathlib.NumberTheory.Padics.RingHoms
4 import Mathlib.Tactic
5 
6 /-! A boundary for arbitrary local conditions: nontrivial representations are
7 not adically closed. Each nontrivial unipotent representation below becomes
8 invisible to any fixed finite precision, while the limiting representation is
9 trivial. This refutes automatic preservation of arbitrary properties. -/
10 set_option autoImplicit false
11 namespace PaperX.CompletionBoundary
12 open scoped Matrix
13 open PaperX.RepresentationLimits
14 variable {R : Type*} [CommRing R]
15 
16 /-- A genuine representation of the additive integers (written multiplicatively). -/
17 def unipotent (a : R) : MatrixRep R (Multiplicative ℤ) (Fin 2) where
18   toFun g := !![1, a * (Multiplicative.toAdd g : ℤ); 0, 1]
19   map_one' := by
20     ext i j
21     fin_cases i <;> fin_cases j <;> simp
22   map_mul' g h := by
23     ext i j
24     fin_cases i <;> fin_cases j <;>
25       simp [Matrix.mul_apply, Fin.sum_univ_succ, mul_add, add_comm]
26 
27 /-- This supplies an actual matrix distinction, not just a descriptive label. -/
28 theorem unipotent_ne_trivial {a : R} (ha : a ≠ 0) : unipotent a ≠ unipotent (0 : R) := by
29   intro he
30   have H := congrArg (fun ρ => ρ (Multiplicative.ofAdd (1 : ℤ)) (0 : Fin 2) (1 : Fin 2)) he
31   exact ha (by simpa [unipotent] using H)
32 
33 @[simp] theorem trivial_apply (g : Multiplicative ℤ) : unipotent (0 : R) g = 1 := by
34   ext i j
35   fin_cases i <;> fin_cases j <;> simp [unipotent]
36 
37 /-- A parameter in I^k is invisible to precision k. -/
38 theorem invisible_parameter (I : Ideal R) (k : ℕ) {a : R} (ha : a ∈ I^k) :
39     reduce I (unipotent a) k = reduce I (unipotent (0 : R)) k := by
40   have hz : Ideal.Quotient.mk (I^k) a = 0 := Ideal.Quotient.eq_zero_iff_mem.mpr ha
41   apply MonoidHom.ext
42   intro g
43   apply Matrix.ext
44   intro i j
45   fin_cases i <;> fin_cases j <;> simp [reduce, unipotent, hz]
46 
47 /-- Every finite neighborhood of the trivial representation contains a nontrivial
48 one, whenever I contains a nonzero element in a domain. -/
49 theorem nontrivial_approximations [IsDomain R] (I : Ideal R) (π : R)
50     (hne : π ≠ 0) (hπ : π ∈ I) :
51     ∀ k, ∃ ρ : MatrixRep R (Multiplicative ℤ) (Fin 2),
52       ρ ≠ unipotent (0 : R) ∧ reduce I ρ k = reduce I (unipotent (0 : R)) k := by
53   intro k
54   refine ⟨unipotent (π^k), unipotent_ne_trivial (pow_ne_zero k hne), ?_⟩
55   apply invisible_parameter
56   exact Ideal.pow_mem_pow hπ k
57 
58 /-- Higher and higher unipotent parameters vanish at every fixed precision. -/
59 theorem eventually_trivial_reduction (I : Ideal R) (π : R) (hπ : π ∈ I)
60     (k n : ℕ) (hkn : k ≤ n) :
61     reduce I (unipotent (π^n)) k = reduce I (unipotent (0 : R)) k := by
62   apply invisible_parameter
63   exact Ideal.pow_le_pow_right hkn (Ideal.pow_mem_pow hπ n)
64 
65 /-- Literal topological convergence of the representation matrices at every
66 integer group element, not just a finite congruence experiment. -/
67 theorem unipotent_tendsto (I : Ideal R) (π : R) (hπ : π ∈ I)
68     (g : Multiplicative ℤ) :
69     letI : TopologicalSpace R := I.adicTopology
70     Filter.Tendsto (fun n : ℕ => unipotent (π^n) g) Filter.atTop (nhds (1 : Matrix (Fin 2) (Fin 2) R)) := by
71   let : TopologicalSpace R := I.adicTopology
72   apply tendsto_pi_nhds.mpr
73   intro i
74   apply tendsto_pi_nhds.mpr
75   intro j
76   apply PaperX.RepresentationTopology.adic_tendsto_of_reductions I
77   intro k
78   apply Filter.eventually_atTop.mpr
79   refine ⟨k, ?_⟩
80   intro n hn
81   have H := congrArg (fun ρ => ρ g i j) (eventually_trivial_reduction I π hπ k n hn)
82   simpa [reduce, changeCoefficients] using H
83 
84 /-- The adic-closure implication is genuinely false for the property of being
85 nontrivial. Increasing precision does not make arbitrary local properties stable. -/
86 theorem nontrivial_not_limit_stable [IsDomain R] (I : Ideal R) (π : R)
87     (hne : π ≠ 0) (hπ : π ∈ I) :
88     ¬ (∀ ρ : MatrixRep R (Multiplicative ℤ) (Fin 2),
89       (∀ k, ∃ τ, τ ≠ unipotent (0 : R) ∧ reduce I τ k = reduce I ρ k) →
90       ρ ≠ unipotent (0 : R)) := by
91   intro h
92   exact h (unipotent (0 : R)) (nontrivial_approximations I π hne hπ) rfl
93 
94 /-- A compatible family is reconstructed uniquely, but not with an arbitrary
95 property shared by all approximating representatives. -/
96 theorem trivial_reconstructs (I : Ideal R) [IsAdicComplete I R] :
97     reconstruct I (reduceFamily I (unipotent (0 : R))) = unipotent (0 : R) :=
98   reconstruct_reduce I _
99 
100 /-- All scalar congruences 2*x=1 modulo odd powers are solvable. -/
101 theorem inverse_two_mod_three_power (k : ℕ) :
102     ∃ x : ZMod (3^k), 2*x = 1 := by
103   have hc : Nat.Coprime 2 (3^k) := (by decide : Nat.Coprime 2 3).pow_right k
104   have hu : IsUnit (2 : ZMod (3^k)) := (ZMod.isUnit_iff_coprime 2 (3^k)).mpr hc
105   obtain ⟨u,hu⟩ := hu
106   exact ⟨↑u⁻¹, by rw [← hu]; simp⟩
107 
108 /-- Completeness cannot be dropped just because every scalar congruence is solvable. -/
109 theorem no_integer_inverse_two : ¬ ∃ x : ℤ, 2*x = 1 := by omega
110 
111 end PaperX.CompletionBoundary

Back to source controls