WeilExamples.lean

1 import PaperX.WeilSpecialChain
2 import PaperX.WeilSmooth
3 import PaperX.WeilMorphisms
4 import Mathlib.Data.ZMod.Basic
5 import Mathlib.Tactic.NormNum
6 
7 /-! An infinite finite-by-cyclic group with two actual inertia actions.
8 The same F and the same nonzero N can have different local Euler denominators.
9 No identification with an arithmetic local field's Weil group is asserted. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperX.WeilExamples
13 open Polynomial PaperX.WeilData PaperX.WeilEuler PaperX.WeilSpecialChain
14 open PaperX.WeilCopies PaperX.CarrierSummands
15 
16 abbrev C2 := Multiplicative (ZMod 2)
17 abbrev G := C2 × Multiplicative ℤ
18 
19 def inertia : Subgroup G := (MonoidHom.snd C2 (Multiplicative ℤ)).ker
20 instance inertiaNormal : inertia.Normal := inferInstanceAs (MonoidHom.ker _).Normal
21 
22 instance inertiaFinite : Finite inertia := Finite.of_injective (fun h : inertia => h.val.1) (by
23   intro h k he
24   apply Subtype.ext
25   apply Prod.ext he
26   exact h.property.trans k.property.symm)
27 
28 instance groupTopology : TopologicalSpace G := ⊥
29 instance groupDiscrete : DiscreteTopology G := ⟨rfl⟩
30 
31 def powerChar (b : ℚˣ) : Multiplicative ℤ →* ℚˣ where
32   toFun z := b ^ z.toAdd
33   map_one' := by simp
34   map_mul' x y := by
35     change b ^ (x.toAdd + y.toAdd) = _
36     rw [zpow_add]
37 
38 def signChar : C2 →* ℚˣ where
39   toFun g := if g.toAdd = 0 then 1 else -1
40   map_one' := by decide +kernel
41   map_mul' := by decide +kernel
42 
43 def ν : G →* ℚˣ :=
44   (powerChar (Units.mk0 (1/3) (by norm_num))).comp (MonoidHom.snd _ _)
45 
46 def α : G →* ℚˣ :=
47   (powerChar (Units.mk0 2 (by norm_num))).comp (MonoidHom.snd _ _)
48 
49 def β : G →* ℚˣ := (signChar.comp (MonoidHom.fst _ _)) * α
50 
51 def φ : G := (1, Multiplicative.ofAdd 1)
52 def τ : inertia := ⟨(Multiplicative.ofAdd 1, 1), rfl⟩
53 
54 theorem norm_inertia (h : inertia) : ν h = 1 := by
55   have hh : h.val.2 = 1 := h.property
56   simp [ν, hh]
57 
58 theorem unramified_inertia (h : inertia) : α h = 1 := by
59   have hh : h.val.2 = 1 := h.property
60   simp [α, hh]
61 
62 theorem ramified_inertia : β τ ≠ 1 := by
63   change (if (1 : ZMod 2) = 0 then (1 : ℚˣ) else -1) * _ ≠ 1
64   rw [unramified_inertia]
65   norm_num
66 
67 theorem character_at_frobenius : α φ = Units.mk0 2 (by norm_num) ∧ β φ = α φ := by
68   constructor <;> simp [α, β, φ, signChar, powerChar]
69 
70 def unramified : Datum ν (Fin 3 → ℚ) := chainDatum ν α 3
71 def ramified : Datum ν (Fin 3 → ℚ) := chainDatum ν β 3
72 
73 def unramifiedInertial : PaperX.WeilSmooth.InertialDatum (ν := ν) inertia (Fin 3 → ℚ) where
74   toDatum := unramified
75   inertia_finite := Set.finite_range _
76   inertia_open := isOpen_discrete _
77 
78 def ramifiedInertial : PaperX.WeilSmooth.InertialDatum (ν := ν) inertia (Fin 3 → ℚ) where
79   toDatum := ramified
80   inertia_finite := Set.finite_range _
81   inertia_open := isOpen_discrete _
82 
83 theorem same_F_and_N : unramified.r φ = ramified.r φ ∧ unramified.N = ramified.N := by
84   constructor
85   · change (PaperX.SpecialMonodromy.diagonalF (ν φ) (α φ) 3).toLinearMap =
86       (PaperX.SpecialMonodromy.diagonalF (ν φ) (β φ) 3).toLinearMap
87     rw [character_at_frobenius.2]
88   · rfl
89 
90 theorem nonzero_monodromy : unramified.N ^ 2 ≠ 0 ∧ unramified.N ^ 3 = 0 :=
91   ⟨PaperX.SpecialMonodromy.shift_previous_power_nonzero 3 (by decide),
92     PaperX.SpecialMonodromy.shift_nilpotent 3⟩
93 
94 theorem local_dimensions : Module.finrank ℚ (fixedKernel unramified inertia) = 1 ∧
95     Module.finrank ℚ (fixedKernel ramified inertia) = 0 := by
96   constructor
97   · exact unramified_dimension ν α 3 (by decide) inertia norm_inertia unramified_inertia
98   · exact ramified_dimension ν β 3 inertia norm_inertia ⟨τ, ramified_inertia⟩
99 
100 theorem local_polynomials : localCharpoly unramified inertia φ = X - C 2 ∧
101     localCharpoly ramified inertia φ = 1 := by
102   constructor
103   · rw [unramified, unramified_charpoly ν α 3 (by decide) inertia norm_inertia
104       unramified_inertia φ, character_at_frobenius.1]
105     rfl
106   · exact ramified_charpoly ν β 3 inertia norm_inertia ⟨τ, ramified_inertia⟩ φ
107 
108 theorem euler_polynomials : eulerPolynomial unramified inertia φ = 1 - C 2 * X ∧
109     eulerPolynomial ramified inertia φ = 1 := by
110   constructor
111   · rw [unramified, unramified_euler ν α 3 (by decide) inertia norm_inertia
112       unramified_inertia φ, character_at_frobenius.1]
113     rfl
114   · exact ramified_euler ν β 3 inertia norm_inertia ⟨τ, ramified_inertia⟩ φ
115 
116 theorem same_F_N_different_euler : unramified.r φ = ramified.r φ ∧
117     unramified.N = ramified.N ∧
118     eulerPolynomial unramified inertia φ ≠ eulerPolynomial ramified inertia φ := by
119   refine ⟨same_F_and_N.1, same_F_and_N.2, ?_⟩
120   rw [euler_polynomials.1, euler_polynomials.2]
121   intro he
122   have hc := congrArg (fun p : Polynomial ℚ => p.coeff 1) he
123   norm_num at hc
124 
125 def family (i : Fin 2) : Datum ν (Fin 3 → ℚ) := if i = 0 then unramified else ramified
126 def multiplicities (i : Fin 2) : ℕ := if i = 0 then 2 else 1
127 
128 theorem mixed_dimension :
129     Module.finrank ℚ (fixedKernel (copiesDatum family multiplicities) inertia) = 2 := by
130   rw [fixed_dimension_sum, Fin.sum_univ_two]
131   change 2 * Module.finrank ℚ (fixedKernel unramified inertia) +
132     1 * Module.finrank ℚ (fixedKernel ramified inertia) = 2
133   rw [local_dimensions.1, local_dimensions.2]
134 
135 theorem mixed_euler : eulerPolynomial (copiesDatum family multiplicities) inertia φ =
136     (1 - C 2 * X)^2 := by
137   rw [euler_product]
138   simp [Fin.prod_univ_two, family, multiplicities, euler_polynomials.1, euler_polynomials.2]
139 
140 
141 theorem geometric_norm : (ν φ : ℚ) = 1/3 := by simp [ν, φ, powerChar]
142 
143 /-- Equal Euler factors do not recover chain length or the monodromy operator. -/
144 theorem same_euler_different_monodromy :
145     eulerPolynomial (chainDatum ν α 1) inertia φ = eulerPolynomial unramified inertia φ ∧
146     (chainDatum ν α 1).N = 0 ∧ unramified.N ^ 2 ≠ 0 := by
147   refine ⟨?_, ?_, nonzero_monodromy.1⟩
148   · rw [unramified, unramified_euler ν α 1 (by decide) inertia norm_inertia
149       unramified_inertia φ, unramified_euler ν α 3 (by decide) inertia norm_inertia
150       unramified_inertia φ]
151   · exact PaperX.SpecialMonodromy.shift_nilpotent 1
152 
153 end PaperX.WeilExamples

Back to source controls