FiniteTensorLocality.lean

1 import PaperXII.CompletedFiniteTensor
2 import PaperXII.AdicCompletionComparison
3 import Mathlib.RingTheory.LocalRing.Quotient
4 import Mathlib.RingTheory.Finiteness.Ideal
5 
6 /-!
7 # Locality of the actual completed finite tensor ring
8 
9 Common residue data are explicit algebra maps into one field. The defining
10 ideal is proved maximal by constructing its residue-field equivalence. Finite
11 generation follows from the factor ideals, not from an assumed tensor theorem.
12 -/
13 noncomputable section
14 open Function
15 set_option autoImplicit false
16 namespace PaperXII.FiniteTensor
17 
18 variable {O ι k : Type*} [CommRing O] [Fintype ι] [DecidableEq ι] [Field k] [Algebra O k]
19 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
20 variable (res : ∀ i, R i →ₐ[O] k)
21 
22 abbrev residueIdeal : Ideal (Raw (O := O) R) :=
23   definingIdeal (O := O) R (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i))
24 
25 /-- All defining generators vanish under the actual tensor residue map. -/
26 theorem residueIdeal_le_kernel : residueIdeal R res ≤ RingHom.ker (liftFamily R res) := by
27   rw [residueIdeal, definingIdeal, sup_le_iff]
28   constructor
29   · rw [Ideal.map_le_iff_le_comap]
30     intro a ha
31     change liftFamily R res (algebraMap O (Raw (O := O) R) a) = 0
32     rw [AlgHom.commutes]
33     exact ha
34   · rw [conditions, iSup_le_iff]
35     intro i
36     rw [Ideal.map_le_iff_le_comap]
37     intro a ha
38     change liftFamily R res (includeFactor R i a) = 0
39     rw [liftFamily_include]
40     exact ha
41 
42 def residueForward : (Raw (O := O) R ⧸ residueIdeal R res) →ₐ[O] k :=
43   Ideal.Quotient.liftₐ _ (liftFamily R res) (residueIdeal_le_kernel R res)
44 
45 /-- Construct the reverse residue map by descending the scalar algebra map. -/
46 def residueInverse (hO : Surjective (algebraMap O k)) :
47     k →ₐ[O] (Raw (O := O) R ⧸ residueIdeal R res) :=
48   AlgHom.liftOfSurjective (Algebra.ofId O k) hO (Algebra.ofId O _) (by
49     intro a ha
50     apply Ideal.Quotient.eq_zero_iff_mem.mpr
51     exact (show (RingHom.ker (algebraMap O k)).map (algebraMap O (Raw (O := O) R)) ≤
52       residueIdeal R res from le_sup_left) (Ideal.mem_map_of_mem _ ha))
53 
54 omit [Fintype ι] in
55 theorem residueInverse_factor (hO : Surjective (algebraMap O k)) (i : ι) (r : R i) :
56     residueInverse R res hO (res i r) =
57       Ideal.Quotient.mk (residueIdeal R res) (includeFactor R i r) := by
58   obtain ⟨a, ha⟩ := hO (res i r)
59   have hr : r - algebraMap O (R i) a ∈ RingHom.ker (res i) := by
60     change res i (r - algebraMap O (R i) a) = 0
61     rw [map_sub, AlgHom.commutes, ha, sub_self]
62   have hk : Ideal.Quotient.mk (residueIdeal R res)
63       (includeFactor R i (r - algebraMap O (R i) a)) = 0 := by
64     apply Ideal.Quotient.eq_zero_iff_mem.mpr
65     exact (show conditions (O := O) R (fun i ↦ RingHom.ker (res i)) ≤ residueIdeal R res
66       from le_sup_right) ((le_iSup (fun j ↦ (RingHom.ker (res j)).map
67       (includeFactor R j).toRingHom) i) (Ideal.mem_map_of_mem _ hr))
68   rw [map_sub, AlgHom.commutes, map_sub, sub_eq_zero] at hk
69   rw [← ha, AlgHom.commutes]
70   exact hk.symm
71 
72 theorem residueInverse_forward (hO : Surjective (algebraMap O k)) :
73     (residueInverse R res hO).comp (residueForward R res) = AlgHom.id O _ := by
74   apply Ideal.Quotient.algHom_ext
75   apply hom_ext
76   intro i
77   ext r
78   change residueInverse R res hO (liftFamily R res (includeFactor R i r)) = _
79   rw [liftFamily_include]
80   exact residueInverse_factor R res hO i r
81 
82 theorem residueForward_inverse (hO : Surjective (algebraMap O k)) :
83     (residueForward R res).comp (residueInverse R res hO) = AlgHom.id O k := by
84   ext x
85   obtain ⟨a, rfl⟩ := hO x
86   exact AlgHom.commutes _ a
87 
88 /-- The defining ideal has exactly the declared common residue field. -/
89 def residueEquiv (hO : Surjective (algebraMap O k)) :
90     (Raw (O := O) R ⧸ residueIdeal R res) ≃ₐ[O] k :=
91   AlgEquiv.ofAlgHom (residueForward R res) (residueInverse R res hO)
92     (residueForward_inverse R res hO) (residueInverse_forward R res hO)
93 
94 theorem residueIdeal_isMaximal (hO : Surjective (algebraMap O k)) :
95     (residueIdeal R res).IsMaximal := by
96   exact Ideal.Quotient.maximal_of_isField _ ((residueEquiv R res hO).toRingEquiv.isField (Field.toIsField k))
97 
98 /-- Finite generation survives this finite tensor construction. -/
99 theorem definingIdeal_fg (mO : Ideal O) (m : ∀ i, Ideal (R i))
100     (fgO : mO.FG) (fg : ∀ i, (m i).FG) : (definingIdeal (O := O) R mO m).FG := by
101   exact Submodule.FG.sup (fgO.map _) (Submodule.fg_iSup _ (fun i ↦ (fg i).map _))
102 
103 /-- The completed finite tensor product is local under the actual common-residue data. -/
104 theorem completedTensor_isLocalRing (hO : Surjective (algebraMap O k))
105     (fgO : (RingHom.ker (algebraMap O k)).FG)
106     (fg : ∀ i, (RingHom.ker (res i)).FG) :
107     IsLocalRing (CompletedTensor (O := O) R (RingHom.ker (algebraMap O k))
108       (fun i ↦ RingHom.ker (res i))) := by
109   have := residueIdeal_isMaximal R res hO
110   exact AdicModel.completed_isLocalRing _ (definingIdeal_fg R _ _ fgO fg)
111 
112 /-- The manuscript's Noetherian hypotheses discharge finite generation internally. -/
113 theorem completedTensor_isLocalRing_noetherian [IsNoetherianRing O]
114     [∀ i, IsNoetherianRing (R i)] (hO : Surjective (algebraMap O k)) :
115     IsLocalRing (CompletedTensor (O := O) R (RingHom.ker (algebraMap O k))
116       (fun i ↦ RingHom.ker (res i))) :=
117   completedTensor_isLocalRing R res hO (Ideal.fg_of_isNoetherianRing _)
118     (fun _i ↦ Ideal.fg_of_isNoetherianRing _)
119 
120 /-- Proper quotients retain locality. The zero-ring case remains covered by the ring equivalence. -/
121 theorem completed_tensor_quotient_isLocalRing [IsNoetherianRing O]
122     [∀ i, IsNoetherianRing (R i)] (hO : Surjective (algebraMap O k))
123     (J : ∀ i, Ideal (R i))
124     [Nontrivial (CompletedTensor (O := O) R (RingHom.ker (algebraMap O k))
125       (fun i ↦ RingHom.ker (res i)) ⧸ closedConditions R (RingHom.ker (algebraMap O k))
126         (fun i ↦ RingHom.ker (res i)) J)] :
127     IsLocalRing (CompletedTensor (O := O) R (RingHom.ker (algebraMap O k))
128       (fun i ↦ RingHom.ker (res i)) ⧸ closedConditions R (RingHom.ker (algebraMap O k))
129         (fun i ↦ RingHom.ker (res i)) J) := by
130   have := completedTensor_isLocalRing_noetherian R res hO
131   exact IsLocalRing.of_surjective' (Ideal.Quotient.mk _) Ideal.Quotient.mk_surjective
132 
133 /-- The completion topology is the topology of its actual extended defining ideal. -/
134 theorem completedTensor_isAdic (mO : Ideal O) (m : ∀ i, Ideal (R i))
135     (fgO : mO.FG) (fg : ∀ i, (m i).FG) :
136     IsAdic ((definingIdeal (O := O) R mO m).map (tensorEmbed R mO m).toRingHom) :=
137   AdicModel.completed_isAdic _ (definingIdeal_fg R mO m fgO fg)
138 
139 /-- Under the common-residue data this topology is precisely the maximal-ideal topology. -/
140 theorem completedTensor_isMaximalAdic (hO : Surjective (algebraMap O k))
141     (fgO : (RingHom.ker (algebraMap O k)).FG) (fg : ∀ i, (RingHom.ker (res i)).FG) :
142     haveI := completedTensor_isLocalRing R res hO fgO fg
143     IsAdic (IsLocalRing.maximalIdeal (CompletedTensor (O := O) R
144       (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i)))) := by
145   have hm := residueIdeal_isMaximal R res hO
146   rw [AdicModel.completed_maximalIdeal _ (definingIdeal_fg R _ _ fgO fg)]
147   exact AdicModel.completed_isAdic _ (definingIdeal_fg R _ _ fgO fg)
148 
149 end PaperXII.FiniteTensor

Back to source controls