ValuationConductor.lean

1 import PaperXI.ResidueWeil
2 import PaperXI.RamificationSeparation
3 import Mathlib.Topology.Algebra.InfiniteSum.NatInt
4 import Mathlib.Basic.Real.Basic
5 
6 /-! Conductor sums from actual maximal-ideal congruence groups. For a finite
7 Galois extension with discrete valuation these are the lower-numbering expressions.
8 No change-of-extension theorem, absolute Weil comparison, or Hasse--Arf integrality
9 is inferred from this definition. Finite support is proved under the stated
10 Noetherian/finite faithful action conditions. -/
11 set_option autoImplicit false
12 noncomputable section
13 open scoped Classical BigOperators
14 namespace PaperXI.ValuationConductor
15 open PaperXI.ValuationRamification PaperXI.ResidueWeil
16 
17 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [MulSemiringAction D R]
18 
19 abbrev residue : D →* RingAut (IsLocalRing.ResidueField R) :=
20   MulSemiringAction.toRingAut D (IsLocalRing.ResidueField R)
21 
22 /-- The lower group embeds into the degree-zero part of the actual residue pullback. -/
23 def lift (F : RingAut (IsLocalRing.ResidueField R)) (i : ℕ) :
24     lower R D i →* Pullback (residue R D) F where
25   toFun g := ⟨(g.val, 1), by
26     change residue R D g.val = F ^ (0 : ℤ)
27     rw [zpow_zero]
28     exact lower_le_inertia R D i g.property⟩
29   map_one' := rfl
30   map_mul' _ _ := rfl
31 
32 @[simp] theorem lift_degree (F : RingAut (IsLocalRing.ResidueField R))
33     (i : ℕ) (g : lower R D i) : degree (residue R D) F (lift R D F i g) = 1 := rfl
34 
35 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
36 
37 /-- These are fixed spaces for actual congruence-group operators. -/
38 def fixed (F : RingAut (IsLocalRing.ResidueField R))
39     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ) : Submodule ℂ V :=
40   Representation.invariants (ρ.comp (lift R D F i))
41 
42 /-- Zeroth lower fixed space is exactly the degree-kernel fixed space. -/
43 theorem fixed_zero (F : RingAut (IsLocalRing.ResidueField R))
44     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
45     fixed R D F ρ 0 = Representation.invariants (ρ.comp (degree (residue R D) F).ker.subtype) := by
46   ext v
47   constructor
48   · intro hv w
49     have hg : w.val.val.1 ∈ lower R D 0 := by
50       rw [lower_zero_eq_residue_kernel]
51       exact (inertiaEquiv (residue R D) F w).property
52     have hh := hv ⟨w.val.val.1, hg⟩
53     have he : lift R D F 0 ⟨w.val.val.1, hg⟩ = w.val := by
54       apply Subtype.ext
55       exact Prod.ext rfl w.property.symm
56     change ρ w.val v = v
57     simpa only [MonoidHom.comp_apply, he] using hh
58   · intro hv g
59     exact hv ⟨lift R D F 0 g, rfl⟩
60 
61 def codimension (F : RingAut (IsLocalRing.ResidueField R))
62     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ) : ℕ :=
63   Module.finrank ℂ V - Module.finrank ℂ (fixed R D F ρ i)
64 
65 /-- The conventional lower-numbering weight is derived from actual subgroup orders. -/
66 def summand (F : RingAut (IsLocalRing.ResidueField R))
67     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ) : ℝ :=
68   (Nat.card (lower R D i) : ℝ) / (Nat.card (lower R D 0) : ℝ) * codimension R D F ρ i
69 
70 def swan (F : RingAut (IsLocalRing.ResidueField R))
71     (ρ : Representation ℂ (Pullback (residue R D) F) V) : ℝ :=
72   ∑' i : ℕ, summand R D F ρ (i+1)
73 
74 def artin (F : RingAut (IsLocalRing.ResidueField R))
75     (ρ : Representation ℂ (Pullback (residue R D) F) V) : ℝ :=
76   (codimension R D F ρ 0 : ℝ) + swan R D F ρ
77 
78 /-- First-group triviality forces every positive-depth term to vanish. -/
79 theorem positive_fixed_top (F : RingAut (IsLocalRing.ResidueField R))
80     (ρ : Representation ℂ (Pullback (residue R D) F) V)
81     (ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1) (i : ℕ) :
82     fixed R D F ρ (i+1) = ⊤ := by
83   apply top_unique
84   intro v _ g
85   have hg : g.val ∈ lower R D 1 := positive_le_one R D (Nat.le_add_left 1 i) g.property
86   exact LinearMap.congr_fun (ht ⟨g.val, hg⟩) v
87 
88 theorem tame_summand_zero (F : RingAut (IsLocalRing.ResidueField R))
89     (ρ : Representation ℂ (Pullback (residue R D) F) V)
90     (ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1) (i : ℕ) :
91     summand R D F ρ (i+1) = 0 := by
92   unfold summand codimension
93   rw [positive_fixed_top R D F ρ ht i]
94   simp
95 
96 theorem tame_swan_zero (F : RingAut (IsLocalRing.ResidueField R))
97     (ρ : Representation ℂ (Pullback (residue R D) F) V)
98     (ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1) : swan R D F ρ = 0 := by
99   simp only [swan, tame_summand_zero R D F ρ ht, tsum_zero]
100 
101 /-- The original irreducible dimension argument no longer needs tame orbit induction. -/
102 theorem tame_irreducible_dimension [FiniteDimensional ℂ V] (F : RingAut (IsLocalRing.ResidueField R))
103     (ρ : Representation ℂ (Pullback (residue R D) F) V) [Representation.IsIrreducible ρ]
104     (ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1)
105     (hdim : 1 < Module.finrank ℂ V) :
106     fixed R D F ρ 0 = ⊥ ∧ swan R D F ρ = 0 ∧ artin R D F ρ = (Module.finrank ℂ V : ℝ) := by
107   have hf : fixed R D F ρ 0 = ⊥ := by
108     rw [fixed_zero]
109     exact NormalInertia.fixed_eq_bot_of_dimension_gt_one ρ (degree (residue R D) F).ker hdim
110   refine ⟨hf, tame_swan_zero R D F ρ ht, ?_⟩
111   unfold artin codimension
112   rw [hf, tame_swan_zero R D F ρ ht]
113   simp
114 
115 /-- Unramified one-dimensional representations retain conductor zero. -/
116 theorem tame_artin_dichotomy [FiniteDimensional ℂ V] (F : RingAut (IsLocalRing.ResidueField R))
117     (ρ : Representation ℂ (Pullback (residue R D) F) V) [Representation.IsIrreducible ρ]
118     (ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1) :
119     artin R D F ρ = if (degree (residue R D) F).ker ≤ ρ.ker then 0 else
120       (Module.finrank ℂ V : ℝ) := by
121   rw [artin, tame_swan_zero R D F ρ ht, add_zero]
122   unfold codimension
123   rw [fixed_zero, NormalInertia.fixed_codimension]
124   split_ifs <;> simp
125 
126 /-- A trivial congruence subgroup has the full fixed space. -/
127 theorem fixed_top_of_lower_bot (F : RingAut (IsLocalRing.ResidueField R))
128     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ)
129     (hi : lower R D i = ⊥) : fixed R D F ρ i = ⊤ := by
130   apply top_unique
131   intro v _ g
132   have hg : g.val = 1 := by simpa only [hi, Subgroup.mem_bot] using g.property
133   have he : lift R D F i g = 1 := by apply Subtype.ext; exact Prod.ext hg rfl
134   change ρ (lift R D F i g) v = v
135   simp [he]
136 
137 /-- Finite support follows from Krull separation and finite faithful ring action. -/
138 theorem summable_summands [IsNoetherianRing R] [Finite D] [FaithfulSMul D R]
139     (F : RingAut (IsLocalRing.ResidueField R))
140     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
141     Summable (summand R D F ρ) := by
142   obtain ⟨N, hN⟩ := RamificationSeparation.eventually_trivial R D
143   apply summable_of_ne_finset_zero (s := Finset.range N)
144   intro i hi
145   have hh : N ≤ i := by simpa only [Finset.mem_range, not_lt] using hi
146   unfold summand codimension
147   rw [fixed_top_of_lower_bot R D F ρ i (hN i hh)]
148   simp
149 
150 /-- The inertia denominator is nonzero, so the zeroth conventional weight is one. -/
151 theorem zeroth_summand [Finite D] (F : RingAut (IsLocalRing.ResidueField R))
152     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
153     summand R D F ρ 0 = (codimension R D F ρ 0 : ℝ) := by
154   unfold summand
155   have hc : (Nat.card (lower R D 0) : ℝ) ≠ 0 := by
156     exact_mod_cast (Nat.card_pos : 0 < Nat.card (lower R D 0)).ne'
157   rw [div_self hc, one_mul]
158 
159 /-- The split Artin definition equals the full convergent lower-numbering sum. -/
160 theorem artin_eq_full_sum [IsNoetherianRing R] [Finite D] [FaithfulSMul D R]
161     (F : RingAut (IsLocalRing.ResidueField R))
162     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
163     artin R D F ρ = ∑' i : ℕ, summand R D F ρ i := by
164   have h := (summable_summands R D F ρ).sum_add_tsum_nat_add 1
165   simpa only [Finset.sum_range_one, zeroth_summand, artin, swan] using h
166 
167 end PaperXI.ValuationConductor

Back to source controls