QuadraticRootCompletion.lean

1 import PaperX.QuadraticAlgebra
2 import PaperX.Reconstruction
3 import PaperX.Compactness
4 import Mathlib.Data.Fintype.EquivFin
5 
6 /-! Actual quadratic roots and allowed root sets commute with adic completion.
7 The finite-level existence theorem uses positive precisions and does not assume
8 surjective reduction maps or a previously chosen compatible root family. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.QuadraticRootCompletion
12 open PaperX.QuadraticAlgebra
13 variable {R : Type} [CommRing R] (I : Ideal R)
14 
15 /-- Roots in all quotient rings, with actual quotient reduction compatibility. -/
16 @[ext] structure Family where
17   values : (n : ℕ) → Root (R ⧸ I ^ n)
18   compatible : ∀ {m n : ℕ} (h : m ≤ n),
19     mapRoot (Ideal.Quotient.factorPow I h) (values n) = values m
20 
21 def reduce (x : Root R) : Family I where
22   values n := mapRoot (Ideal.Quotient.mk (I ^ n)) x
23   compatible := by
24     intro m n h
25     apply Subtype.ext
26     simp
27 
28 /-- The compatible roots give actual points of the integer quadratic ring. -/
29 def pointFamily (x : Family I) : PaperX.Reconstruction.RingFamily (CoordinateRing ℤ) I where
30   maps n := (rootPoint ℤ (x.values n)).toRingHom
31   compatible := by
32     intro m n h
33     apply AdjoinRoot.ringHom_ext
34     · exact Subsingleton.elim _ _
35     · have hc := congrArg Subtype.val (x.compatible h)
36       change (Ideal.Quotient.factorPow I h)
37         ((rootPoint ℤ (x.values n)) (coordinate ℤ)) =
38           (rootPoint ℤ (x.values m)) (coordinate ℤ)
39       simpa only [rootPoint_coordinate, mapRoot_val] using hc
40 
41 /-- Reconstruction uses the checked ring-map reconstruction universal property. -/
42 def reconstruct [IsAdicComplete I R] (x : Family I) : Root R :=
43   let f := PaperX.Reconstruction.reconstruct I (pointFamily I x)
44   ⟨f (coordinate ℤ), by simpa only [map_pow, map_one] using congrArg f (coordinate_sq ℤ)⟩
45 
46 theorem reconstruct_reduces [IsAdicComplete I R] (x : Family I) (n : ℕ) :
47     mapRoot (Ideal.Quotient.mk (I ^ n)) (reconstruct I x) = x.values n := by
48   apply Subtype.ext
49   have h := congrArg (fun f : CoordinateRing ℤ →+* R ⧸ I ^ n => f (coordinate ℤ))
50     (PaperX.Reconstruction.reconstruct_reduces I (pointFamily I x) n)
51   simpa only [mapRoot_val, reconstruct, RingHom.comp_apply, pointFamily,
52     AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, rootPoint_coordinate] using h
53 
54 theorem root_ext [IsHausdorff I R] {x y : Root R}
55     (h : ∀ n, mapRoot (Ideal.Quotient.mk (I ^ n)) x =
56       mapRoot (Ideal.Quotient.mk (I ^ n)) y) : x = y := by
57   apply Subtype.ext
58   have H := IsHausdorff.funext' I (f := fun _ : Unit => x.val)
59     (g := fun _ : Unit => y.val) (fun n _ => congrArg Subtype.val (h n))
60   exact congrFun H ()
61 
62 theorem reconstruct_unique [IsAdicComplete I R] (x : Family I) (y : Root R)
63     (h : ∀ n, mapRoot (Ideal.Quotient.mk (I ^ n)) y = x.values n) :
64     y = reconstruct I x := by
65   apply root_ext I
66   intro n
67   rw [h n, reconstruct_reduces]
68 
69 theorem reconstruct_reduce [IsAdicComplete I R] (x : Root R) :
70     reconstruct I (reduce I x) = x :=
71   (reconstruct_unique I (reduce I x) x (fun _ => rfl)).symm
72 
73 theorem reduce_reconstruct [IsAdicComplete I R] (x : Family I) :
74     reduce I (reconstruct I x) = x := by
75   ext n
76   exact congrArg Subtype.val (reconstruct_reduces I x n)
77 
78 /-- Root-valued form of the universal property, with uniqueness. -/
79 def reconstructionEquiv [IsAdicComplete I R] : Root R ≃ Family I where
80   toFun := reduce I
81   invFun := reconstruct I
82   left_inv := reconstruct_reduce I
83   right_inv := reduce_reconstruct I
84 
85 /-- Only positive precisions are constrained. -/
86 structure Conditions where
87   allowed : (k : ℕ) → Root (R ⧸ I ^ (k + 1)) → Prop
88   downward : ∀ {j k : ℕ} (h : j ≤ k) x, allowed k x →
89     allowed j (mapRoot (Ideal.Quotient.factorPow I (Nat.add_le_add_right h 1)) x)
90 
91 def tower (C : Conditions I) : PaperX.Compactness.Tower where
92   Level k := {x : Root (R ⧸ I ^ (k + 1)) // C.allowed k x}
93   parent k x := ⟨mapRoot (Ideal.Quotient.factorPow I
94     (Nat.add_le_add_right (Nat.le_succ k) 1)) x.val, C.downward (Nat.le_succ k) _ x.property⟩
95 
96 def branchValue (C : Conditions I) (b : PaperX.Compactness.Branch (tower I C)) :
97     (n : ℕ) → Root (R ⧸ I ^ n)
98   | 0 => ⟨1, by simp⟩
99   | n + 1 => (b.value n).val
100 
101 theorem branchValue_compatible (C : Conditions I)
102     (b : PaperX.Compactness.Branch (tower I C)) {j k : ℕ} (h : j ≤ k) :
103     mapRoot (Ideal.Quotient.factorPow I h) (branchValue I C b k) =
104       branchValue I C b j := by
105   apply Subtype.ext
106   apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
107     (fun _ _ h => Ideal.pow_le_pow_right h)
108     (fun m => (branchValue I C b m).val) ?_ h).symm
109   intro m
110   cases m with
111   | zero =>
112     have : Subsingleton (R ⧸ I ^ 0) := by
113       simpa only [pow_zero, Ideal.one_eq_top] using (inferInstance : Subsingleton (R ⧸ (⊤ : Ideal R)))
114     exact Subsingleton.elim _ _
115   | succ m =>
116     exact (congrArg (fun x => x.val.val) (b.compatible m)).symm
117 
118 def branchFamily (C : Conditions I) (b : PaperX.Compactness.Branch (tower I C)) :
119     Family I where
120   values := branchValue I C b
121   compatible := branchValue_compatible I C b
122 
123 theorem finite_levels (C : Conditions I)
124     (finite : ∀ k, Finite {x : Root (R ⧸ I ^ (k + 1)) // C.allowed k x}) :
125     PaperX.Compactness.FiniteLevels (tower I C) := by
126   intro k
127   let : Finite ((tower I C).Level k) := finite k
128   let : Fintype ((tower I C).Level k) := Fintype.ofFinite _
129   classical
130   exact ⟨Finset.univ.toList, by simp⟩
131 
132 /-- The actual root has every required finite reduction. -/
133 def Realizes (C : Conditions I) (x : Root R) : Prop :=
134   ∀ k, C.allowed k (mapRoot (Ideal.Quotient.mk (I ^ (k + 1))) x)
135 
136 /-- Finite, nonempty, downward-closed positive levels suffice. -/
137 theorem exists_realization [IsAdicComplete I R] (C : Conditions I)
138     (finite : ∀ k, Finite {x : Root (R ⧸ I ^ (k + 1)) // C.allowed k x})
139     (occupied : ∀ k, ∃ x, C.allowed k x) :
140     ∃ x : Root R, Realizes I C x := by
141   obtain ⟨b⟩ := PaperX.Compactness.finite_branch_compactness (tower I C)
142     (finite_levels I C finite) (fun k => let ⟨x,h⟩ := occupied k; ⟨x,h⟩)
143   refine ⟨reconstruct I (branchFamily I C b), ?_⟩
144   intro k
145   rw [reconstruct_reduces]
146   exact (b.value k).property
147 
148 /-- Necessity does not need completeness or finiteness. -/
149 theorem levels_of_realization (C : Conditions I) (x : Root R) (h : Realizes I C x) :
150     ∀ k, ∃ y, C.allowed k y :=
151   fun k => ⟨mapRoot (Ideal.Quotient.mk (I ^ (k + 1))) x, h k⟩
152 
153 theorem realization_iff [IsAdicComplete I R] (C : Conditions I)
154     (finite : ∀ k, Finite {x : Root (R ⧸ I ^ (k + 1)) // C.allowed k x}) :
155     (∃ x : Root R, Realizes I C x) ↔ ∀ k, ∃ y, C.allowed k y :=
156   ⟨fun ⟨x,h⟩ => levels_of_realization I C x h, exists_realization I C finite⟩
157 
158 /-- Here finite quotient rings really do imply finite root levels. -/
159 theorem realization_iff_of_finite_quotients [IsAdicComplete I R] (C : Conditions I)
160     (finite : ∀ k, Finite (R ⧸ I ^ (k + 1))) :
161     (∃ x : Root R, Realizes I C x) ↔ ∀ k, ∃ y, C.allowed k y := by
162   apply realization_iff I C
163   intro k
164   let : Finite (R ⧸ I ^ (k + 1)) := finite k
165   infer_instance
166 
167 end PaperX.QuadraticRootCompletion

Back to source controls