TameConductor.lean

1 import PaperXI.PacketBasis
2 import PaperXI.InertiaFixed
3 import PaperXI.InertiaQuotient
4 import Mathlib.Data.Rat.Cast.Order
5 
6 /-! The nontrivial tame conductor calculation, with its finite-quotient
7 attachment explicit. These definitions encode finite ramification sums. They
8 do not construct local fields, Weil groups or ramification filtrations. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.TameConductor
12 open scoped BigOperators Classical
13 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
14 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
15 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
16 variable [FiniteDimensional ℂ V]
17 variable {M : ℕ} [NeZero M]
18 
19 omit [FiniteDimensional ℂ V] [NeZero M] in
20 /-- The trivial inertia label has exact period one. -/
21 theorem zero_label_period (q : (ZMod M)ˣ) : period q 0 = 1 :=
22   Nat.dvd_one.mp ((stabilizing_power_iff q 0 1).mp (by simp))
23 
24 /-- Nonzero inertia invariants would force the whole irreducible space to
25 have dimension one. No invariant-space or orbit-basis conclusion is assumed. -/
26 theorem inertia_invariants_eq_bot
27     (π : Representation ℂ G V) [Representation.IsIrreducible π]
28     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
29     (hgen : Submonoid.closure (generators ι φ) = ⊤)
30     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
31       ι (Multiplicative.ofAdd (q : ZMod M)))
32     (hdim : 1 < Module.finrank ℂ V) : (Representation.invariants (π.comp ι)) = ⊥ := by
33   by_contra h
34   have hj : packet (tameRestriction π ι) 0 ≠ ⊥ := by
35     simpa only [PaperXI.InertiaFixed.invariants_eq_packet_zero] using h
36   have hn := PaperXI.PacketBasis.finrank_eq_period π ι φ q hgen hrel hj
37   rw [zero_label_period] at hn
38   omega
39 
40 theorem inertia_finrank_zero
41     (π : Representation ℂ G V) [Representation.IsIrreducible π]
42     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
43     (hgen : Submonoid.closure (generators ι φ) = ⊤)
44     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
45       ι (Multiplicative.ofAdd (q : ZMod M)))
46     (hdim : 1 < Module.finrank ℂ V) : Module.finrank ℂ (Representation.invariants (π.comp ι)) = 0 := by
47   rw [inertia_invariants_eq_bot π ι φ q hgen hrel hdim]
48   simp
49 
50 /-- Codimension of the genuine J-fixed subspace. -/
51 def fixedCodimension (π : Representation ℂ G V) (J : Subgroup G) : ℕ :=
52   Module.finrank ℂ V - Module.finrank ℂ (Representation.invariants (π.comp J.subtype))
53 
54 /-- A finite positive-depth ramification sum; the filtration and conventional
55 weights must be supplied and identified by the local-field attachment. -/
56 def finiteSwan (π : Representation ℂ G V) (S : Finset ℕ)
57     (J : ℕ → Subgroup G) (w : ℕ → ℚ) : ℚ :=
58   ∑ r ∈ S, w r * (fixedCodimension π (J r) : ℚ)
59 
60 omit [NeZero M] [FiniteDimensional ℂ V] in
61 theorem invariants_eq_top_of_trivial_on (π : Representation ℂ G V) (J : Subgroup G)
62     (hJ : ∀ g ∈ J, ∀ v, π g v = v) : (Representation.invariants (π.comp J.subtype)) = ⊤ := by
63   apply top_unique
64   intro v _ g
65   exact hJ g g.property v
66 
67 omit [NeZero M] [FiniteDimensional ℂ V] in
68 theorem fixedCodimension_zero_of_trivial_on (π : Representation ℂ G V) (J : Subgroup G)
69     (hJ : ∀ g ∈ J, ∀ v, π g v = v) : fixedCodimension π J = 0 := by
70   unfold fixedCodimension
71   rw [invariants_eq_top_of_trivial_on π J hJ]
72   simp
73 
74 omit [NeZero M] [FiniteDimensional ℂ V] in
75 /-- Wild triviality is an action hypothesis, not an assumed Swan value. -/
76 theorem finiteSwan_zero (π : Representation ℂ G V) (P : Subgroup G)
77     (hP : ∀ g ∈ P, ∀ v, π g v = v)
78     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
79     (hJP : ∀ r ∈ S, J r ≤ P) : finiteSwan π S J w = 0 := by
80   unfold finiteSwan
81   apply Finset.sum_eq_zero
82   intro r hr
83   rw [fixedCodimension_zero_of_trivial_on π (J r)
84     (fun g hg v => hP g (hJP r hr hg) v)]
85   simp
86 
87 /-- Finite Artin expression with the actual inertia fixed-space term. -/
88 def finiteArtin (π : Representation ℂ G V)
89     (ι : Multiplicative (ZMod M) →* G)
90     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ) : ℚ :=
91   (Module.finrank ℂ V : ℚ) - (Module.finrank ℂ (Representation.invariants (π.comp ι)) : ℚ) +
92     finiteSwan π S J w
93 
94 /-- Source-facing conductor endpoint in the declared finite-inertia model. -/
95 theorem conductor_of_nontrivial_tame_atom
96     (π : Representation ℂ G V) [Representation.IsIrreducible π]
97     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
98     (hgen : Submonoid.closure (generators ι φ) = ⊤)
99     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
100       ι (Multiplicative.ofAdd (q : ZMod M)))
101     (hdim : 1 < Module.finrank ℂ V)
102     (P : Subgroup G) (hP : ∀ g ∈ P, ∀ v, π g v = v)
103     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
104     (hJP : ∀ r ∈ S, J r ≤ P) :
105     finiteSwan π S J w = 0 ∧
106     Module.finrank ℂ (Representation.invariants (π.comp ι)) = 0 ∧
107     finiteArtin π ι S J w = (Module.finrank ℂ V : ℚ) := by
108   have hs := finiteSwan_zero π P hP S J w hJP
109   have hi := inertia_finrank_zero π ι φ q hgen hrel hdim
110   refine ⟨hs, hi, ?_⟩
111   simp [finiteArtin, hs, hi]
112 
113 end PaperXI.TameConductor

Back to source controls