IntegralCharts.lean

1 import PaperX.SmoothMaps
2 
3 /-! Integral local maps are reconstructed from the finite parameter evaluations.
4 Completeness is required explicitly; it is not inferred from finite counts. -/
5 set_option autoImplicit false
6 namespace PaperX.IntegralCharts
7 open PaperX.FormalCharts PaperX.SmoothMaps
8 
9 variable {R : Type*} [CommRing R] [IsLocalRing R]
10 
11 /-- Reducing a maximal-ideal element at any precision produces a nilpotent. -/
12 theorem parameter_reduction_nilpotent (x : IsLocalRing.maximalIdeal R) (n : ℕ) :
13     IsNilpotent (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R ^ n) x.val) := by
14   refine ⟨n, ?_⟩
15   rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
16   exact Ideal.pow_mem_pow x.property n
17 
18 /-- Evaluate a fixed integral tuple at each finite precision, including the
19 trivial precision-zero quotient to match the completion API. -/
20 noncomputable def finiteEvaluation {d : ℕ} (a : Fin d → IsLocalRing.maximalIdeal R) (n : ℕ) :
21     MvPowerSeries (Fin d) R →ₐ[R] (R ⧸ IsLocalRing.maximalIdeal R ^ n) :=
22   nilAeval (fun i => Ideal.Quotient.mk _ (a i).val)
23     (fun i => parameter_reduction_nilpotent (a i) n)
24 
25 @[simp] theorem finiteEvaluation_X {d : ℕ}
26     (a : Fin d → IsLocalRing.maximalIdeal R) (n : ℕ) (i : Fin d) :
27     finiteEvaluation a n (MvPowerSeries.X i) = Ideal.Quotient.mk _ (a i).val := by
28   exact nilAeval_X _ _ _
29 
30 /-- The evaluations commute with every quotient reduction. -/
31 theorem finiteEvaluation_compatible {d : ℕ}
32     (a : Fin d → IsLocalRing.maximalIdeal R) {m n : ℕ} (h : m ≤ n) :
33     (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal R) h).comp
34       (finiteEvaluation a n).toRingHom = (finiteEvaluation a m).toRingHom := by
35   apply nilpotent_hom_ext d
36   · intro r
37     change Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal R) h
38       (finiteEvaluation a n (MvPowerSeries.C r)) = finiteEvaluation a m (MvPowerSeries.C r)
39     rw [MvPowerSeries.c_eq_algebraMap, (finiteEvaluation a n).commutes r, (finiteEvaluation a m).commutes r]
40     rfl
41   · intro i
42     change Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal R) h
43       (finiteEvaluation a n (MvPowerSeries.X i)) = finiteEvaluation a m (MvPowerSeries.X i)
44     simp
45   · intro i
46     simpa only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
47       finiteEvaluation_X] using (parameter_reduction_nilpotent (a i) n).map
48         (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal R) h)
49 
50 noncomputable def evaluationFamily {d : ℕ} (a : Fin d → IsLocalRing.maximalIdeal R) :
51     PaperX.Reconstruction.RingFamily (MvPowerSeries (Fin d) R) (IsLocalRing.maximalIdeal R) where
52   maps n := (finiteEvaluation a n).toRingHom
53   compatible := finiteEvaluation_compatible a
54 
55 /-- Genuine local algebra maps to the coefficient ring. -/
56 def IntegralPoint (d : ℕ) :=
57   {f : MvPowerSeries (Fin d) R →ₐ[R] R // IsLocalHom f.toRingHom}
58 
59 noncomputable def integralParameters {d : ℕ} (f : IntegralPoint (R := R) d) :
60     Fin d → IsLocalRing.maximalIdeal R := by
61   let : IsLocalHom f.val.toRingHom := f.property
62   exact fun i => ⟨f.val (MvPowerSeries.X i), map_nonunit f.val.toRingHom _ (variable_nonunit d i)⟩
63 
64 /-- A local integral map has exactly the expected finite evaluations. -/
65 theorem integral_map_reduces {d : ℕ} (f : IntegralPoint (R := R) d) (n : ℕ) :
66     (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R ^ n)).comp f.val.toRingHom =
67       (finiteEvaluation (integralParameters f) n).toRingHom := by
68   apply nilpotent_hom_ext d
69   · intro r
70     change Ideal.Quotient.mk _ (f.val (MvPowerSeries.C r)) =
71       finiteEvaluation (integralParameters f) n (MvPowerSeries.C r)
72     rw [MvPowerSeries.c_eq_algebraMap, f.val.commutes r, (finiteEvaluation _ n).commutes r]
73     rfl
74   · intro i
75     simp only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, finiteEvaluation_X]
76     rfl
77   · intro i
78     exact parameter_reduction_nilpotent (integralParameters f i) n
79 
80 /-- Continuity is in the maximal-ideal adic topologies, not an auxiliary discrete topology. -/
81 theorem integralPoint_continuous {d : ℕ} (f : IntegralPoint (R := R) d) :
82     @Continuous _ _ (IsLocalRing.maximalIdeal (MvPowerSeries (Fin d) R)).adicTopology
83       (IsLocalRing.maximalIdeal R).adicTopology f.val := by
84   let : IsLocalHom f.val.toRingHom := f.property
85   exact PaperX.Reconstruction.local_map_continuous f.val.toRingHom
86 
87 variable [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
88 
89 /-- Build the actual integral algebra map from the compatible quotient evaluations. -/
90 noncomputable def integralEval {d : ℕ} (a : Fin d → IsLocalRing.maximalIdeal R) :
91     MvPowerSeries (Fin d) R →ₐ[R] R :=
92   PaperX.Reconstruction.reconstructAlg (IsLocalRing.maximalIdeal R) (evaluationFamily a)
93     (fun n r => (finiteEvaluation a n).commutes r)
94 
95 theorem integralEval_reduces {d : ℕ} (a : Fin d → IsLocalRing.maximalIdeal R) (n : ℕ) :
96     (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R ^ n)).comp (integralEval a).toRingHom =
97       (finiteEvaluation a n).toRingHom :=
98   PaperX.Reconstruction.reconstruct_reduces _ (evaluationFamily a) n
99 
100 @[simp] theorem integralEval_X {d : ℕ}
101     (a : Fin d → IsLocalRing.maximalIdeal R) (i : Fin d) :
102     integralEval a (MvPowerSeries.X i) = (a i).val := by
103   apply congrFun (IsHausdorff.funext' (IsLocalRing.maximalIdeal R)
104     (f := fun _ : Unit => integralEval a (MvPowerSeries.X i))
105     (g := fun _ : Unit => (a i).val) ?_) ()
106   intro n _
107   have h := congrArg (fun f : MvPowerSeries (Fin d) R →+* (R ⧸ IsLocalRing.maximalIdeal R ^ n) =>
108     f (MvPowerSeries.X i)) (integralEval_reduces a n)
109   simpa using h
110 
111 /-- Locality follows from the first positive finite evaluation. -/
112 theorem integralEval_local {d : ℕ} (a : Fin d → IsLocalRing.maximalIdeal R) :
113     IsLocalHom (integralEval a).toRingHom := by
114   apply PaperX.Reconstruction.reconstruct_isLocal
115   let : Nontrivial (R ⧸ IsLocalRing.maximalIdeal R ^ (0+1)) := quotient_nontrivial R 0
116   let : IsLocalRing (R ⧸ IsLocalRing.maximalIdeal R ^ (0+1)) := quotient_local R 0
117   let : IsLocalHom (algebraMap R (R ⧸ IsLocalRing.maximalIdeal R ^ (0+1))) := quotient_map_local R 0
118   apply nilpotent_map_isLocal (finiteEvaluation a 1)
119   intro i
120   simpa using parameter_reduction_nilpotent (a i) 1
121 
122 /-- Equality at every precision yields uniqueness of the integral map. -/
123 theorem integralEval_unique {d : ℕ} (f : IntegralPoint (R := R) d) :
124     integralEval (integralParameters f) = f.val := by
125   have h := PaperX.Reconstruction.reconstruct_unique (IsLocalRing.maximalIdeal R)
126     (evaluationFamily (integralParameters f)) f.val.toRingHom (integral_map_reduces f)
127   ext p
128   exact congrArg (fun F : MvPowerSeries (Fin d) R →+* R => F p) h.symm
129 
130 /-- Complete local formal points are precisely arbitrary tuples in the maximal ideal. -/
131 noncomputable def integralPointEquiv (d : ℕ) : IntegralPoint (R := R) d ≃
132     (Fin d → IsLocalRing.maximalIdeal R) where
133   toFun := integralParameters
134   invFun a := ⟨integralEval a, integralEval_local a⟩
135   left_inv f := Subtype.ext (integralEval_unique f)
136   right_inv a := by
137     funext i
138     exact Subtype.ext (integralEval_X a i)
139 
140 end PaperX.IntegralCharts

Back to source controls