Reconstruction.lean

1 import Mathlib.RingTheory.AdicCompletion.RingHom
2 import Mathlib.RingTheory.LocalRing.RingHom.Basic
3 import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
4 
5 /-!
6 Paper X Block 02. The represented-point reconstruction theorem is implemented
7 using actual Mathlib ring homomorphisms and ideal-power quotients, rather than
8 an assumed bijection of sets. Completeness is an explicit coefficient-ring
9 hypothesis. Locality and adic continuity are proved separately below.
10 The universal lifting theorem is Mathlib's IsAdicComplete.liftRingHom.
11 -/
12 set_option autoImplicit false
13 namespace PaperX.Reconstruction
14 
15 variable {R S : Type*} [CommRing R] [CommRing S]
16 
17 /-- Compatible maps at all ideal-power precisions. Level zero is the trivial
18 quotient and is included solely to match Mathlib's indexing. -/
19 @[ext] structure RingFamily (R : Type*) [CommRing R] (I : Ideal S) where
20   maps : (n : ℕ) → R →+* S ⧸ I ^ n
21   compatible : ∀ {m n : ℕ} (h : m ≤ n),
22     (Ideal.Quotient.factorPow I h).comp (maps n) = maps m
23 
24 variable (I : Ideal S)
25 
26 def reduce (F : R →+* S) : RingFamily R I where
27   maps n := (Ideal.Quotient.mk (I ^ n)).comp F
28   compatible := by
29     intro m n h
30     ext x
31     simp
32 
33 noncomputable def reconstruct [IsAdicComplete I S] (f : RingFamily R I) : R →+* S :=
34   IsAdicComplete.liftRingHom I f.maps f.compatible
35 
36 theorem reconstruct_reduces [IsAdicComplete I S] (f : RingFamily R I) (n : ℕ) :
37     (Ideal.Quotient.mk (I ^ n)).comp (reconstruct I f) = f.maps n :=
38   IsAdicComplete.mk_comp_liftRingHom I f.maps f.compatible n
39 
40 theorem reconstruct_unique [IsAdicComplete I S] (f : RingFamily R I) (F : R →+* S)
41     (h : ∀ n, (Ideal.Quotient.mk (I ^ n)).comp F = f.maps n) :
42     F = reconstruct I f :=
43   IsAdicComplete.eq_liftRingHom I f.maps f.compatible F h
44 
45 theorem reconstruct_reduce [IsAdicComplete I S] (F : R →+* S) :
46     reconstruct I (reduce I F) = F :=
47   (reconstruct_unique I (reduce I F) F (fun _ => rfl)).symm
48 
49 theorem reduce_reconstruct [IsAdicComplete I S] (f : RingFamily R I) :
50     reduce I (reconstruct I f) = f := by
51   ext n x
52   exact congrArg (fun F : R →+* S ⧸ I ^ n => F x) (reconstruct_reduces I f n)
53 
54 /-- The genuine ring-map version of Paper X's inverse-limit reconstruction. -/
55 noncomputable def ringReconstructionEquiv [IsAdicComplete I S] :
56     (R →+* S) ≃ RingFamily R I where
57   toFun := reduce I
58   invFun := reconstruct I
59   left_inv := reconstruct_reduce I
60   right_inv := reduce_reconstruct I
61 
62 /-- Completeness does not assert existence of compatible finite maps. -/
63 theorem ring_maps_nonempty_iff [IsAdicComplete I S] :
64     Nonempty (R →+* S) ↔ Nonempty (RingFamily R I) :=
65   ⟨fun ⟨F⟩ => ⟨reduce I F⟩, fun ⟨f⟩ => ⟨reconstruct I f⟩⟩
66 
67 /-- Precomposition is compatible with reconstruction, giving source naturality. -/
68 def precompose {T : Type*} [CommRing T] (f : RingFamily R I) (g : T →+* R) :
69     RingFamily T I where
70   maps n := (f.maps n).comp g
71   compatible := by
72     intro m n h
73     rw [← RingHom.comp_assoc, f.compatible h]
74 
75 theorem reconstruct_precompose [IsAdicComplete I S]
76     {T : Type*} [CommRing T] (f : RingFamily R I) (g : T →+* R) :
77     reconstruct I (precompose I f g) = (reconstruct I f).comp g := by
78   symm
79   apply reconstruct_unique
80   intro n
81   rw [← RingHom.comp_assoc, reconstruct_reduces]
82   rfl
83 
84 /-- Locality of the first positive precision suffices to make the lift local. -/
85 theorem reconstruct_isLocal [IsAdicComplete I S] (f : RingFamily R I)
86     (h : IsLocalHom (f.maps 1)) : IsLocalHom (reconstruct I f) := by
87   have hc : IsLocalHom ((Ideal.Quotient.mk (I ^ 1)).comp (reconstruct I f)) := by
88     rw [reconstruct_reduces]
89     exact h
90   let := hc
91   exact isLocalHom_of_comp (reconstruct I f) (Ideal.Quotient.mk (I ^ 1))
92 
93 /-- A local map of local rings preserves every power of the maximal ideal. -/
94 theorem local_map_preserves_powers [IsLocalRing R] [IsLocalRing S]
95     (F : R →+* S) [IsLocalHom F] (n : ℕ) :
96     (IsLocalRing.maximalIdeal R ^ n).map F ≤ IsLocalRing.maximalIdeal S ^ n := by
97   rw [Ideal.map_pow]
98   exact Ideal.pow_right_mono (IsLocalRing.map_maximalIdeal_le F) n
99 
100 /-- Continuity in the actual maximal-ideal adic topologies, not a renamed
101 abstract continuity assumption. -/
102 theorem local_map_continuous [IsLocalRing R] [IsLocalRing S]
103     (F : R →+* S) [IsLocalHom F] :
104     @Continuous R S (IsLocalRing.maximalIdeal R).adicTopology
105       (IsLocalRing.maximalIdeal S).adicTopology F := by
106   let : WithIdeal R := ⟨IsLocalRing.maximalIdeal R⟩
107   let : WithIdeal S := ⟨IsLocalRing.maximalIdeal S⟩
108   exact (WithIdeal.uniformContinuous_of_map_le
109     (IsLocalRing.map_maximalIdeal_le F)).continuous
110 
111 /-- The reconstructed ring map is local and continuous if its residual map is local. -/
112 theorem local_continuous_reconstruction [IsAdicComplete I S]
113     [IsLocalRing R] [IsLocalRing S] (f : RingFamily R I)
114     (h : IsLocalHom (f.maps 1)) :
115     ∃! F : R →+* S,
116       (∀ n, (Ideal.Quotient.mk (I ^ n)).comp F = f.maps n) ∧
117       IsLocalHom F ∧
118       @Continuous R S (IsLocalRing.maximalIdeal R).adicTopology
119         (IsLocalRing.maximalIdeal S).adicTopology F := by
120   let := reconstruct_isLocal I f h
121   refine ⟨reconstruct I f, ⟨reconstruct_reduces I f, inferInstance,
122     local_map_continuous _⟩, ?_⟩
123   intro F hF
124   exact reconstruct_unique I f F hF.1
125 
126 /-- Scalar compatibility also survives the limit, producing algebra maps. -/
127 theorem reconstruct_preserves_scalars [IsAdicComplete I S]
128     {B : Type*} [CommRing B] [Algebra B R] [Algebra B S]
129     (f : RingFamily R I)
130     (hf : ∀ n b, f.maps n (algebraMap B R b) =
131       Ideal.Quotient.mk (I ^ n) (algebraMap B S b)) (b : B) :
132     reconstruct I f (algebraMap B R b) = algebraMap B S b := by
133   have H : (reconstruct I f).comp (algebraMap B R) = algebraMap B S := by
134     apply DFunLike.coe_injective
135     apply IsHausdorff.funext' I
136     intro n b'
137     change Ideal.Quotient.mk (I ^ n) (reconstruct I f (algebraMap B R b')) = _
138     simp only [reconstruct, IsAdicComplete.mk_liftRingHom]
139     exact hf n b'
140   exact congrArg (fun F : B →+* S => F b) H
141 
142 /-- The inverse-limit equivalence restricted to local maps. -/
143 noncomputable def localReconstructionEquiv [IsAdicComplete I S]
144     [IsLocalRing S] (hI : I ≠ ⊤) :
145     {F : R →+* S // IsLocalHom F} ≃
146       {f : RingFamily R I // IsLocalHom (f.maps 1)} where
147   toFun F := ⟨reduce I F.val, by
148     let : Nontrivial (S ⧸ I ^ 1) :=
149       Ideal.Quotient.nontrivial_iff.mpr (by simpa using hI)
150     let : IsLocalHom (Ideal.Quotient.mk (I ^ 1)) :=
151       IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
152     let : IsLocalHom F.val := F.property
153     change IsLocalHom ((Ideal.Quotient.mk (I ^ 1)).comp F.val)
154     infer_instance⟩
155   invFun f := ⟨reconstruct I f.val, reconstruct_isLocal I f.val f.property⟩
156   left_inv F := Subtype.ext (reconstruct_reduce I F.val)
157   right_inv f := Subtype.ext (reduce_reconstruct I f.val)
158 
159 /-- Coefficient-preserving reconstruction as an actual algebra homomorphism. -/
160 noncomputable def reconstructAlg [IsAdicComplete I S]
161     {B : Type*} [CommRing B] [Algebra B R] [Algebra B S]
162     (f : RingFamily R I)
163     (hf : ∀ n b, f.maps n (algebraMap B R b) =
164       Ideal.Quotient.mk (I ^ n) (algebraMap B S b)) : R →ₐ[B] S where
165   __ := reconstruct I f
166   commutes' := reconstruct_preserves_scalars I f hf
167 
168 /-- The represented deformation-point version, retaining scalar compatibility,
169 locality, and genuine adic continuity. Representability itself is not asserted. -/
170 theorem represented_local_algebra_reconstruction [IsAdicComplete I S]
171     {B : Type*} [CommRing B] [Algebra B R] [Algebra B S]
172     [IsLocalRing R] [IsLocalRing S] (f : RingFamily R I)
173     (hf : ∀ n b, f.maps n (algebraMap B R b) =
174       Ideal.Quotient.mk (I ^ n) (algebraMap B S b))
175     (hl : IsLocalHom (f.maps 1)) :
176     ∃! F : R →ₐ[B] S,
177       (∀ n, (Ideal.Quotient.mk (I ^ n)).comp F.toRingHom = f.maps n) ∧
178       IsLocalHom F.toRingHom ∧
179       @Continuous R S (IsLocalRing.maximalIdeal R).adicTopology
180         (IsLocalRing.maximalIdeal S).adicTopology F := by
181   let F := reconstructAlg I f hf
182   let : IsLocalHom (reconstruct I f) := reconstruct_isLocal I f hl
183   refine ⟨F, ⟨reconstruct_reduces I f, reconstruct_isLocal I f hl,
184     local_map_continuous (reconstruct I f)⟩, ?_⟩
185   intro G hG
186   ext x
187   exact congrArg (fun H : R →+* S => H x) (reconstruct_unique I f G.toRingHom hG.1)
188 
189 end PaperX.Reconstruction

Back to source controls