ResidueDegreeBaseChange.lean

1 import PaperXI.ResidueWeil
2 import Mathlib.Data.ZMod.Basic
3 
4 /-! Integer-degree base change for residue-action pullbacks.
5 The map (g,m) ↦ (g,n*m) is constructed; neither subgroup equality nor index is
6 assumed. This does not identify a pullback with an absolute local Weil group. -/
7 set_option autoImplicit false
8 noncomputable section
9 open scoped Classical
10 namespace PaperXI.ResidueDegreeBaseChange
11 open PaperXI.ResidueWeil
12 variable {D C : Type*} [Group D] [Group C]
13 
14 /-- Residue degree modulo n, with the additive quotient written multiplicatively. -/
15 def degreeMod (r : D →* C) (F : C) (n : ℕ) :
16     Pullback r F →* Multiplicative (ZMod n) where
17   toFun w := Multiplicative.ofAdd ((Multiplicative.toAdd (degree r F w) : ℤ) : ZMod n)
18   map_one' := by simp
19   map_mul' a b := by
20     change Multiplicative.ofAdd (((Multiplicative.toAdd a.val.2 + Multiplicative.toAdd b.val.2 : ℤ)) : ZMod n) = _
21     simp
22 
23 /-- The actual degree-divisible subgroup. -/
24 def periodSubgroup (r : D →* C) (F : C) (n : ℕ) : Subgroup (Pullback r F) :=
25   (degreeMod r F n).ker
26 
27 instance period_normal (r : D →* C) (F : C) (n : ℕ) : (periodSubgroup r F n).Normal :=
28   inferInstanceAs ((degreeMod r F n).ker.Normal)
29 
30 @[simp] theorem mem_periodSubgroup (r : D →* C) (F : C) (n : ℕ) (w : Pullback r F) :
31     w ∈ periodSubgroup r F n ↔ (n : ℤ) ∣ Multiplicative.toAdd (degree r F w) := by
32   change (((Multiplicative.toAdd (degree r F w) : ℤ) : ZMod n) = 0) ↔ _
33   exact ZMod.intCast_zmod_eq_zero_iff_dvd _ _
34 
35 /-- Change residue Frobenius from F to F^n without reducing the integer degree. -/
36 def inclusion (r : D →* C) (F : C) (n : ℕ) :
37     Pullback r (F^n) →* Pullback r F where
38   toFun w := ⟨(w.val.1, Multiplicative.ofAdd ((n : ℤ) * Multiplicative.toAdd w.val.2)), by
39     change r w.val.1 = F ^ ((n : ℤ) * Multiplicative.toAdd w.val.2)
40     rw [zpow_mul, zpow_natCast]
41     exact w.property⟩
42   map_one' := by apply Subtype.ext; simp
43   map_mul' a b := by
44     apply Subtype.ext
45     apply Prod.ext
46     · rfl
47     · change Multiplicative.ofAdd ((n : ℤ) * (Multiplicative.toAdd a.val.2 + Multiplicative.toAdd b.val.2)) = _
48       simp [mul_add]
49 
50 @[simp] theorem inclusion_projection (r : D →* C) (F : C) (n : ℕ)
51     (w : Pullback r (F^n)) : projection r F (inclusion r F n w) = projection r (F^n) w := rfl
52 
53 @[simp] theorem inclusion_degree (r : D →* C) (F : C) (n : ℕ)
54     (w : Pullback r (F^n)) : Multiplicative.toAdd (degree r F (inclusion r F n w)) =
55       (n : ℤ) * Multiplicative.toAdd (degree r (F^n) w) := rfl
56 
57 theorem inclusion_injective (r : D →* C) (F : C) {n : ℕ} (hn : n ≠ 0) :
58     Function.Injective (inclusion r F n) := by
59   intro a b hab
60   have h1 := congrArg (fun x : Pullback r F => x.val.1) hab
61   have h2 := congrArg (fun x : Pullback r F => Multiplicative.toAdd x.val.2) hab
62   have hnz : (n : ℤ) ≠ 0 := by exact_mod_cast hn
63   apply Subtype.ext
64   apply Prod.ext
65   · exact h1
66   · exact Multiplicative.toAdd.injective (mul_left_cancel₀ hnz h2)
67 
68 /-- Surjectivity onto the degree subgroup needs no residue-surjectivity assumption. -/
69 theorem inclusion_range (r : D →* C) (F : C) (n : ℕ) :
70     (inclusion r F n).range = periodSubgroup r F n := by
71   ext w
72   constructor
73   · rintro ⟨v, rfl⟩
74     rw [mem_periodSubgroup, inclusion_degree]
75     exact dvd_mul_right _ _
76   · intro hw
77     obtain ⟨m, hm⟩ := (mem_periodSubgroup r F n w).mp hw
78     let v : Pullback r (F^n) := ⟨(w.val.1, Multiplicative.ofAdd m), by
79       change r w.val.1 = (F^n)^m
80       rw [← zpow_natCast F n, ← zpow_mul, ← hm]
81       exact w.property⟩
82     refine ⟨v, ?_⟩
83     apply Subtype.ext
84     apply Prod.ext
85     · rfl
86     · exact Multiplicative.toAdd.injective hm.symm
87 
88 /-- An actual multiplicative equivalence onto the period subgroup. -/
89 def periodEquiv (r : D →* C) (F : C) {n : ℕ} (hn : n ≠ 0) :
90     Pullback r (F^n) ≃* periodSubgroup r F n :=
91   (MonoidHom.ofInjective (inclusion_injective r F hn)).trans
92     (MulEquiv.subgroupCongr (inclusion_range r F n))
93 
94 /-- A degree-one lift provides all integer degrees, not just residue powers. -/
95 theorem degree_surjective (r : D →* C) (F : C) (hF : F ∈ r.range) :
96     Function.Surjective (degree r F) := by
97   obtain ⟨w, hw⟩ := (exists_degree_one_iff r F).mpr hF
98   intro m
99   refine ⟨w ^ Multiplicative.toAdd m, ?_⟩
100   rw [map_zpow, hw]
101   apply Multiplicative.toAdd.injective
102   simp
103 
104 /-- Reduction modulo n is onto once a degree-one lift exists. -/
105 theorem degreeMod_surjective (r : D →* C) (F : C) (n : ℕ) (hF : F ∈ r.range) :
106     Function.Surjective (degreeMod r F n) := by
107   intro z
108   obtain ⟨m, hm⟩ := ZMod.intCast_surjective (Multiplicative.toAdd z)
109   obtain ⟨w, hw⟩ := degree_surjective r F hF (Multiplicative.ofAdd m)
110   refine ⟨w, ?_⟩
111   change Multiplicative.ofAdd (((Multiplicative.toAdd (degree r F w) : ℤ)) : ZMod n) = z
112   rw [hw]
113   exact Multiplicative.toAdd.injective hm
114 
115 /-- The quotient is the actual cyclic degree quotient. -/
116 def quotientEquiv (r : D →* C) (F : C) (n : ℕ) (hF : F ∈ r.range) :
117     Pullback r F ⧸ periodSubgroup r F n ≃* Multiplicative (ZMod n) :=
118   QuotientGroup.quotientKerEquivOfSurjective (degreeMod r F n)
119     (degreeMod_surjective r F n hF)
120 
121 theorem quotient_card (r : D →* C) (F : C) (n : ℕ) [NeZero n] (hF : F ∈ r.range) :
122     Nat.card (Pullback r F ⧸ periodSubgroup r F n) = n := by
123   rw [Nat.card_congr (quotientEquiv r F n hF).toEquiv]
124   simp
125 
126 /-- Inertia is unaffected by nonzero degree dilation. -/
127 theorem inertia_preimage (r : D →* C) (F : C) {n : ℕ} (hn : n ≠ 0) :
128     ((degree r F).ker).comap (inclusion r F n) = (degree r (F^n)).ker := by
129   ext w
130   change (Multiplicative.ofAdd ((n : ℤ) * Multiplicative.toAdd w.val.2) = 1) ↔ w.val.2 = 1
131   have hnz : (n : ℤ) ≠ 0 := by exact_mod_cast hn
132   constructor
133   · intro hw
134     apply Multiplicative.toAdd.injective
135     have hz := congrArg Multiplicative.toAdd hw
136     exact (mul_eq_zero.mp hz).resolve_left hnz
137   · intro hw
138     simp [hw]
139 
140 /-- The integer degree map composes multiplicatively along an unramified tower. -/
141 theorem tower_degree (r : D →* C) (F : C) (m n : ℕ)
142     (w : Pullback r ((F^m)^n)) :
143     Multiplicative.toAdd (degree r F
144       (inclusion r F m (inclusion r (F^m) n w))) =
145       ((m*n : ℕ) : ℤ) * Multiplicative.toAdd (degree r ((F^m)^n) w) := by
146   simp only [inclusion_degree, Nat.cast_mul, mul_assoc]
147 
148 end PaperXI.ResidueDegreeBaseChange

Back to source controls