CompletedGlobalBaseChange.lean

1 import PaperXII.AdicQuotientTopology
2 import PaperXII.LocalQuotients
3 import Mathlib.RingTheory.TensorProduct.Quotient
4 
5 /-!
6 # Actual completed base change along a quotient
7 
8 The carrier is the completion of `B ⊗[A] (A/J)`, with the sum of the two mapped
9 adic ideals. It is not defined to be a quotient of `B`. The actual quotient
10 comparison determines its points and the universal factorization criterion.
11 -/
12 noncomputable section
13 open Filter Topology UniformSpace
14 open scoped TensorProduct Uniformity
15 set_option autoImplicit false
16 namespace PaperXII.CompletedBaseChange
17 
18 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
19 variable (mA : Ideal A) (mB : Ideal B) (J : Ideal A)
20 
21 abbrev Raw := B ⊗[A] (A ⧸ J)
22 
23 /-- The literal sum defining the completed tensor topology. -/
24 def tensorIdeal : Ideal (Raw (B := B) J) :=
25   mB.map (algebraMap B (Raw (B := B) J)) ⊔
26     ((mA.map (Ideal.Quotient.mk J)).map
27       (Algebra.TensorProduct.includeRight (A := B) (R := A)).toRingHom)
28 
29 abbrev Completed := AdicModel.Completed (Raw (B := B) J) (tensorIdeal mA mB J)
30 
31 /-- The canonical global ring map into the actual completed base change. -/
32 def globalMap : B →+* Completed mA mB J :=
33   (AdicModel.embed _ (tensorIdeal mA mB J)).comp (algebraMap B (Raw (B := B) J))
34 
35 /-- The ordinary tensor quotient equivalence, only an intermediate step. -/
36 def rawEquiv : Raw (B := B) J ≃+* B ⧸ J.map (algebraMap A B) :=
37   (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B J).symm.toRingEquiv
38 
39 @[simp] theorem rawEquiv_left (b : B) :
40     rawEquiv (B := B) J (algebraMap B (Raw (B := B) J) b) =
41       Ideal.Quotient.mk (J.map (algebraMap A B)) b := by
42   change (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B J).symm (b ⊗ₜ[A] 1) = _
43   simpa using Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul B J b (1 : A)
44 
45 @[simp] theorem rawEquiv_right (a : A) :
46     rawEquiv (B := B) J (Algebra.TensorProduct.includeRight (A := B) (R := A)
47       (Ideal.Quotient.mk J a)) =
48       Ideal.Quotient.mk (J.map (algebraMap A B)) (algebraMap A B a) := by
49   change (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B J).symm
50     (1 ⊗ₜ[A] (Ideal.Quotient.mk J a)) = _
51   simp [Algebra.smul_def]
52 
53 /-- The sum topology is proved to correspond to the quotient topology. -/
54 theorem rawEquiv_tensorIdeal (h : mA.map (algebraMap A B) ≤ mB) :
55     (tensorIdeal mA mB J).map (rawEquiv J).toRingHom =
56       mB.map (Ideal.Quotient.mk (J.map (algebraMap A B))) := by
57   have hl : (rawEquiv (B := B) J).toRingHom.comp (algebraMap B (Raw (B := B) J)) =
58       Ideal.Quotient.mk (J.map (algebraMap A B)) := by ext b; exact rawEquiv_left J b
59   have hr : ((rawEquiv (B := B) J).toRingHom.comp
60       (Algebra.TensorProduct.includeRight (A := B) (R := A)).toRingHom).comp
61       (Ideal.Quotient.mk J) =
62       (Ideal.Quotient.mk (J.map (algebraMap A B))).comp (algebraMap A B) := by
63     ext a; exact rawEquiv_right J a
64   simp only [tensorIdeal, Ideal.map_sup, Ideal.map_map]
65   rw [hl, ← RingHom.comp_assoc, hr, ← Ideal.map_map, sup_eq_left]
66   exact Ideal.map_mono h
67 
68 /-- The completed tensor ring compared with the actual completion of the quotient. -/
69 def completedEquiv (h : mA.map (algebraMap A B) ≤ mB) :
70     Completed mA mB J ≃+*
71       AdicModel.Completed (B ⧸ J.map (algebraMap A B))
72         (mB.map (Ideal.Quotient.mk (J.map (algebraMap A B)))) :=
73   AdicModel.completedEquiv _ _ (rawEquiv J) (rawEquiv_tensorIdeal mA mB J h)
74 
75 theorem completedEquiv_continuous (h : mA.map (algebraMap A B) ≤ mB) :
76     Continuous (completedEquiv mA mB J h) :=
77   AdicModel.completedEquiv_continuous _ _ _ (rawEquiv_tensorIdeal mA mB J h)
78 
79 theorem completedEquiv_symm_continuous (h : mA.map (algebraMap A B) ≤ mB) :
80     Continuous (completedEquiv mA mB J h).symm :=
81   AdicModel.completedEquiv_symm_continuous _ _ _ (rawEquiv_tensorIdeal mA mB J h)
82 
83 @[simp] theorem completedEquiv_globalMap (h : mA.map (algebraMap A B) ≤ mB) (b : B) :
84     completedEquiv mA mB J h (globalMap mA mB J b) =
85       AdicModel.embed _ (mB.map (Ideal.Quotient.mk (J.map (algebraMap A B))))
86         (Ideal.Quotient.mk (J.map (algebraMap A B)) b) := by
87   change AdicModel.completedEquiv _ _ _ (rawEquiv_tensorIdeal mA mB J h)
88     (AdicModel.embed _ _ _) = _
89   rw [AdicModel.completedEquiv_embed]
90   exact congrArg (AdicModel.embed _ _) (rawEquiv_left J b)
91 
92 /-- The canonical map from the global ring has dense image. -/
93 theorem globalMap_dense : DenseRange (globalMap mA mB J) := by
94   have hs : Function.Surjective (algebraMap B (Raw (B := B) J)) := by
95     intro t
96     obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective (rawEquiv (B := B) J t)
97     refine ⟨b, (rawEquiv J).injective ?_⟩
98     exact (rawEquiv_left J b).trans hb
99   have hr : Set.range (globalMap mA mB J) =
100       Set.range ((↑) : AdicModel.Carrier (Raw (B := B) J) (tensorIdeal mA mB J) →
101         Completed mA mB J) := by
102     ext x
103     constructor
104     · rintro ⟨b, rfl⟩
105       exact ⟨(AdicModel.rawEquiv _ _).symm (algebraMap B (Raw (B := B) J) b), rfl⟩
106     · rintro ⟨t, rfl⟩
107       obtain ⟨b, hb⟩ := hs (AdicModel.rawEquiv _ _ t)
108       refine ⟨b, ?_⟩
109       change Completion.coeRingHom (α := AdicModel.Carrier (Raw (B := B) J) (tensorIdeal mA mB J))
110         ((AdicModel.rawEquiv _ _).symm (algebraMap B (Raw (B := B) J) b)) =
111           Completion.coeRingHom t
112       rw [hb, RingEquiv.symm_apply_apply]
113   change Dense (Set.range (globalMap mA mB J))
114   rw [hr]
115   exact Completion.denseRange_coe
116 
117 /-- The canonical completed global map kills the original extended ideal. -/
118 theorem globalMap_kills : J.map (algebraMap A B) ≤ RingHom.ker (globalMap mA mB J) := by
119   intro b hb
120   have hzero : algebraMap B (Raw (B := B) J) b = 0 := by
121     apply (rawEquiv J).injective
122     rw [rawEquiv_left, map_zero]
123     exact Ideal.Quotient.eq_zero_iff_mem.mpr hb
124   change AdicModel.embed _ _ (algebraMap B (Raw (B := B) J) b) = 0
125   rw [hzero, map_zero]
126 
127 /-- Continuity uses the literal adic tensor topology, not a discrete replacement. -/
128 theorem globalMap_continuous :
129     Continuous ((globalMap mA mB J).comp (AdicModel.rawEquiv B mB).toRingHom) := by
130   exact Completion.continuous_coeRingHom.comp (AdicModel.map_continuous mB
131     (tensorIdeal mA mB J) (algebraMap B (Raw (B := B) J)) le_sup_left)
132 
133 variable {P : Type*} [CommRing P] [UniformSpace P] [IsUniformAddGroup P]
134   [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
135 
136 /-- Point on the quotient carrier obtained from a continuous global point. -/
137 def quotientPoint (p : B →+* P) (_hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
138     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) :
139     AdicModel.Carrier (B ⧸ J.map (algebraMap A B))
140       (mB.map (Ideal.Quotient.mk (J.map (algebraMap A B)))) →+* P :=
141   (Ideal.Quotient.lift (AdicModel.carrierIdeal mB (J.map (algebraMap A B)))
142     (p.comp (AdicModel.rawEquiv B mB).toRingHom)
143     (by
144       intro b hb
145       change p (AdicModel.rawEquiv B mB b) = 0
146       exact hJ ((AdicModel.carrierIdeal_mem _ _ _).mp hb))).comp
147     (AdicModel.quotientCarrierEquiv mB (J.map (algebraMap A B))).symm.toRingHom
148 
149 omit [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] [T2Space P] in
150 theorem quotientPoint_continuous (p : B →+* P)
151     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
152     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) : Continuous (quotientPoint mB J p hp hJ) := by
153   apply Continuous.comp _ (AdicModel.quotientCarrierEquiv_symm_continuous _ _)
154   apply (QuotientRing.isOpenQuotientMap_mk _).isQuotientMap.continuous_iff.mpr
155   exact hp
156 
157 omit [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] [T2Space P] in
158 @[simp] theorem quotientPoint_mk (p : B →+* P)
159     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
160     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) (b : B) :
161     quotientPoint mB J p hp hJ ((AdicModel.rawEquiv _ _).symm
162       (Ideal.Quotient.mk (J.map (algebraMap A B)) b)) = p b := by
163   unfold quotientPoint
164   rw [RingHom.comp_apply]
165   have hb := AdicModel.quotientCarrierEquiv_mk mB (J.map (algebraMap A B)) b
166   rw [← hb]
167   simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]
168   rfl
169 
170 /-- Extend the quotient point and pull it back along the proved completed comparison. -/
171 def factor (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
172     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
173     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) : Completed mA mB J →+* P :=
174   (Completion.extensionHom (quotientPoint mB J p hp hJ)
175     (quotientPoint_continuous mB J p hp hJ)).comp (completedEquiv mA mB J h).toRingHom
176 
177 theorem factor_continuous (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
178     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
179     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) : Continuous (factor mA mB J h p hp hJ) :=
180   Completion.continuous_extension.comp (completedEquiv_continuous mA mB J h)
181 
182 @[simp] theorem factor_globalMap (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
183     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
184     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p) (b : B) :
185     factor mA mB J h p hp hJ (globalMap mA mB J b) = p b := by
186   change Completion.extensionHom (quotientPoint mB J p hp hJ)
187     (quotientPoint_continuous mB J p hp hJ)
188       (completedEquiv mA mB J h (globalMap mA mB J b)) = p b
189   rw [completedEquiv_globalMap]
190   exact (Completion.extensionHom_coe (quotientPoint mB J p hp hJ)
191     (quotientPoint_continuous mB J p hp hJ)
192       ((AdicModel.rawEquiv _ _).symm (Ideal.Quotient.mk (J.map (algebraMap A B)) b))).trans
193         (quotientPoint_mk mB J p hp hJ b)
194 
195 omit [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] in
196 /-- No two continuous extensions of the same global point can differ. -/
197 theorem factor_unique (g₁ g₂ : Completed mA mB J →+* P) (hg₁ : Continuous g₁) (hg₂ : Continuous g₂)
198     (heq : g₁.comp (globalMap mA mB J) = g₂.comp (globalMap mA mB J)) : g₁ = g₂ := by
199   apply DFunLike.coe_injective
200   exact (globalMap_dense mA mB J).equalizer hg₁ hg₂ (funext fun b ↦ DFunLike.congr_fun heq b)
201 
202 /-- The exact existence-and-uniqueness criterion for points of completed base change. -/
203 theorem exists_unique_factor_iff (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
204     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom)) :
205     (∃! g : Completed mA mB J →+* P,
206       Continuous g ∧ g.comp (globalMap mA mB J) = p) ↔
207         J.map (algebraMap A B) ≤ RingHom.ker p := by
208   constructor
209   · rintro ⟨g, ⟨_, hg⟩, _⟩ b hb
210     change p b = 0
211     rw [← hg]
212     change g (globalMap mA mB J b) = 0
213     rw [show globalMap mA mB J b = 0 from globalMap_kills mA mB J hb, map_zero]
214   · intro hJ
215     refine ⟨factor mA mB J h p hp hJ, ⟨factor_continuous mA mB J h p hp hJ, ?_⟩, ?_⟩
216     · ext b; exact factor_globalMap mA mB J h p hp hJ b
217     · intro g hg
218       apply factor_unique mA mB J g _ hg.1 (factor_continuous mA mB J h p hp hJ)
219       ext b
220       exact (DFunLike.congr_fun hg.2 b).trans (factor_globalMap mA mB J h p hp hJ b).symm
221 
222 /-- The same criterion expressed at the original local algebra. -/
223 theorem exists_unique_factor_iff_restriction (h : mA.map (algebraMap A B) ≤ mB)
224     (p : B →+* P) (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom)) :
225     (∃! g : Completed mA mB J →+* P,
226       Continuous g ∧ g.comp (globalMap mA mB J) = p) ↔
227         J ≤ RingHom.ker (p.comp (algebraMap A B)) := by
228   rw [exists_unique_factor_iff mA mB J h p hp, Ideal.map_le_iff_le_comap]
229   rfl
230 
231 /-- Claim 3.3: all local conditions, for the actual completed global tensor. -/
232 theorem global_base_change {V : Type*} (S : V → Type*) [∀ v, CommRing (S v)]
233     [TopologicalSpace A] [IsTopologicalRing A] (hA : IsAdic mA)
234     (inc : ∀ v, S v →+* A) (I : ∀ v, Ideal (S v))
235     (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
236     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom)) :
237     (∃! g : Completed mA mB (LocalQuotients.closedConditions S inc I) →+* P,
238       Continuous g ∧ g.comp (globalMap mA mB (LocalQuotients.closedConditions S inc I)) = p) ↔
239         ∀ v, I v ≤ RingHom.ker ((p.comp (algebraMap A B)).comp (inc v)) := by
240   rw [exists_unique_factor_iff_restriction mA mB _ h p hp]
241   apply LocalQuotients.closed_conditions_iff S inc I
242   have hc : Continuous (((AdicModel.rawEquiv B mB).symm.toRingHom).comp (algebraMap A B)) := by
243     apply AdicModel.continuous_of_map_le hA (AdicModel.carrier_isAdic B mB)
244     exact h
245   exact hp.comp hc
246 
247 /-- Natural behavior of the unique completed extension under continuous target maps. -/
248 theorem factor_natural {Q : Type*} [CommRing Q] [UniformSpace Q] [IsUniformAddGroup Q]
249     [IsTopologicalRing Q] [CompleteSpace Q] [T2Space Q]
250     (h : mA.map (algebraMap A B) ≤ mB) (p : B →+* P)
251     (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom))
252     (hJ : J.map (algebraMap A B) ≤ RingHom.ker p)
253     (u : P →+* Q) (hu : Continuous u) :
254     u.comp (factor mA mB J h p hp hJ) =
255       factor mA mB J h (u.comp p) (hu.comp hp)
256         (fun b hb ↦ by change u (p b) = 0; rw [hJ hb, map_zero]) := by
257   apply factor_unique mA mB J _ _ (hu.comp (factor_continuous mA mB J h p hp hJ))
258     (factor_continuous mA mB J h (u.comp p) (hu.comp hp) _)
259   ext b
260   change u (factor mA mB J h p hp hJ (globalMap mA mB J b)) = _
261   simp only [factor_globalMap, RingHom.comp_apply]
262 
263 end PaperXII.CompletedBaseChange

Back to source controls