FormalCharts.lean

1 import PaperX.Counting
2 import PaperX.Reconstruction
3 import Mathlib.RingTheory.MvPowerSeries.Equiv
4 import Mathlib.RingTheory.MvPowerSeries.Evaluation
5 import Mathlib.Topology.UniformSpace.DiscreteUniformity
6 
7 /-! Finite-variable formal power-series maps into nilpotent thickenings.
8 The uniqueness argument is algebraic, so it does not assume the desired
9 map-to-parameter correspondence or hide a continuity hypothesis. -/
10 set_option autoImplicit false
11 namespace PaperX.FormalCharts
12 
13 variable {R S : Type*} [CommRing R] [CommRing S]
14 
15 /-- A map killing a power of X only sees a finite truncation. -/
16 theorem hom_eq_on_trunc (f : PowerSeries R →+* S) (n : ℕ)
17     (hn : f PowerSeries.X ^ n = 0) (p : PowerSeries R) :
18     f p = f (p.trunc n : PowerSeries R) := by
19   conv_lhs => rw [p.eq_X_pow_mul_shift_add_trunc n]
20   simp [hn]
21 
22 /-- Algebraic uniqueness for one variable with nilpotent image. -/
23 theorem univariate_hom_ext (f g : PowerSeries R →+* S)
24     (hC : ∀ r, f (PowerSeries.C r) = g (PowerSeries.C r))
25     (hX : f PowerSeries.X = g PowerSeries.X)
26     (hnil : IsNilpotent (f PowerSeries.X)) : f = g := by
27   obtain ⟨n, hn⟩ := hnil
28   have hg : g PowerSeries.X ^ n = 0 := by rw [← hX]; exact hn
29   have hp : ∀ p : Polynomial R, f (p : PowerSeries R) = g (p : PowerSeries R) := by
30     intro p
31     induction p using Polynomial.induction_on' with
32     | add p q hp hq => simpa using congrArg₂ (· + ·) hp hq
33     | monomial n r => simp [PowerSeries.monomial_eq_C_mul_X_pow, hC, hX]
34   ext p
35   rw [hom_eq_on_trunc f n hn, hom_eq_on_trunc g n hg]
36   exact hp _
37 
38 @[simp] theorem finSucc_symm_C (d : ℕ) (r : R) :
39     (MvPowerSeries.finSuccEquiv R d).symm (PowerSeries.C (MvPowerSeries.C r)) =
40       MvPowerSeries.C r := by
41   apply (MvPowerSeries.finSuccEquiv R d).injective
42   simp
43 
44 @[simp] theorem finSucc_symm_X (d : ℕ) :
45     (MvPowerSeries.finSuccEquiv R d).symm PowerSeries.X = MvPowerSeries.X 0 := by
46   apply (MvPowerSeries.finSuccEquiv R d).injective
47   simp
48 
49 @[simp] theorem finSucc_symm_C_X (d : ℕ) (i : Fin d) :
50     (MvPowerSeries.finSuccEquiv R d).symm (PowerSeries.C (MvPowerSeries.X i)) =
51       MvPowerSeries.X i.succ := by
52   apply (MvPowerSeries.finSuccEquiv R d).injective
53   simp
54 
55 /-- Every ring map with nilpotent parameter images is determined by constants
56 and parameters. No topology on the source or target is assumed. -/
57 theorem nilpotent_hom_ext (d : ℕ)
58     (f g : MvPowerSeries (Fin d) R →+* S)
59     (hC : ∀ r, f (MvPowerSeries.C r) = g (MvPowerSeries.C r))
60     (hX : ∀ i, f (MvPowerSeries.X i) = g (MvPowerSeries.X i))
61     (hnil : ∀ i, IsNilpotent (f (MvPowerSeries.X i))) : f = g := by
62   induction d with
63   | zero =>
64     ext p
65     have hp : MvPowerSeries.C (MvPowerSeries.constantCoeff p) = p :=
66       (MvPowerSeries.isEmptyEquiv (Fin 0) R).left_inv p
67     rw [← hp]
68     exact hC _
69   | succ d ih =>
70     let E := MvPowerSeries.finSuccEquiv R d
71     let f' := f.comp E.symm.toRingHom
72     let g' := g.comp E.symm.toRingHom
73     have hcoeff : f'.comp PowerSeries.C = g'.comp PowerSeries.C := by
74       apply ih
75       · intro r
76         simpa [f', g', E] using hC r
77       · intro i
78         simpa [f', g', E] using hX i.succ
79       · intro i
80         simpa [f', E] using hnil i.succ
81     have heq : f' = g' := by
82       apply univariate_hom_ext
83       · intro p
84         exact congrArg (fun h : MvPowerSeries (Fin d) R →+* S => h p) hcoeff
85       · simpa [f', g', E] using hX 0
86       · simpa [f', E] using hnil 0
87     ext p
88     have hh := congrArg (fun h : PowerSeries (MvPowerSeries (Fin d) R) →+* S => h (E p)) heq
89     simpa [f', g', E] using hh
90 
91 
92 
93 /-- Evaluation at finitely many nilpotents, with discrete auxiliary topologies.
94 This is an actual ring homomorphism supplied by Mathlib's evaluation theorem. -/
95 noncomputable def nilEval {d : ℕ} (φ : R →+* S) (a : Fin d → S)
96     (ha : ∀ i, IsNilpotent (a i)) : MvPowerSeries (Fin d) R →+* S := by
97   let : UniformSpace R := ⊥
98   let : UniformSpace S := ⊥
99   apply MvPowerSeries.eval₂Hom (φ := φ) (a := a) continuous_of_discreteTopology
100   exact ⟨fun i => (ha i).isTopologicallyNilpotent, by simp⟩
101 
102 @[simp] theorem nilEval_C {d : ℕ} (φ : R →+* S) (a : Fin d → S)
103     (ha : ∀ i, IsNilpotent (a i)) (r : R) :
104     nilEval φ a ha (MvPowerSeries.C r) = φ r := by
105   let : UniformSpace R := ⊥
106   let : UniformSpace S := ⊥
107   unfold nilEval
108   rw [MvPowerSeries.coe_eval₂Hom]
109   exact MvPowerSeries.eval₂_C φ a r
110 
111 @[simp] theorem nilEval_X {d : ℕ} (φ : R →+* S) (a : Fin d → S)
112     (ha : ∀ i, IsNilpotent (a i)) (i : Fin d) :
113     nilEval φ a ha (MvPowerSeries.X i) = a i := by
114   let : UniformSpace R := ⊥
115   let : UniformSpace S := ⊥
116   unfold nilEval
117   rw [MvPowerSeries.coe_eval₂Hom]
118   exact MvPowerSeries.eval₂_X φ a i
119 
120 /-- Coefficient-preserving evaluation into an R-algebra. -/
121 noncomputable def nilAeval [Algebra R S] {d : ℕ} (a : Fin d → S)
122     (ha : ∀ i, IsNilpotent (a i)) : MvPowerSeries (Fin d) R →ₐ[R] S where
123   __ := nilEval (algebraMap R S) a ha
124   commutes' r := nilEval_C _ a ha r
125 
126 @[simp] theorem nilAeval_X [Algebra R S] {d : ℕ} (a : Fin d → S)
127     (ha : ∀ i, IsNilpotent (a i)) (i : Fin d) :
128     nilAeval (R := R) a ha (MvPowerSeries.X i) = a i := nilEval_X (algebraMap R S) a ha i
129 
130 /-- Parameter images determine the actual algebra map, not a separately
131 postulated equivalence. -/
132 theorem nilpotent_algHom_ext [Algebra R S] {d : ℕ}
133     (f g : MvPowerSeries (Fin d) R →ₐ[R] S)
134     (hX : ∀ i, f (MvPowerSeries.X i) = g (MvPowerSeries.X i))
135     (hnil : ∀ i, IsNilpotent (f (MvPowerSeries.X i))) : f = g := by
136   have H := nilpotent_hom_ext d f.toRingHom g.toRingHom
137     (fun r => (f.commutes r).trans (g.commutes r).symm) hX hnil
138   ext p
139   exact congrArg (fun h : MvPowerSeries (Fin d) R →+* S => h p) H
140 
141 /-- Exact universal property for nilpotent parameter images. -/
142 noncomputable def nilpotentParameterEquiv [Algebra R S] (d : ℕ) :
143     {f : MvPowerSeries (Fin d) R →ₐ[R] S // ∀ i, IsNilpotent (f (MvPowerSeries.X i))} ≃
144     (Fin d → {x : S // IsNilpotent x}) where
145   toFun f i := ⟨f.val (MvPowerSeries.X i), f.property i⟩
146   invFun a := ⟨nilAeval (fun i => (a i).val) (fun i => (a i).property), by
147     intro i; simpa using (a i).property⟩
148   left_inv f := by
149     apply Subtype.ext
150     apply nilpotent_algHom_ext
151     · simp
152     · simpa using f.property
153   right_inv a := by
154     funext i
155     exact Subtype.ext (by simp)
156 
157 end PaperX.FormalCharts

Back to source controls