LocalQuotients.lean

1 import Mathlib.Topology.Algebra.Ring.Ideal
2 import Mathlib.RingTheory.LocalRing.RingHom.Basic
3 import Mathlib.RingTheory.Ideal.Maps
4 
5 /-! Actual quotient factorization, including continuity and the closed ideal
6 generated by local conditions. This proves the factorization assertion of
7 Paper XII 3.2 for the supplied topological rings and inclusions. -/
8 set_option autoImplicit false
9 namespace PaperXII.LocalQuotients
10 
11 variable {R A : Type*} [CommRing R] [CommRing A]
12 
13 /-- Factorization of the original point through the actual ideal quotient. -/
14 def Factors (J : Ideal R) (f : R →+* A) : Prop :=
15   ∃ g : R ⧸ J →+* A, g.comp (Ideal.Quotient.mk J) = f
16 
17 /-- Algebraic factorization is exactly kernel containment. -/
18 theorem factors_iff (J : Ideal R) (f : R →+* A) :
19     Factors J f ↔ J ≤ RingHom.ker f := by
20   constructor
21   · rintro ⟨g, hg⟩ a ha
22     change f a = 0
23     rw [← hg]
24     change g (Ideal.Quotient.mk J a) = 0
25     rw [Ideal.Quotient.eq_zero_iff_mem.mpr ha, map_zero]
26   · intro h
27     exact ⟨Ideal.Quotient.lift J f h, by ext a; rfl⟩
28 
29 /-- The quotient map is surjective, so its factor is unique. -/
30 theorem factor_unique (J : Ideal R) (f : R →+* A) (g h : R ⧸ J →+* A)
31     (hg : g.comp (Ideal.Quotient.mk J) = f)
32     (hh : h.comp (Ideal.Quotient.mk J) = f) : g = h :=
33   Ideal.Quotient.ringHom_ext (hg.trans hh.symm)
34 
35 /-- A factor of a local point is itself a local map. -/
36 theorem factor_isLocal (J : Ideal R) (f : R →+* A) [IsLocalHom f]
37     (g : R ⧸ J →+* A) (hg : g.comp (Ideal.Quotient.mk J) = f) : IsLocalHom g := by
38   constructor
39   intro x hx
40   obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
41   have ha : IsUnit (f a) := by
42     rw [← hg]
43     exact hx
44   exact (isUnit_of_map_unit f a ha).map (Ideal.Quotient.mk J)
45 
46 variable [TopologicalSpace R] [IsTopologicalRing R] [TopologicalSpace A]
47 
48 /-- Continuous factorization uses the actual quotient topology. -/
49 def ContinuousFactors (J : Ideal R) (f : R →+* A) : Prop :=
50   ∃ g : R ⧸ J →+* A, Continuous g ∧ g.comp (Ideal.Quotient.mk J) = f
51 
52 /-- The actual quotient factor of a continuous point is continuous. -/
53 theorem continuous_lift (J : Ideal R) (f : R →+* A) (hf : Continuous f)
54     (hJ : J ≤ RingHom.ker f) : Continuous (Ideal.Quotient.lift J f hJ) := by
55   apply (QuotientRing.isOpenQuotientMap_mk J).isQuotientMap.continuous_iff.mpr
56   exact hf
57 
58 /-- There is no additional continuity obstruction after kernel containment. -/
59 theorem continuous_factors_iff (J : Ideal R) (f : R →+* A) (hf : Continuous f) :
60     ContinuousFactors J f ↔ J ≤ RingHom.ker f := by
61   constructor
62   · rintro ⟨g, _, hg⟩
63     exact (factors_iff J f).mp ⟨g, hg⟩
64   · intro hJ
65     exact ⟨Ideal.Quotient.lift J f hJ, continuous_lift J f hf hJ, by ext a; rfl⟩
66 
67 /-- Existence and uniqueness hold for the continuous quotient factor of the same point. -/
68 theorem exists_unique_continuous_factor (J : Ideal R) (f : R →+* A)
69     (hf : Continuous f) (hJ : J ≤ RingHom.ker f) :
70     ∃! g : R ⧸ J →+* A, Continuous g ∧ g.comp (Ideal.Quotient.mk J) = f := by
71   obtain ⟨g, hc, hg⟩ := (continuous_factors_iff J f hf).mpr hJ
72   exact ⟨g, ⟨hc, hg⟩, fun h hh ↦ factor_unique J f h g hh.2 hg⟩
73 
74 variable [T2Space A]
75 
76 omit [IsTopologicalRing R] in
77 /-- The Hausdorff target makes the kernel of a continuous point closed. -/
78 theorem kernel_closed (f : R →+* A) (hf : Continuous f) :
79     IsClosed (RingHom.ker f : Set R) := isClosed_eq hf continuous_const
80 
81 /-- Killing an ideal and killing its topological closure are equivalent. -/
82 theorem closure_le_kernel_iff (J : Ideal R) (f : R →+* A) (hf : Continuous f) :
83     J.closure ≤ RingHom.ker f ↔ J ≤ RingHom.ker f := by
84   constructor
85   · intro h a ha
86     exact h (subset_closure ha)
87   · intro h
88     exact closure_minimal h (kernel_closed f hf)
89 
90 variable {V : Type*} (S : V → Type*) [∀ v, CommRing (S v)]
91     (inc : ∀ v, S v →+* R) (J : ∀ v, Ideal (S v))
92 
93 /-- The literal closed ideal generated by all local condition ideals. -/
94 def closedConditions : Ideal R := (⨆ v, (J v).map (inc v)).closure
95 
96 /-- The closure step and restriction to every local ideal are both proved. -/
97 theorem closed_conditions_iff (f : R →+* A) (hf : Continuous f) :
98     closedConditions S inc J ≤ RingHom.ker f ↔
99       ∀ v, J v ≤ RingHom.ker (f.comp (inc v)) := by
100   rw [closedConditions, closure_le_kernel_iff _ f hf, iSup_le_iff]
101   apply forall_congr'
102   intro v
103   rw [Ideal.map_le_iff_le_comap]
104   rfl
105 
106 /-- Corollary 3.2: the global point factors exactly when all local restrictions do. -/
107 theorem factors_iff_local_factors [∀ v, TopologicalSpace (S v)]
108     [∀ v, IsTopologicalRing (S v)] (hinc : ∀ v, Continuous (inc v))
109     (f : R →+* A) (hf : Continuous f) :
110     ContinuousFactors (closedConditions S inc J) f ↔
111       ∀ v, ContinuousFactors (J v) (f.comp (inc v)) := by
112   rw [continuous_factors_iff _ f hf, closed_conditions_iff S inc J f hf]
113   exact forall_congr' (fun v ↦ (continuous_factors_iff (J v)
114     (f.comp (inc v)) (hf.comp (hinc v))).symm)
115 
116 /-- When the point is local, its unique continuous global quotient factor is local. -/
117 theorem exists_unique_local_factor (f : R →+* A) [IsLocalHom f]
118     (hf : Continuous f) (h : ∀ v, J v ≤ RingHom.ker (f.comp (inc v))) :
119     ∃! g : R ⧸ closedConditions S inc J →+* A,
120       Continuous g ∧ IsLocalHom g ∧ g.comp (Ideal.Quotient.mk _) = f := by
121   obtain ⟨g, hg, _⟩ := exists_unique_continuous_factor (closedConditions S inc J) f hf
122     ((closed_conditions_iff S inc J f hf).mpr h)
123   exact ⟨g, ⟨hg.1, factor_isLocal _ f g hg.2, hg.2⟩,
124     fun k hk ↦ factor_unique _ f k g hk.2.2 hg.2⟩
125 
126 end PaperXII.LocalQuotients

Back to source controls