CompletedGlobalQuotient.lean

1 import PaperXII.CompletedBaseChangeTransport
2 import Mathlib.RingTheory.LocalRing.RingHom.Basic
3 
4 /-! For an actually complete global ring the completed base change is its
5 closed ideal quotient. This additionally proves surjectivity and preservation
6 of locality for the point factorizations. -/
7 noncomputable section
8 open Filter Topology UniformSpace
9 open scoped Uniformity
10 set_option autoImplicit false
11 namespace PaperXII.CompletedBaseChange
12 
13 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
14 variable [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B]
15   [CompleteSpace B]
16 variable (mA : Ideal A) (mB : Ideal B) (J : Ideal A) (hB : IsAdic mB)
17   (h : mA.map (algebraMap A B) ≤ mB)
18 
19 abbrev globalClosedIdeal := (J.map (algebraMap A B)).closure
20 
21 instance globalClosedIdeal_closed : IsClosed (globalClosedIdeal (B := B) J : Set B) := isClosed_closure
22 attribute [local instance] CompletionQuotient.quotientUniformSpace
23 
24 include hB in
25 theorem globalQuotient_complete : CompleteSpace (B ⧸ globalClosedIdeal (B := B) J) := by
26   have : Filter.IsCountablyGenerated (𝓤 B) :=
27     hB.hasBasis_nhds_zero.uniformity_of_nhds_zero.isCountablyGenerated
28   exact QuotientAddGroup.completeSpace_right B (globalClosedIdeal (B := B) J).toAddSubgroup
29 
30 omit [CompleteSpace B] [IsUniformAddGroup B] in
31 include hB in
32 theorem globalMap_continuous_actual : Continuous (globalMap mA mB J) := by
33   have ht : Continuous ((AdicModel.rawEquiv B mB).symm : B → AdicModel.Carrier B mB) := by
34     apply AdicModel.continuous_of_map_le hB (AdicModel.carrier_isAdic B mB)
35       (AdicModel.rawEquiv B mB).symm.toRingHom
36     change mB.map (RingHom.id B) ≤ mB
37     simp
38   exact (globalMap_continuous mA mB J).comp ht
39 
40 omit [CompleteSpace B] [IsUniformAddGroup B] in
41 include hB in
42 theorem globalClosedIdeal_le_ker : globalClosedIdeal (B := B) J ≤ RingHom.ker (globalMap mA mB J) := by
43   exact (LocalQuotients.closure_le_kernel_iff _ _ (globalMap_continuous_actual mA mB J hB)).mpr
44     (globalMap_kills mA mB J)
45 
46 /-- Map from the actual closed global quotient into the completed tensor. -/
47 def fromGlobalQuotient : (B ⧸ globalClosedIdeal (B := B) J) →+* Completed mA mB J :=
48   Ideal.Quotient.lift _ (globalMap mA mB J) (globalClosedIdeal_le_ker mA mB J hB)
49 
50 omit [CompleteSpace B] [IsUniformAddGroup B] in
51 theorem fromGlobalQuotient_continuous : Continuous (fromGlobalQuotient mA mB J hB) :=
52   LocalQuotients.continuous_lift _ _ (globalMap_continuous_actual mA mB J hB) _
53 
54 omit [CompleteSpace B] [IsUniformAddGroup B] in
55 @[simp] theorem fromGlobalQuotient_mk (b : B) :
56     fromGlobalQuotient mA mB J hB (Ideal.Quotient.mk _ b) = globalMap mA mB J b := rfl
57 
58 omit [CompleteSpace B] [IsUniformAddGroup B] in
59 include hB in
60 theorem globalQuotient_point_continuous :
61     Continuous ((Ideal.Quotient.mk (globalClosedIdeal (B := B) J)).comp
62       (AdicModel.rawEquiv B mB).toRingHom) := by
63   have hr : Continuous ((AdicModel.rawEquiv B mB).toRingHom :
64       AdicModel.Carrier B mB →+* B) := by
65     apply AdicModel.continuous_of_map_le (AdicModel.carrier_isAdic B mB) hB
66       (AdicModel.rawEquiv B mB).toRingHom
67     change mB.map (RingHom.id B) ≤ mB
68     simp
69   have hq : Continuous (Ideal.Quotient.mk (globalClosedIdeal (B := B) J) :
70       B → B ⧸ globalClosedIdeal (B := B) J) :=
71     (QuotientRing.isOpenQuotientMap_mk (globalClosedIdeal (B := B) J)).continuous
72   exact hq.comp hr
73 
74 omit [CompleteSpace B] [IsUniformAddGroup B] in
75 theorem globalQuotient_point_kills : J.map (algebraMap A B) ≤
76     RingHom.ker (Ideal.Quotient.mk (globalClosedIdeal (B := B) J)) :=
77   fun _ hb ↦ Ideal.Quotient.eq_zero_iff_mem.mpr (subset_closure hb)
78 
79 /-- Construct the reverse map using actual completeness of the closed quotient. -/
80 def toGlobalQuotient : Completed mA mB J →+* (B ⧸ globalClosedIdeal (B := B) J) := by
81   letI := globalQuotient_complete mB J hB
82   exact factor mA mB J h (Ideal.Quotient.mk (globalClosedIdeal (B := B) J))
83     (globalQuotient_point_continuous mB J hB) (globalQuotient_point_kills J)
84 
85 theorem toGlobalQuotient_continuous : Continuous (toGlobalQuotient mA mB J hB h) := by
86   have := globalQuotient_complete mB J hB
87   exact factor_continuous mA mB J h (Ideal.Quotient.mk (globalClosedIdeal (B := B) J))
88     (globalQuotient_point_continuous mB J hB) (globalQuotient_point_kills J)
89 
90 @[simp] theorem toGlobalQuotient_globalMap (b : B) :
91     toGlobalQuotient mA mB J hB h (globalMap mA mB J b) = Ideal.Quotient.mk _ b := by
92   have := globalQuotient_complete mB J hB
93   exact factor_globalMap mA mB J h (Ideal.Quotient.mk (globalClosedIdeal (B := B) J))
94     (globalQuotient_point_continuous mB J hB) (globalQuotient_point_kills J) b
95 
96 theorem toGlobalQuotient_from (x : B ⧸ globalClosedIdeal (B := B) J) :
97     toGlobalQuotient mA mB J hB h (fromGlobalQuotient mA mB J hB x) = x := by
98   obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective x
99   rw [fromGlobalQuotient_mk, toGlobalQuotient_globalMap]
100 
101 theorem fromGlobalQuotient_to (x : Completed mA mB J) :
102     fromGlobalQuotient mA mB J hB (toGlobalQuotient mA mB J hB h x) = x := by
103   have he : (fromGlobalQuotient mA mB J hB).comp (toGlobalQuotient mA mB J hB h) =
104       RingHom.id _ := by
105     apply factor_unique mA mB J _ _
106       ((fromGlobalQuotient_continuous mA mB J hB).comp (toGlobalQuotient_continuous mA mB J hB h))
107       continuous_id
108     ext b
109     change fromGlobalQuotient mA mB J hB
110       (toGlobalQuotient mA mB J hB h (globalMap mA mB J b)) = globalMap mA mB J b
111     rw [toGlobalQuotient_globalMap, fromGlobalQuotient_mk]
112   exact DFunLike.congr_fun he x
113 
114 /-- Actual topological global quotient description; no completed object is postulated. -/
115 def globalQuotientEquiv : Completed mA mB J ≃+* (B ⧸ globalClosedIdeal (B := B) J) :=
116   RingEquiv.ofRingHom (toGlobalQuotient mA mB J hB h) (fromGlobalQuotient mA mB J hB)
117     (RingHom.ext (toGlobalQuotient_from mA mB J hB h))
118     (RingHom.ext (fromGlobalQuotient_to mA mB J hB h))
119 
120 theorem globalQuotientEquiv_continuous :
121     Continuous (globalQuotientEquiv mA mB J hB h) ∧
122       Continuous (globalQuotientEquiv mA mB J hB h).symm :=
123   ⟨toGlobalQuotient_continuous mA mB J hB h, fromGlobalQuotient_continuous mA mB J hB⟩
124 
125 include hB h in
126 /-- Actual completeness of the global ring makes its canonical base-change map surjective. -/
127 theorem globalMap_surjective : Function.Surjective (globalMap mA mB J) := by
128   intro x
129   obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective (globalQuotientEquiv mA mB J hB h x)
130   refine ⟨b, (globalQuotientEquiv mA mB J hB h).injective ?_⟩
131   exact (toGlobalQuotient_globalMap mA mB J hB h b).trans hb
132 
133 include hB h in
134 /-- Nonzero actual global base changes retain locality. -/
135 theorem completed_global_isLocalRing [IsLocalRing B] [Nontrivial (Completed mA mB J)] :
136     IsLocalRing (Completed mA mB J) :=
137   IsLocalRing.of_surjective' (globalMap mA mB J) (globalMap_surjective mA mB J hB h)
138 
139 include hB h in
140 /-- A local global point has a local factor through its actual completed base change. -/
141 theorem completed_factor_isLocal {P : Type*} [CommRing P] (p : B →+* P) [IsLocalHom p]
142     (g : Completed mA mB J →+* P) (hg : g.comp (globalMap mA mB J) = p) : IsLocalHom g := by
143   constructor
144   intro x hx
145   obtain ⟨b, rfl⟩ := globalMap_surjective mA mB J hB h x
146   have hp : IsUnit (p b) := by
147     rw [← hg]
148     exact hx
149   exact (isUnit_of_map_unit p b hp).map (globalMap mA mB J)
150 
151 variable {C : Type*} [CommRing C] [Algebra A C] (e : (A ⧸ J) ≃ₐ[A] C)
152 
153 include hB h in
154 /-- The separately constructed condition ring gives the same surjective global map. -/
155 theorem transportedGlobalMap_surjective :
156     Function.Surjective (transportedGlobalMap mA mB J e) := by
157   intro x
158   obtain ⟨y, rfl⟩ := (completedTransport mA mB J e).surjective x
159   obtain ⟨b, rfl⟩ := globalMap_surjective mA mB J hB h y
160   exact ⟨b, (completedTransport_globalMap mA mB J e b).symm⟩
161 
162 include hB h in
163 /-- Every factor of a local point through the actual transported base change is local. -/
164 theorem transported_factor_isLocal {P : Type*} [CommRing P] (p : B →+* P) [IsLocalHom p]
165     (g : Transported mA mB J e →+* P)
166     (hg : g.comp (transportedGlobalMap mA mB J e) = p) : IsLocalHom g := by
167   constructor
168   intro x hx
169   obtain ⟨b, rfl⟩ := transportedGlobalMap_surjective mA mB J hB h e x
170   have hp : IsUnit (p b) := by rw [← hg]; exact hx
171   exact (isUnit_of_map_unit p b hp).map (transportedGlobalMap mA mB J e)
172 
173 end PaperXII.CompletedBaseChange

Back to source controls