AdicCompletionComparison.lean

1 import PaperXII.AdicQuotientTopology
2 import Mathlib.RingTheory.AdicCompletion.LocalRing
3 
4 /-!
5 # Comparison with the actual algebraic adic completion
6 
7 The inverse-limit completion is proved to be a completion of the same uniform
8 space. Density and the inducing property are proved from actual residue maps;
9 no completion package is supplied as an assumption.
10 -/
11 noncomputable section
12 open Filter Topology UniformSpace
13 open scoped Uniformity
14 set_option autoImplicit false
15 namespace PaperXII.AdicModel
16 
17 variable {R : Type*} [CommRing R] (I : Ideal R)
18 
19 abbrev AlgebraicTarget := Carrier (AdicCompletion I R)
20   (I.map (algebraMap R (AdicCompletion I R)))
21 
22 def intoAlgebraic : Carrier R I →+* AlgebraicTarget I :=
23   ((rawEquiv _ _).symm.toRingHom.comp (algebraMap R (AdicCompletion I R))).comp
24     (rawEquiv R I).toRingHom
25 
26 theorem algebraicTarget_complete (fg : I.FG) : CompleteSpace (AlgebraicTarget I) := by
27   have h : IsAdicComplete (WithIdeal.i : Ideal (AlgebraicTarget I)) (AlgebraicTarget I) :=
28     AdicCompletion.isAdicComplete_self I fg
29   exact ((carrier_isAdic _ _).isAdicComplete_iff.mp h).1
30 
31 theorem algebraicTarget_t2 (fg : I.FG) : T2Space (AlgebraicTarget I) := by
32   have h : IsAdicComplete (WithIdeal.i : Ideal (AlgebraicTarget I)) (AlgebraicTarget I) :=
33     AdicCompletion.isAdicComplete_self I fg
34   exact ((carrier_isAdic _ _).isAdicComplete_iff.mp h).2
35 
36 /-- Powers of the actual extended ideal are exactly residue-evaluation kernels. -/
37 theorem algebraic_mem_power_iff (fg : I.FG) (n : ℕ) (x : AdicCompletion I R) :
38     x ∈ (I.map (algebraMap R (AdicCompletion I R))) ^ n ↔
39       AdicCompletion.eval I R n x = 0 := by
40   rw [← Ideal.map_pow, ← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map,
41     AdicCompletion.pow_smul_top_eq_ker_eval fg, LinearMap.mem_ker]
42 
43 /-- Inverse images of every ideal power are computed, not postulated. -/
44 theorem intoAlgebraic_power_iff (fg : I.FG) (n : ℕ) (x : Carrier R I) :
45     intoAlgebraic I x ∈ (WithIdeal.i : Ideal (AlgebraicTarget I)) ^ n ↔
46       x ∈ (WithIdeal.i : Ideal (Carrier R I)) ^ n := by
47   change algebraMap R (AdicCompletion I R) (rawEquiv R I x) ∈
48     (I.map (algebraMap R (AdicCompletion I R))) ^ n ↔ rawEquiv R I x ∈ I ^ n
49   rw [algebraic_mem_power_iff I fg]
50   change AdicCompletion.eval I R n (AdicCompletion.of I R (rawEquiv R I x)) = 0 ↔ _
51   rw [AdicCompletion.eval_of]
52   simp [Ideal.Quotient.eq_zero_iff_mem, Ideal.mul_top]
53 
54 /-- The canonical map induces the exact original adic uniformity. -/
55 theorem intoAlgebraic_isUniformInducing (fg : I.FG) : IsUniformInducing (intoAlgebraic I) := by
56   rw [(carrier_isAdic R I).hasBasis_nhds_zero.uniformity_of_nhds_zero.isUniformInducing_iff
57     (carrier_isAdic _ _).hasBasis_nhds_zero.uniformity_of_nhds_zero]
58   constructor
59   · intro n _
60     refine ⟨n, trivial, ?_⟩
61     intro x y hxy
62     change intoAlgebraic I y - intoAlgebraic I x ∈ (WithIdeal.i : Ideal (AlgebraicTarget I)) ^ n
63     rw [← map_sub]
64     exact (intoAlgebraic_power_iff I fg n (y - x)).mpr hxy
65   · intro n _
66     refine ⟨n, trivial, ?_⟩
67     intro x y hxy
68     change intoAlgebraic I y - intoAlgebraic I x ∈ (WithIdeal.i : Ideal (AlgebraicTarget I)) ^ n at hxy
69     rw [← map_sub] at hxy
70     exact (intoAlgebraic_power_iff I fg n (y - x)).mp hxy
71 
72 /-- Every residue class in the completion has an actual original representative. -/
73 theorem intoAlgebraic_dense (fg : I.FG) : DenseRange (intoAlgebraic I) := by
74   rw [DenseRange, dense_iff_inter_open]
75   intro U hU hne
76   obtain ⟨x, hx⟩ := hne
77   obtain ⟨n, _, hn⟩ := (carrier_isAdic _ _).hasBasis_nhds x |>.mem_iff.mp (hU.mem_nhds hx)
78   obtain ⟨r, hr⟩ := Submodule.Quotient.mk_surjective _
79     (AdicCompletion.eval I R n (rawEquiv _ _ x))
80   let y : AlgebraicTarget I := intoAlgebraic I ((rawEquiv R I).symm r)
81   have hdiff : y - x ∈ (WithIdeal.i : Ideal (AlgebraicTarget I)) ^ n := by
82     change algebraMap R (AdicCompletion I R) r - rawEquiv _ _ x ∈
83       (I.map (algebraMap R (AdicCompletion I R))) ^ n
84     rw [algebraic_mem_power_iff I fg]
85     change AdicCompletion.eval I R n (AdicCompletion.of I R r - rawEquiv _ _ x) = 0
86     rw [map_sub, AdicCompletion.eval_of]
87     exact sub_eq_zero.mpr hr
88   refine ⟨y, ?_, ⟨(rawEquiv R I).symm r, rfl⟩⟩
89   apply hn
90   exact ⟨y - x, hdiff, add_sub_cancel _ _⟩
91 
92 /-- An abstract package constructed from the actual algebraic completion. -/
93 def algebraicPackage (fg : I.FG) : AbstractCompletion (Carrier R I) where
94   space := AlgebraicTarget I
95   coe := intoAlgebraic I
96   uniformStruct := inferInstance
97   complete := algebraicTarget_complete I fg
98   separation := by have := algebraicTarget_t2 I fg; infer_instance
99   isUniformInducing := intoAlgebraic_isUniformInducing I fg
100   dense := intoAlgebraic_dense I fg
101 
102 /-- A proved uniform equivalence between the two actual completion constructions. -/
103 def algebraicUniformEquiv (fg : I.FG) : Completed R I ≃ᵤ AlgebraicTarget I :=
104   Completion.cPkg.compareEquiv (algebraicPackage I fg)
105 
106 /-- The comparison preserves the ring operations, not only the uniformity. -/
107 def algebraicRingEquiv (fg : I.FG) : Completed R I ≃+* AlgebraicTarget I := by
108   letI := algebraicTarget_complete I fg
109   letI := algebraicTarget_t2 I fg
110   exact RingEquiv.ofBijective
111     (Completion.extensionHom (intoAlgebraic I) (intoAlgebraic_isUniformInducing I fg).uniformContinuous.continuous)
112       (algebraicUniformEquiv I fg).bijective
113 
114 theorem algebraicRingEquiv_continuous (fg : I.FG) : Continuous (algebraicRingEquiv I fg) :=
115   (algebraicUniformEquiv I fg).continuous
116 
117 theorem algebraicRingEquiv_symm_continuous (fg : I.FG) :
118     Continuous (algebraicRingEquiv I fg).symm := by
119   have he : (⇑(algebraicRingEquiv I fg).symm) = (⇑(algebraicUniformEquiv I fg).symm) := by
120     funext x
121     apply (algebraicRingEquiv I fg).injective
122     exact ((algebraicRingEquiv I fg).apply_symm_apply x).trans
123       ((algebraicUniformEquiv I fg).apply_symm_apply x).symm
124   rw [he]
125   exact (algebraicUniformEquiv I fg).symm.continuous
126 
127 @[simp] theorem algebraicRingEquiv_embed (fg : I.FG) (r : R) :
128     algebraicRingEquiv I fg (embed R I r) =
129       (rawEquiv _ _).symm (algebraMap R (AdicCompletion I R) r) := by
130   have := algebraicTarget_complete I fg
131   have := algebraicTarget_t2 I fg
132   exact Completion.extensionHom_coe (intoAlgebraic I)
133     (intoAlgebraic_isUniformInducing I fg).uniformContinuous.continuous ((rawEquiv R I).symm r)
134 
135 /-- Completion at any finitely generated maximal ideal is an actual local ring. -/
136 theorem completed_isLocalRing [I.IsMaximal] (fg : I.FG) : IsLocalRing (Completed R I) := by
137   have hm := AdicCompletion.isMaximal_map_of_le I I le_rfl fg
138   have hc := AdicCompletion.isAdicComplete_self I fg
139   have hl : IsLocalRing (AdicCompletion I R) :=
140     isLocalRing_of_isAdicComplete_maximal (I.map (algebraMap R (AdicCompletion I R)))
141   have : IsLocalRing (AlgebraicTarget I) := hl
142   exact (algebraicRingEquiv I fg).symm.isLocalRing
143 
144 /-- The comparison carries the actual extended defining ideal to the algebraic one. -/
145 theorem algebraicRingEquiv_mapIdeal (fg : I.FG) :
146     (I.map (embed R I)).map (algebraicRingEquiv I fg).toRingHom =
147       (WithIdeal.i : Ideal (AlgebraicTarget I)) := by
148   rw [Ideal.map_map]
149   have he : (algebraicRingEquiv I fg).toRingHom.comp (embed R I) =
150       (rawEquiv _ _).symm.toRingHom.comp (algebraMap R (AdicCompletion I R)) := by
151     ext r
152     exact algebraicRingEquiv_embed I fg r
153   rw [he, ← Ideal.map_map]
154   change Ideal.map (RingHom.id _) (I.map (algebraMap R (AdicCompletion I R))) = _
155   rw [Ideal.map_id]
156   rfl
157 
158 /-- Transport the actual ideal-adic topology through a bicontinuous ring equivalence. -/
159 theorem isAdic_of_equiv {S T : Type*} [CommRing S] [CommRing T]
160     [TopologicalSpace S] [TopologicalSpace T] [IsTopologicalRing S] [IsTopologicalRing T]
161     (L : Ideal S) (N : Ideal T) (e : S ≃+* T) (he : Continuous e) (hi : Continuous e.symm)
162     (hmap : L.map e.toRingHom = N) (hN : IsAdic N) : IsAdic L := by
163   have hpow (n : ℕ) : (N ^ n).comap e.toRingHom = L ^ n := by
164     rw [← hmap, ← Ideal.map_pow]
165     exact Ideal.comap_map_of_bijective e.toRingHom e.bijective
166   rw [isAdic_iff]
167   constructor
168   · intro n
169     have hEq : ((L ^ n : Ideal S) : Set S) = e ⁻¹' ((N ^ n : Ideal T) : Set T) := by
170       change ((L ^ n : Ideal S) : Set S) = ((N ^ n).comap e.toRingHom : Set S)
171       rw [hpow]
172     rw [hEq]
173     exact ((isAdic_iff.mp hN).1 n).preimage he
174   · intro U hU
175     have hpre : e.symm ⁻¹' U ∈ 𝓝 (0 : T) := by
176       have ht : Filter.Tendsto e.symm (𝓝 (0 : T)) (𝓝 (0 : S)) := by
177         simpa only [ContinuousAt, map_zero] using hi.continuousAt (x := (0 : T))
178       exact ht hU
179     obtain ⟨n, _, hn⟩ := hN.hasBasis_nhds_zero.mem_iff.mp hpre
180     refine ⟨n, ?_⟩
181     intro x hx
182     have hex : e x ∈ N ^ n := by
183       change x ∈ (N ^ n).comap e.toRingHom
184       rw [hpow]
185       exact hx
186     simpa only [Set.mem_preimage, RingEquiv.symm_apply_apply] using hn hex
187 
188 /-- The uniform completion has the adic topology of the actual extended ideal. -/
189 theorem completed_isAdic (fg : I.FG) : IsAdic (I.map (embed R I)) :=
190   isAdic_of_equiv _ _ (algebraicRingEquiv I fg) (algebraicRingEquiv_continuous I fg)
191     (algebraicRingEquiv_symm_continuous I fg) (algebraicRingEquiv_mapIdeal I fg)
192     (carrier_isAdic _ _)
193 
194 /-- The extended maximal ideal is the actual maximal ideal of the constructed completion. -/
195 theorem completed_maximalIdeal [I.IsMaximal] (fg : I.FG) :
196     haveI := completed_isLocalRing I fg
197     IsLocalRing.maximalIdeal (Completed R I) = I.map (embed R I) := by
198   have := completed_isLocalRing I fg
199   have ht : (WithIdeal.i : Ideal (AlgebraicTarget I)).IsMaximal :=
200     AdicCompletion.isMaximal_map_of_le I I le_rfl fg
201   have hm : (I.map (embed R I)).IsMaximal := by
202     have hh : (WithIdeal.i : Ideal (AlgebraicTarget I)).comap (algebraicRingEquiv I fg).toRingHom =
203         I.map (embed R I) := by
204       rw [← algebraicRingEquiv_mapIdeal I fg]
205       exact Ideal.comap_map_of_bijective (algebraicRingEquiv I fg).toRingHom (algebraicRingEquiv I fg).bijective
206     rw [← hh]
207     exact Ideal.comap_isMaximal_of_surjective _ (algebraicRingEquiv I fg).surjective
208   exact (IsLocalRing.eq_maximalIdeal hm).symm
209 
210 end PaperXII.AdicModel

Back to source controls