InducedTameProfile.lean

1 import PaperXI.InducedCycleInvariants
2 import PaperXI.TameConductor
3 import PaperXI.InvariantPolynomial
4 
5 /-! All inertia and determinant data are read from the actual induced space.
6 The finite ramification expression is kept distinct from an arithmetically
7 identified Artin conductor. No irreducibility or regularity is needed here. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.InducedTameProfile
11 open scoped Classical BigOperators
12 open Polynomial PaperXI.CyclicInduced PaperXI.CyclicAction PaperXI.PacketTransport
13 open PaperXI.TameOrbitTransitivity PaperXI.GeneratedIrreducibility
14 variable {G : Type*} [Group G] {M : ℕ} [NeZero M]
15 variable (δ : G →* Multiplicative ℤ) (ι : Multiplicative (ZMod M) →* G)
16 
17 /-- Finite inertia has degree zero in an integer degree group. -/
18 theorem inertia_degree (a : Multiplicative (ZMod M)) : δ (ι a) = 1 := by
19   have hp : (ι a) ^ M = 1 := by
20     rw [← map_pow]
21     have ha : a ^ M = 1 := by
22       apply Multiplicative.toAdd.injective
23       simp [toAdd_pow, nsmul_eq_mul]
24     rw [ha, map_one]
25   have hd := congrArg (fun g => (δ g).toAdd) hp
26   have hm : (M : ℤ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne M)
27   have hz : (M : ℤ) * (δ (ι a)).toAdd = 0 := by
28     simpa [map_pow, toAdd_pow, nsmul_eq_mul] using hd
29   apply Multiplicative.toAdd.injective
30   exact (mul_eq_zero.mp hz).resolve_left hm
31 
32 /-- The actual inclusion of finite inertia into every degree-divisibility subgroup. -/
33 def inertiaInDegree (n : ℕ) : Multiplicative (ZMod M) →* TameDegree.degreeSubgroup δ n where
34   toFun a := ⟨ι a, by
35     change TameDegree.degreeMod δ n (ι a) = 1
36     simp [TameDegree.degreeMod, TameDegree.degree, inertia_degree δ ι a]⟩
37   map_one' := by apply Subtype.ext; simp
38   map_mul' a b := by apply Subtype.ext; simp
39 
40 variable (φ : G) (hφ : δ φ = Multiplicative.ofAdd (1 : ℤ))
41 variable (n : ℕ) [NeZero n] (ξ : TameDegree.degreeSubgroup δ n →* ℂˣ)
42 variable (q : (ZMod M)ˣ) (j : ZMod M)
43 variable (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
44   ι (Multiplicative.ofAdd (q : ZMod M)))
45 variable (hξ : ∀ a : ZMod M,
46   (ξ (inertiaInDegree δ ι n (Multiplicative.ofAdd a)) : ℂ) = ZMod.stdAddChar (j * a))
47 
48 include hξ in
49 /-- The zeroth basis line carries the declared inertia character, derived from
50 its actual inducing-character restriction. -/
51 theorem origin_mem : degreeBasis δ φ hφ n ξ 0 ∈
52     packet (tameRestriction (degreeInduced δ n ξ) ι) j := by
53   intro a
54   have h := degreeBasis_action_zero δ φ hφ n ξ
55     (inertiaInDegree δ ι n (Multiplicative.ofAdd a))
56   change degreeInduced δ n ξ (ι (Multiplicative.ofAdd a))
57     (degreeBasis δ φ hφ n ξ 0) = _ at h
58   rw [hξ] at h
59   exact h
60 
61 include hφ hrel hξ in
62 /-- Each basis line lies in the computed Frobenius-rotated inertia packet. -/
63 theorem basis_packet (i : Fin n) :
64     InducedCycleInvariants.basis δ φ hφ n ξ i ∈
65       packet (tameRestriction (degreeInduced δ n ξ) ι)
66         (((q ^ (i : ℕ) : (ZMod M)ˣ) : ZMod M) * j) := by
67   have hn := Nat.pos_of_ne_zero (NeZero.ne n)
68   rw [InducedCycleInvariants.basis_powers δ φ hφ n ξ hn i]
69   have h := PacketReturn.power_mem (tameRestriction (degreeInduced δ n ξ) ι)
70     (actionEquiv (degreeInduced δ n ξ) φ) q
71     (geometric_relation (degreeInduced δ n ξ) ι φ q hrel) j (i : ℕ)
72     (origin_mem δ ι φ hφ n ξ j hξ)
73   simpa only [← PacketCycle.linear_power, InducedCycleInvariants.basis_apply,
74     Fin.val_zero, Nat.cast_zero, actionEquiv] using h
75 
76 /-- A general eigenbasis support theorem; repeated labels are allowed. -/
77 theorem support_of_basis {V : Type*} [AddCommGroup V] [Module ℂ V]
78     (ρ : Action (K := ℂ) (V := V) (M := M)) {A : Type*}
79     (b : Module.Basis A ℂ V) (labels : A → ZMod M)
80     (hb : ∀ a, b a ∈ packet ρ (labels a)) (k : ZMod M) :
81     packet ρ k ≠ ⊥ ↔ ∃ a, labels a = k := by
82   constructor
83   · intro hk
84     by_contra hnone
85     have hne : ∀ a, labels a ≠ k := by simpa using hnone
86     have hp : projector ρ k = 0 := by
87       apply b.ext
88       intro a
89       exact projector_on_other_packet ρ (Ne.symm (hne a)) (hb a)
90     apply hk
91     apply le_antisymm
92     · intro v hv
93       have he := (mem_iff_projector ρ k v).mp hv
94       rw [hp] at he
95       exact he.symm
96     · exact bot_le
97   · rintro ⟨a, rfl⟩ he
98     have hv := hb a
99     rw [he] at hv
100     exact b.ne_zero a hv
101 
102 include hφ hrel hξ in
103 /-- The support is the actual set of labels on the induced Frobenius cycle. -/
104 theorem inertia_support (k : ZMod M) :
105     packet (tameRestriction (degreeInduced δ n ξ) ι) k ≠ ⊥ ↔
106       ∃ i : Fin n, ((q ^ (i : ℕ) : (ZMod M)ˣ) : ZMod M) * j = k :=
107   support_of_basis _ (InducedCycleInvariants.basis δ φ hφ n ξ) _
108     (basis_packet δ ι φ hφ n ξ q j hrel hξ) k
109 
110 include hφ hrel hξ in
111 /-- All or none of this induced cycle survives inertia invariants. -/
112 theorem inertia_invariants :
113     (tameRestriction (degreeInduced δ n ξ) ι).invariants = if j = 0 then ⊤ else ⊥ := by
114   classical
115   by_cases hj : j = 0
116   · rw [ite_eq_left hj]
117     apply InertiaFixed.invariants_eq_top_of_basis _ (InducedCycleInvariants.basis δ φ hφ n ξ)
118     intro i
119     simpa [hj] using basis_packet δ ι φ hφ n ξ q j hrel hξ i
120   · rw [ite_eq_right hj]
121     apply InertiaFixed.invariants_eq_bot_of_basis _ (InducedCycleInvariants.basis δ φ hφ n ξ)
122       (fun i => ((q ^ (i : ℕ) : (ZMod M)ˣ) : ZMod M) * j)
123     · intro i hz
124       exact hj ((InertiaFixed.orbit_label_eq_zero_iff q j (i : ℕ)).mp hz)
125     · exact basis_packet δ ι φ hφ n ξ q j hrel hξ
126 
127 include hφ hrel hξ in
128 theorem invariant_dimension :
129     Module.finrank ℂ (tameRestriction (degreeInduced δ n ξ) ι).invariants =
130       if j = 0 then n else 0 := by
131   by_cases hj : j = 0
132   · rw [ite_eq_left hj]
133     have ht : (tameRestriction (degreeInduced δ n ξ) ι).invariants = ⊤ := by
134       simpa only [ite_eq_left hj] using inertia_invariants δ ι φ hφ n ξ q j hrel hξ
135     exact (LinearEquiv.ofTop _ ht).finrank_eq.trans
136       (InducedCycleInvariants.dimension δ φ hφ n ξ)
137   · rw [ite_eq_right hj]
138     have hb : (tameRestriction (degreeInduced δ n ξ) ι).invariants = ⊥ := by
139       simpa only [ite_eq_right hj] using inertia_invariants δ ι φ hφ n ξ q j hrel hξ
140     have : Subsingleton (tameRestriction (degreeInduced δ n ξ) ι).invariants :=
141       Submodule.subsingleton_iff_eq_bot.mpr hb
142     exact Module.finrank_zero_of_subsingleton
143 
144 variable [FiniteDimensional ℂ (DegreeIndSpace δ n ξ)]
145 
146 include hφ hrel hξ in
147 /-- The local polynomial is defined by restricting the actual Frobenius map,
148 not by a case split. The case formula is derived afterward. -/
149 theorem local_polynomial :
150     InvariantPolynomial.localPolynomial (tameRestriction (degreeInduced δ n ξ) ι)
151       (actionEquiv (degreeInduced δ n ξ) φ) q
152       (geometric_relation (degreeInduced δ n ξ) ι φ q hrel) =
153       if j = 0 then 1 - C (InducedCycleInvariants.returnScalar δ φ hφ n ξ : ℂ) * X ^ n
154       else 1 := by
155   by_cases hj : j = 0
156   · rw [ite_eq_left hj]
157     have ht : (tameRestriction (degreeInduced δ n ξ) ι).invariants = ⊤ := by
158       simpa [hj] using inertia_invariants δ ι φ hφ n ξ q j hrel hξ
159     rw [InvariantPolynomial.localPolynomial_of_top _ _ _ _ ht]
160     change ((degreeInduced δ n ξ φ).charpoly).reverse = _
161     rw [(InducedCycleInvariants.cycle_invariants δ φ hφ n ξ).1,
162       CyclicPolynomial.reverse_cycle_polynomial]
163   · rw [ite_eq_right hj]
164     have hb : (tameRestriction (degreeInduced δ n ξ) ι).invariants = ⊥ := by
165       simpa [hj] using inertia_invariants δ ι φ hφ n ξ q j hrel hξ
166     exact InvariantPolynomial.localPolynomial_of_bot _ _ _ _ hb
167 
168 include hφ hrel hξ in
169 omit [FiniteDimensional ℂ (DegreeIndSpace δ n ξ)] in
170 /-- Uniform finite tame conductor rule, including one-dimensional ramified
171 characters and reducible zero-label cycles. Standard conductor identification
172 is a separate arithmetic interface. -/
173 theorem finite_conductors (P : Subgroup G)
174     (hP : ∀ g ∈ P, ∀ v, degreeInduced δ n ξ g v = v)
175     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
176     (hJP : ∀ r ∈ S, J r ≤ P) :
177     TameConductor.finiteSwan (degreeInduced δ n ξ) S J w = 0 ∧
178     TameConductor.finiteArtin (degreeInduced δ n ξ) ι S J w =
179       if j = 0 then 0 else (n : ℚ) := by
180   have hs := TameConductor.finiteSwan_zero (degreeInduced δ n ξ) P hP S J w hJP
181   refine ⟨hs, ?_⟩
182   unfold TameConductor.finiteArtin
183   rw [hs, InducedCycleInvariants.dimension δ φ hφ n ξ,
184     invariant_dimension δ ι φ hφ n ξ q j hrel hξ]
185   split_ifs <;> simp
186 
187 end PaperXI.InducedTameProfile

Back to source controls