RamificationPolyphaseDimensions.lean

1 import PaperXI.RamificationPolyphase
2 import PaperXI.RamificationSeparation
3 import Mathlib.Tactic
4 
5 /-! # Dimension and conductor accounting for ramification details
6 
7 The literal depth projectors split every successive fixed space into its previous
8 coarse part and one newly visible detail range.  In finite dimension, the detail
9 ranks telescope to the whole representation and give a finite tail formula for
10 every lower-numbering codimension.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 open scoped Classical BigOperators
15 
16 namespace PaperXI.RamificationPolyphaseDimensions
17 
18 open PaperXI.ResidueWeil
19 open PaperXI.ValuationRamification
20 open PaperXI.ValuationConductor
21 open PaperXI.RamificationPolyphase
22 open PaperXI.FiniteAverage
23 
24 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [Fintype D]
25   [MulSemiringAction D R]
26 variable (F : RingAut (IsLocalRing.ResidueField R))
27 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
28 variable (ρ : Representation ℂ (Pullback (residue R D) F) V)
29 
30 /-- The actual subspace carried by the detail projector at depth `i`. -/
31 def detailSpace (i : ℕ) : Submodule ℂ V :=
32   LinearMap.range
33     (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i)
34 
35 omit [Fintype D] in
36 /-- Fixed spaces increase as the lower ramification subgroup decreases. -/
37 theorem fixed_mono {i j : ℕ} (hij : i ≤ j) :
38     fixed R D F ρ i ≤ fixed R D F ρ j := by
39   intro v hv g
40   have h := hv (lowerInclusion (R := R) (D := D) hij g)
41   change ρ (lift R D F i (lowerInclusion (R := R) (D := D) hij g)) v = v at h
42   change ρ (lift R D F j g) v = v
43   simpa only [lift_lowerInclusion] using h
44 
45 /-- The next fixed space is the sum of the preceding fixed space and the new
46 detail channel. -/
47 theorem fixed_succ_eq_sup_detail (i : ℕ) :
48     fixed R D F ρ (i+1) = fixed R D F ρ i ⊔ detailSpace R D F ρ i := by
49   apply le_antisymm
50   · intro v hv
51     have hcoarse : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v ∈
52         fixed R D F ρ i :=
53       invariant _ v
54     have hdetail : detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i v ∈
55         detailSpace R D F ρ i :=
56       ⟨v, rfl⟩
57     have hnext : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v = v :=
58       fixes _ hv
59     have hdecomp : v =
60         depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v +
61           detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
62       rw [detailProjector_apply, hnext]
63       abel
64     rw [hdecomp]
65     exact Submodule.add_mem _
66       ((le_sup_left : fixed R D F ρ i ≤ fixed R D F ρ i ⊔ detailSpace R D F ρ i)
67         hcoarse)
68       ((le_sup_right : detailSpace R D F ρ i ≤ fixed R D F ρ i ⊔ detailSpace R D F ρ i)
69         hdetail)
70   · apply sup_le
71     · exact fixed_mono R D F ρ (Nat.le_succ i)
72     · rw [detailSpace, detailProjector_range]
73       exact inf_le_left
74 
75 /-- The previous fixed space and the new detail channel intersect trivially. -/
76 theorem fixed_disjoint_detail (i : ℕ) :
77     Disjoint (fixed R D F ρ i) (detailSpace R D F ρ i) := by
78   rw [disjoint_iff_inf_le]
79   intro v hv
80   have hvfix : v ∈ fixed R D F ρ i := hv.1
81   have hvdetail : v ∈ detailSpace R D F ρ i := hv.2
82   have hfix : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v = v :=
83     fixes _ hvfix
84   have hker : v ∈ LinearMap.ker
85       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i) := by
86     rw [detailSpace, detailProjector_range] at hvdetail
87     exact hvdetail.2
88   have hzero := LinearMap.mem_ker.mp hker
89   have hvzero : v = 0 := hfix.symm.trans hzero
90   rw [hvzero]
91   exact Submodule.zero_mem _
92 
93 variable [FiniteDimensional ℂ V]
94 
95 /-- Successive fixed-space dimensions differ by the rank of the corresponding
96 detail channel. -/
97 theorem finrank_fixed_succ (i : ℕ) :
98     Module.finrank ℂ (fixed R D F ρ (i+1)) =
99       Module.finrank ℂ (fixed R D F ρ i) +
100         Module.finrank ℂ (detailSpace R D F ρ i) := by
101   have h := Submodule.finrank_sup_add_finrank_inf_eq
102     (fixed R D F ρ i) (detailSpace R D F ρ i)
103   rw [← fixed_succ_eq_sup_detail R D F ρ i,
104     (fixed_disjoint_detail R D F ρ i).eq_bot] at h
105   simpa using h
106 
107 /-- Prefix form of the ramification multiresolution dimension identity. -/
108 theorem finrank_fixed_eq_base_add_details (n : ℕ) :
109     Module.finrank ℂ (fixed R D F ρ n) =
110       Module.finrank ℂ (fixed R D F ρ 0) +
111         ∑ i ∈ Finset.range n, Module.finrank ℂ (detailSpace R D F ρ i) := by
112   induction n with
113   | zero => simp
114   | succ n ih =>
115       rw [finrank_fixed_succ R D F ρ n, ih, Finset.sum_range_succ, add_assoc]
116 
117 /-- Once the lower filtration is trivial, the inertia-fixed rank plus all detail
118 ranks equals the full representation dimension. -/
119 theorem finrank_eq_inertia_add_details {N : ℕ} (hN : lower R D N = ⊥) :
120     Module.finrank ℂ V =
121       Module.finrank ℂ (fixed R D F ρ 0) +
122         ∑ i ∈ Finset.range N, Module.finrank ℂ (detailSpace R D F ρ i) := by
123   have h := finrank_fixed_eq_base_add_details R D F ρ N
124   rw [fixed_top_of_lower_bot R D F ρ N hN] at h
125   simpa using h
126 
127 
128 section Termination
129 
130 variable [IsNoetherianRing R] [FaithfulSMul D R]
131 
132 omit [FiniteDimensional ℂ V] in
133 /-- For a finite faithful action on a Noetherian local ring, the finite
134 polyphase reconstruction exists without supplying a cutoff. -/
135 theorem exists_identity_eq_inertia_add_details :
136     ∃ N : ℕ, (1 : Module.End ℂ V) =
137       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) 0 +
138         ∑ i ∈ Finset.range N,
139           detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
140   obtain ⟨N, hN⟩ := PaperXI.RamificationSeparation.eventually_trivial R D
141   exact ⟨N, identity_eq_inertia_add_details (R := R) (D := D)
142     (F := F) (ρ := ρ) (hN N le_rfl)⟩
143 
144 /-- The corresponding finite-dimensional rank decomposition also exists under
145 the same derived termination hypotheses. -/
146 theorem exists_finrank_eq_inertia_add_details :
147     ∃ N : ℕ, Module.finrank ℂ V =
148       Module.finrank ℂ (fixed R D F ρ 0) +
149         ∑ i ∈ Finset.range N, Module.finrank ℂ (detailSpace R D F ρ i) := by
150   obtain ⟨N, hN⟩ := PaperXI.RamificationSeparation.eventually_trivial R D
151   exact ⟨N, finrank_eq_inertia_add_details R D F ρ (hN N le_rfl)⟩
152 
153 end Termination
154 
155 /-- Each lower fixed-space codimension is the sum of the unresolved detail
156 ranks at that depth and above, up to any valid triviality cutoff. -/
157 theorem codimension_eq_detail_tail {i N : ℕ} (hiN : i ≤ N)
158     (hN : lower R D N = ⊥) :
159     codimension R D F ρ i =
160       ∑ j ∈ Finset.Ico i N, Module.finrank ℂ (detailSpace R D F ρ j) := by
161   have hNdim := finrank_eq_inertia_add_details R D F ρ hN
162   have hidim := finrank_fixed_eq_base_add_details R D F ρ i
163   have hsplit := Finset.sum_range_add_sum_Ico
164     (fun j => Module.finrank ℂ (detailSpace R D F ρ j)) hiN
165   unfold codimension
166   omega
167 
168 /-- The conventional lower-numbering summand is exactly its ramification-group
169 weight times the unresolved polyphase tail. -/
170 theorem summand_eq_weight_mul_detail_tail {i N : ℕ} (hiN : i ≤ N)
171     (hN : lower R D N = ⊥) :
172     summand R D F ρ i =
173       (Nat.card (lower R D i) : ℝ) / (Nat.card (lower R D 0) : ℝ) *
174         (∑ j ∈ Finset.Ico i N,
175           (Module.finrank ℂ (detailSpace R D F ρ j) : ℝ)) := by
176   unfold summand
177   rw [codimension_eq_detail_tail R D F ρ hiN hN]
178   norm_cast
179 
180 end PaperXI.RamificationPolyphaseDimensions

Back to source controls