SmoothModels.lean

1 import PaperX.Digits
2 
3 /-! Transfer of the canonical smooth chart along a supplied coefficient-algebra
4 isomorphism. Smoothness/representability are not asserted without that datum. -/
5 set_option autoImplicit false
6 namespace PaperX.SmoothModels
7 variable {R A B S : Type*} [CommRing R] [CommRing A] [CommRing B] [CommRing S]
8 variable [Algebra R A] [Algebra R B] [Algebra R S]
9 
10 /-- Local coefficient-preserving maps with their actual algebra-hom structure. -/
11 def LocalMaps (R A S : Type*) [CommRing R] [CommRing A] [CommRing S]
12     [Algebra R A] [Algebra R S] := {f : A →ₐ[R] S // IsLocalHom f.toRingHom}
13 
14 /-- A declared smooth coordinate isomorphism transports all local maps, not only
15 some constructed subset of them. -/
16 noncomputable def localMapCongr (E : A ≃ₐ[R] B) : LocalMaps R A S ≃ LocalMaps R B S where
17   toFun f := ⟨f.val.comp E.symm.toAlgHom, by
18     let : IsLocalHom f.val.toRingHom := f.property
19     constructor
20     intro x hx
21     have h := isUnit_of_map_unit f.val.toRingHom _ hx
22     simpa using h.map E.toRingHom⟩
23   invFun f := ⟨f.val.comp E.toAlgHom, by
24     let : IsLocalHom f.val.toRingHom := f.property
25     constructor
26     intro x hx
27     have h := isUnit_of_map_unit f.val.toRingHom _ hx
28     simpa using h.map E.symm.toRingHom⟩
29   left_inv f := by
30     apply Subtype.ext
31     ext p
32     simp
33   right_inv f := by
34     apply Subtype.ext
35     ext p
36     simp
37 
38 
39 /-- Formal-model points at depth n+1, classified by actual ideal-image tuples. -/
40 noncomputable def modelPointEquiv [IsLocalRing R] {d : ℕ}
41     (E : A ≃ₐ[R] MvPowerSeries (Fin d) R) (n : ℕ) :
42     LocalMaps R A (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) ≃
43       PaperX.Counting.WeightedChart (IsLocalRing.maximalIdeal R) (fun _ : Fin d => 1) (n+1) :=
44   (localMapCongr E).trans (PaperX.SmoothMaps.pointEquiv R d n)
45 
46 /-- Integral formal-model points and d independent residue streams. -/
47 noncomputable def modelDigitEquiv [IsDomain R] [IsDiscreteValuationRing R]
48     [IsAdicComplete (IsLocalRing.maximalIdeal R) R] {d : ℕ}
49     (E : A ≃ₐ[R] MvPowerSeries (Fin d) R) {π : R} (hπ : Irreducible π)
50     (s : IsLocalRing.ResidueField R → R)
51     (hs : Function.RightInverse s (IsLocalRing.residue R)) :
52     LocalMaps R A R ≃ (Fin d → ℕ → IsLocalRing.ResidueField R) :=
53   (localMapCongr E).trans (PaperX.Digits.integralPointDigitEquiv hπ s hs d)
54 
55 /-- Continuity is automatic for local maps in the maximal-ideal adic topologies. -/
56 theorem localMap_continuous [IsLocalRing A] [IsLocalRing S] (f : LocalMaps R A S) :
57     @Continuous _ _ (IsLocalRing.maximalIdeal A).adicTopology
58       (IsLocalRing.maximalIdeal S).adicTopology f.val := by
59   let : IsLocalHom f.val.toRingHom := f.property
60   exact PaperX.Reconstruction.local_map_continuous f.val.toRingHom
61 
62 /-- Full smooth formal-model count, conditional on the specified algebra isomorphism. -/
63 theorem smooth_model_count [IsDomain R] [IsDiscreteValuationRing R]
64     [Finite (R ⧸ IsLocalRing.maximalIdeal R)] {d : ℕ}
65     (E : A ≃ₐ[R] MvPowerSeries (Fin d) R) (n : ℕ) :
66     Nat.card (LocalMaps R A (R ⧸ IsLocalRing.maximalIdeal R ^ (n+1))) =
67       Nat.card (R ⧸ IsLocalRing.maximalIdeal R) ^ (d*n) := by
68   rw [Nat.card_congr (localMapCongr (S := R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) E)]
69   exact PaperX.SmoothMaps.smooth_point_count R d n
70 
71 /-- Series defined from all actual local maps of the supplied representing ring. -/
72 noncomputable def modelZeta [IsLocalRing R] : PowerSeries ℚ :=
73   PowerSeries.mk fun m => if m = 0 then 0 else
74     (Nat.card (LocalMaps R A (R ⧸ IsLocalRing.maximalIdeal R ^ m)) : ℚ)
75 
76 /-- Full smooth formal-model zeta identity. -/
77 theorem smooth_model_zeta [IsDomain R] [IsDiscreteValuationRing R]
78     [Finite (R ⧸ IsLocalRing.maximalIdeal R)] {d : ℕ}
79     (E : A ≃ₐ[R] MvPowerSeries (Fin d) R) :
80     modelZeta (R := R) (A := A) = PowerSeries.X *
81       (1 - PowerSeries.C ((Nat.card (R ⧸ IsLocalRing.maximalIdeal R) : ℚ)^d) * PowerSeries.X)⁻¹ := by
82   rw [← PaperX.SmoothMaps.smooth_point_zeta R d]
83   ext m
84   cases m with
85   | zero => simp [modelZeta, PaperX.SmoothMaps.pointZeta]
86   | succ n =>
87     simp only [modelZeta, PaperX.SmoothMaps.pointZeta, PowerSeries.coeff_mk,
88       Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, ↓reduceIte, Nat.add_sub_cancel]
89     exact congrArg (fun k : ℕ => (k : ℚ)) (Nat.card_congr (localMapCongr
90       (S := R ⧸ IsLocalRing.maximalIdeal R ^ (n+1)) E))
91 
92 end PaperX.SmoothModels

Back to source controls