SmoothMaps.lean

1 import PaperX.FormalCharts
2 import PaperX.Zeta
3 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
4 
5 /-! Actual local algebra maps out of a finite-variable power-series ring.
6 Finite nilpotent evaluation is bridged to ideal-image coordinates, and then to
7 the previously proved counts and rational series. -/
8 set_option autoImplicit false
9 namespace PaperX.SmoothMaps
10 open PaperX.FormalCharts
11 
12 variable {R S : Type*} [CommRing R] [CommRing S]
13 
14 /-- A power-series parameter is a nonunit. -/
15 theorem variable_nonunit [IsLocalRing R] (d : ℕ) (i : Fin d) :
16     MvPowerSeries.X i ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin d) R) := by
17   change ¬ IsUnit (MvPowerSeries.X i : MvPowerSeries (Fin d) R)
18   simp [MvPowerSeries.isUnit_iff_constantCoeff]
19 
20 /-- Reduction of a nilpotent-parameter map is its constant-coefficient map. -/
21 theorem residue_map_eq [IsLocalRing S] [Algebra R S] {d : ℕ}
22     (f : MvPowerSeries (Fin d) R →ₐ[R] S)
23     (hnil : ∀ i, IsNilpotent (f (MvPowerSeries.X i))) :
24     (IsLocalRing.residue S).comp f.toRingHom =
25       ((IsLocalRing.residue S).comp (algebraMap R S)).comp MvPowerSeries.constantCoeff := by
26   apply nilpotent_hom_ext d
27   · intro r
28     simp only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
29       MvPowerSeries.constantCoeff_C]
30     exact congrArg (IsLocalRing.residue S) (f.commutes r)
31   · intro i
32     simp only [RingHom.comp_apply, MvPowerSeries.constantCoeff_X, map_zero]
33     exact ((hnil i).map (IsLocalRing.residue S)).eq_zero
34   · intro i
35     exact (hnil i).map (IsLocalRing.residue S)
36 
37 /-- Nilpotent parameter images give a local map when the coefficient map is local. -/
38 theorem nilpotent_map_isLocal [IsLocalRing R] [IsLocalRing S] [Algebra R S]
39     [IsLocalHom (algebraMap R S)] {d : ℕ}
40     (f : MvPowerSeries (Fin d) R →ₐ[R] S)
41     (hnil : ∀ i, IsNilpotent (f (MvPowerSeries.X i))) : IsLocalHom f.toRingHom := by
42   constructor
43   intro p hp
44   apply MvPowerSeries.isUnit_iff_constantCoeff.mpr
45   apply isUnit_of_map_unit (algebraMap R S)
46   apply (IsLocalRing.residue_ne_zero_iff_isUnit _).mp
47   have he := congrArg (fun h : MvPowerSeries (Fin d) R →+* IsLocalRing.ResidueField S => h p)
48     (residue_map_eq f hnil)
49   change IsLocalRing.residue S (f p) =
50     IsLocalRing.residue S (algebraMap R S (MvPowerSeries.constantCoeff p)) at he
51   rw [← he]
52   exact (IsUnit.map (IsLocalRing.residue S) hp).ne_zero
53 
54 variable (R)
55 section Local
56 variable [IsLocalRing R]
57 
58 /-- The actual quotient at positive depth is nontrivial. -/
59 theorem quotient_nontrivial (n : ℕ) : Nontrivial (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) := by
60   apply Ideal.Quotient.nontrivial_iff.mpr
61   exact ne_top_of_le_ne_top (IsLocalRing.maximalIdeal.isMaximal R).ne_top
62     (Ideal.pow_le_self (Nat.succ_ne_zero n))
63 attribute [local instance] quotient_nontrivial
64 
65 /-- Positive-depth quotients remain local rings. -/
66 theorem quotient_local (n : ℕ) : IsLocalRing (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) := by
67   let : IsLocalHom (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R ^ (n+1))) :=
68     IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
69   exact IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective
70 attribute [local instance] quotient_local
71 
72 /-- The coefficient quotient map is local. -/
73 theorem quotient_map_local (n : ℕ) :
74     IsLocalHom (algebraMap R (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1))) := by
75   exact IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
76 attribute [local instance] quotient_map_local
77 
78 /-- Actual local coefficient-preserving maps; n=0 denotes precision one. -/
79 def Point (d n : ℕ) :=
80   {f : MvPowerSeries (Fin d) R →ₐ[R] (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) //
81     IsLocalHom f.toRingHom}
82 
83 /-- Every positive-depth coordinate is genuinely nilpotent in the quotient. -/
84 theorem coordinate_nilpotent (n : ℕ)
85     (x : PaperX.Counting.Coordinate (IsLocalRing.maximalIdeal R) (n+1) 1) :
86     IsNilpotent x.val := by
87   obtain ⟨a, ha, hx⟩ := Submodule.mem_map.mp x.property
88   rw [pow_one] at ha
89   refine ⟨n+1, ?_⟩
90   change Ideal.Quotient.mk _ a = x.val at hx
91   rw [← hx, ← map_pow, Ideal.Quotient.eq_zero_iff_mem]
92   exact Ideal.pow_mem_pow ha _
93 
94 /-- The local quotient maximal ideal is exactly the positive-depth coordinate image. -/
95 theorem coordinate_iff_maximal (n : ℕ)
96     (x : R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) :
97     x ∈ Submodule.map (IsLocalRing.maximalIdeal R ^ (n+1)).mkQ
98       (IsLocalRing.maximalIdeal R ^ 1) ↔
99     x ∈ IsLocalRing.maximalIdeal (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) := by
100   rw [← IsLocalRing.map_maximalIdeal_of_surjective
101     (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R ^ (n+1))) Ideal.Quotient.mk_surjective]
102   rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective, Submodule.mem_map]
103   simp only [pow_one]
104   rfl
105 
106 /-- A local map must send every formal parameter into the positive-depth ideal. -/
107 noncomputable def parameters (d n : ℕ) (f : Point R d n) :
108     PaperX.Counting.WeightedChart (IsLocalRing.maximalIdeal R) (fun _ : Fin d => 1) (n+1) := by
109   let : IsLocalHom f.val.toRingHom := f.property
110   exact fun i => ⟨f.val (MvPowerSeries.X i), (coordinate_iff_maximal R n _).mpr
111     (map_nonunit f.val.toRingHom _ (variable_nonunit d i))⟩
112 
113 /-- Evaluation of any parameter tuple gives an actual local algebra homomorphism. -/
114 noncomputable def fromParameters (d n : ℕ)
115     (a : PaperX.Counting.WeightedChart (IsLocalRing.maximalIdeal R) (fun _ : Fin d => 1) (n+1)) :
116     Point R d n :=
117   ⟨nilAeval (fun i => (a i).val) (fun i => coordinate_nilpotent R n (a i)), by
118     apply nilpotent_map_isLocal
119     intro i
120     simpa using coordinate_nilpotent R n (a i)⟩
121 
122 /-- The missing smooth formal-map-to-parameter equivalence, with both inverses. -/
123 noncomputable def pointEquiv (d n : ℕ) : Point R d n ≃
124     PaperX.Counting.WeightedChart (IsLocalRing.maximalIdeal R) (fun _ : Fin d => 1) (n+1) where
125   toFun := parameters R d n
126   invFun := fromParameters R d n
127   left_inv f := by
128     apply Subtype.ext
129     apply nilpotent_algHom_ext
130     · intro i; simp [fromParameters, parameters]
131     · intro i; simp only [fromParameters, nilAeval_X]
132       exact coordinate_nilpotent R n (parameters R d n f i)
133   right_inv a := by
134     funext i
135     apply Subtype.ext
136     simp [parameters, fromParameters]
137 
138 
139 
140 /-- Every local point is continuous in the actual maximal-ideal adic topologies. -/
141 theorem point_continuous (d n : ℕ) (f : Point R d n) :
142     @Continuous _ _ (IsLocalRing.maximalIdeal (MvPowerSeries (Fin d) R)).adicTopology
143       (IsLocalRing.maximalIdeal (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1))).adicTopology f.val := by
144   let : IsLocalHom f.val.toRingHom := f.property
145   exact PaperX.Reconstruction.local_map_continuous f.val.toRingHom
146 
147 /-- Zero constant coefficient; coefficient m>=1 counts the actual local maps at precision m. -/
148 noncomputable def pointZeta (d : ℕ) : PowerSeries ℚ :=
149   PowerSeries.mk fun m => if m = 0 then 0 else (Nat.card (Point R d (m-1)) : ℚ)
150 
151 end Local
152 
153 /-- Actual local maps on the smooth formal component, counted at every positive precision. -/
154 theorem smooth_point_count [IsDomain R] [IsDiscreteValuationRing R]
155     [Finite (R ⧸ IsLocalRing.maximalIdeal R)] (d n : ℕ) :
156     Nat.card (Point R d n) = Nat.card (R ⧸ IsLocalRing.maximalIdeal R) ^ (d*n) := by
157   rw [Nat.card_congr (pointEquiv R d n)]
158   simpa [PaperX.Counting.residueCard] using
159     PaperX.Counting.smooth_chart_count (IsLocalRing.maximalIdeal R)
160       (IsDiscreteValuationRing.not_a_field R) d (n+1)
161 
162 /-- The smooth deformation zeta formula now counts actual homomorphisms. -/
163 theorem smooth_point_zeta [IsDomain R] [IsDiscreteValuationRing R]
164     [Finite (R ⧸ IsLocalRing.maximalIdeal R)] (d : ℕ) :
165     pointZeta R d = PowerSeries.X *
166       (1 - PowerSeries.C ((Nat.card (R ⧸ IsLocalRing.maximalIdeal R) : ℚ)^d) * PowerSeries.X)⁻¹ := by
167   rw [← PaperX.Zeta.smooth_zeta_formula]
168   ext m
169   simp [pointZeta, PaperX.Zeta.modelZeta, PaperX.Zeta.weightedCoeff, smooth_point_count]
170 
171 end PaperX.SmoothMaps

Back to source controls