CompletionQuotient.lean

1 import Mathlib.Topology.Algebra.UniformRing
2 import Mathlib.Topology.Algebra.Ring.Ideal
3 import Mathlib.Topology.Algebra.IsUniformGroup.Basic
4 import Mathlib.RingTheory.Ideal.Maps
5 
6 /-!
7 # Completion and closed ideal quotients
8 
9 The completion is Mathlib's actual Hausdorff uniform completion. The quotient has
10 its quotient topology and the associated additive-group uniformity. The
11 countable-uniformity hypothesis is used only to prove completeness of its quotient.
12 No completeness, surjectivity, or inverse for the comparison is postulated.
13 -/
14 
15 noncomputable section
16 open Filter Topology UniformSpace
17 open scoped Uniformity
18 set_option autoImplicit false
19 namespace PaperXII.CompletionQuotient
20 
21 variable {R : Type*} [CommRing R] [UniformSpace R] [IsUniformAddGroup R]
22   [IsTopologicalRing R]
23 
24 /-- Countable uniform bases survive actual Hausdorff completion. -/
25 theorem completion_countablyGenerated {α : Type*} [UniformSpace α]
26     [Filter.IsCountablyGenerated (𝓤 α)] :
27     Filter.IsCountablyGenerated (𝓤 (Completion α)) := by
28   have : Filter.IsCountablyGenerated (𝓤 (CauchyFilter α)) := by
29     obtain ⟨s, hs⟩ := Filter.isCountablyGenerated_iff_exists_antitone_basis.mp
30       (inferInstance : Filter.IsCountablyGenerated (𝓤 α))
31     exact (CauchyFilter.basis_uniformity hs.toHasBasis).isCountablyGenerated
32   change Filter.IsCountablyGenerated (𝓤 (SeparationQuotient (CauchyFilter α)))
33   rw [SeparationQuotient.uniformity_eq]
34   infer_instance
35 
36 /-- The uniformity associated with the actual quotient topology. -/
37 @[instance_reducible] def quotientUniformSpace {S : Type*} [CommRing S] [TopologicalSpace S]
38     [IsTopologicalRing S] (I : Ideal S) : UniformSpace (S ⧸ I) :=
39   IsTopologicalAddGroup.rightUniformSpace (S ⧸ I)
40 
41 attribute [local instance] quotientUniformSpace
42 
43 instance quotientUniformAddGroup {S : Type*} [CommRing S] [TopologicalSpace S]
44     [IsTopologicalRing S] (I : Ideal S) : IsUniformAddGroup (S ⧸ I) :=
45   isUniformAddGroup_of_addCommGroup
46 
47 /-- Close the extended ideal in the actual completion. -/
48 def closedExtension (I : Ideal R) : Ideal (Completion R) :=
49   (I.map (Completion.coeRingHom : R →+* Completion R)).closure
50 
51 instance closedExtension_isClosed (I : Ideal R) :
52     IsClosed (closedExtension I : Set (Completion R)) := isClosed_closure
53 
54 /-- The quotient of the completion is complete; no finite-generation assumption. -/
55 theorem quotient_complete (I : Ideal R) [Filter.IsCountablyGenerated (𝓤 R)] :
56     CompleteSpace (Completion R ⧸ closedExtension I) := by
57   have := completion_countablyGenerated (α := R)
58   exact QuotientAddGroup.completeSpace_right (Completion R) (closedExtension I).toAddSubgroup
59 
60 /-- The completion of the quotient receives the canonical completed quotient map. -/
61 def forwardMap (I : Ideal R) : Completion R →+* Completion (R ⧸ I) :=
62   Completion.mapRingHom (Ideal.Quotient.mk I)
63     (QuotientRing.isOpenQuotientMap_mk I).continuous
64 
65 theorem forwardMap_continuous (I : Ideal R) : Continuous (forwardMap I) :=
66   Completion.continuous_extension
67 
68 @[simp] theorem forwardMap_coe (I : Ideal R) (r : R) :
69     forwardMap I (r : Completion R) = (Ideal.Quotient.mk I r : Completion (R ⧸ I)) :=
70   Completion.mapRingHom_coe _ r
71 
72 /-- The canonical completed map kills the closed extended ideal, by continuity. -/
73 theorem closedExtension_le_ker (I : Ideal R) :
74     closedExtension I ≤ RingHom.ker (forwardMap I) := by
75   apply closure_minimal
76   · change I.map (Completion.coeRingHom : R →+* Completion R) ≤ RingHom.ker (forwardMap I)
77     rw [Ideal.map_le_iff_le_comap]
78     intro r hr
79     change forwardMap I (r : Completion R) = 0
80     rw [forwardMap_coe, Ideal.Quotient.eq_zero_iff_mem.mpr hr]
81     exact map_zero Completion.coeRingHom
82   · exact isClosed_eq (forwardMap_continuous I) continuous_const
83 
84 /-- One direction of the comparison, factored through the actual ideal quotient. -/
85 def forward (I : Ideal R) :
86     (Completion R ⧸ closedExtension I) →+* Completion (R ⧸ I) :=
87   Ideal.Quotient.lift _ (forwardMap I) (closedExtension_le_ker I)
88 
89 theorem forward_continuous (I : Ideal R) : Continuous (forward I) := by
90   apply (QuotientRing.isOpenQuotientMap_mk (closedExtension I)).isQuotientMap.continuous_iff.mpr
91   exact forwardMap_continuous I
92 
93 @[simp] theorem forward_mk (I : Ideal R) (x : Completion R) :
94     forward I (Ideal.Quotient.mk (closedExtension I) x) = forwardMap I x := rfl
95 
96 /-- The dense, uncompleted quotient maps to the quotient of the completion. -/
97 def baseMap (I : Ideal R) : R →+* (Completion R ⧸ closedExtension I) :=
98   (Ideal.Quotient.mk (closedExtension I)).comp Completion.coeRingHom
99 
100 theorem baseMap_continuous (I : Ideal R) : Continuous (baseMap I) :=
101   (QuotientRing.isOpenQuotientMap_mk _).continuous.comp Completion.continuous_coeRingHom
102 
103 theorem ideal_le_ker_baseMap (I : Ideal R) : I ≤ RingHom.ker (baseMap I) := by
104   intro r hr
105   apply Ideal.Quotient.eq_zero_iff_mem.mpr
106   exact subset_closure (Ideal.mem_map_of_mem _ hr)
107 
108 def quotientBaseMap (I : Ideal R) : (R ⧸ I) →+* (Completion R ⧸ closedExtension I) :=
109   Ideal.Quotient.lift I (baseMap I) (ideal_le_ker_baseMap I)
110 
111 theorem quotientBaseMap_continuous (I : Ideal R) : Continuous (quotientBaseMap I) := by
112   apply (QuotientRing.isOpenQuotientMap_mk I).isQuotientMap.continuous_iff.mpr
113   exact baseMap_continuous I
114 
115 @[simp] theorem quotientBaseMap_mk (I : Ideal R) (r : R) :
116     quotientBaseMap I (Ideal.Quotient.mk I r) =
117       Ideal.Quotient.mk (closedExtension I) (r : Completion R) := rfl
118 
119 section Countable
120 variable [Filter.IsCountablyGenerated (𝓤 R)]
121 attribute [local instance] quotient_complete
122 
123 /-- The reverse comparison extends the quotient map to its actual completion. -/
124 def backward (I : Ideal R) :
125     Completion (R ⧸ I) →+* (Completion R ⧸ closedExtension I) :=
126   Completion.extensionHom (quotientBaseMap I) (quotientBaseMap_continuous I)
127 
128 theorem backward_continuous (I : Ideal R) : Continuous (backward I) :=
129   Completion.continuous_extension
130 
131 @[simp] theorem backward_coe (I : Ideal R) (x : R ⧸ I) :
132     backward I (x : Completion (R ⧸ I)) = quotientBaseMap I x :=
133   Completion.extensionHom_coe _ _ x
134 
135 /-- First inverse law, established on dense representatives then by continuity. -/
136 theorem forward_backward (I : Ideal R) (x : Completion (R ⧸ I)) :
137     forward I (backward I x) = x := by
138   refine Completion.induction_on x
139     (isClosed_eq ((forward_continuous I).comp (backward_continuous I)) continuous_id) ?_
140   intro x
141   obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
142   simp
143 
144 /-- Second inverse law; the dense representative argument precedes quotient induction. -/
145 theorem backward_forwardMap (I : Ideal R) (x : Completion R) :
146     backward I (forwardMap I x) = Ideal.Quotient.mk (closedExtension I) x := by
147   refine Completion.induction_on x
148     (isClosed_eq ((backward_continuous I).comp (forwardMap_continuous I))
149       (QuotientRing.isOpenQuotientMap_mk _).continuous) ?_
150   intro r
151   simp
152 
153 theorem backward_forward (I : Ideal R) (x : Completion R ⧸ closedExtension I) :
154     backward I (forward I x) = x := by
155   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
156   exact backward_forwardMap I x
157 
158 /-- Completion commutes with quotient by the closed extended ideal. -/
159 def equiv (I : Ideal R) :
160     (Completion R ⧸ closedExtension I) ≃+* Completion (R ⧸ I) :=
161   RingEquiv.ofRingHom (forward I) (backward I)
162     (RingHom.ext (forward_backward I)) (RingHom.ext (backward_forward I))
163 
164 theorem equiv_continuous (I : Ideal R) : Continuous (equiv I) := forward_continuous I
165 
166 theorem equiv_symm_continuous (I : Ideal R) : Continuous (equiv I).symm :=
167   backward_continuous I
168 
169 @[simp] theorem equiv_mk_coe (I : Ideal R) (r : R) :
170     equiv I (Ideal.Quotient.mk (closedExtension I) (r : Completion R)) =
171       (Ideal.Quotient.mk I r : Completion (R ⧸ I)) := forwardMap_coe I r
172 
173 /-- A bundled homeomorphism accompanying the ring equivalence. -/
174 def homeomorph (I : Ideal R) :
175     (Completion R ⧸ closedExtension I) ≃ₜ Completion (R ⧸ I) where
176   toEquiv := (equiv I).toEquiv
177   continuous_toFun := equiv_continuous I
178   continuous_invFun := equiv_symm_continuous I
179 
180 end Countable
181 end PaperXII.CompletionQuotient

Back to source controls