FiniteResidueSubgroup.lean

1 import PaperXI.FiniteResidueBaseChange
2 
3 /-! A residue-field fixing subgroup, not an abstract subgroup assigned index f.
4 Its pullback for geometric |k'|-Frobenius is identified with the degree-f subgroup
5 of the |k|-Frobenius pullback. No local-field lifting theorem is asserted. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FiniteResidueSubgroup
9 open PaperXI.ResidueWeil PaperXI.ResidueDegreeBaseChange PaperXI.FiniteResidueBaseChange
10 variable (k k' E : Type*) [Field k] [Fintype k] [Field k'] [Fintype k'] [Field E]
11   [Algebra k k'] [Algebra k E] [Algebra k' E] [Algebra.IsAlgebraic k E]
12 
13 /-- q-power Frobenius commutes with the actual field embedding. -/
14 theorem arithmetic_map (x : k') :
15     arithmetic k E (algebraMap k' E x) = algebraMap k' E (arithmetic k k' x) := by
16   simp only [arithmetic_apply, map_pow]
17 
18 /-- Its inverse commutes with that embedding as well. -/
19 theorem geometric_map (x : k') :
20     geometric k E (algebraMap k' E x) = algebraMap k' E (geometric k k' x) := by
21   apply (arithmetic k E).injective
22   change arithmetic k E ((arithmetic k E).symm (algebraMap k' E x)) = _
23   rw [(arithmetic k E).apply_symm_apply, arithmetic_map]
24   exact congrArg (algebraMap k' E) ((arithmetic k k').apply_symm_apply x).symm
25 
26 theorem geometric_pow_map (n : ℕ) (x : k') :
27     (geometric k E ^ n) (algebraMap k' E x) =
28       algebraMap k' E ((geometric k k' ^ n) x) := by
29   induction n with
30   | zero => rfl
31   | succ n ih =>
32     rw [pow_succ', pow_succ']
33     change geometric k E ((geometric k E ^ n) (algebraMap k' E x)) =
34       algebraMap k' E (geometric k k' ((geometric k k' ^ n) x))
35     rw [ih, geometric_map]
36 
37 /-- Integer powers preserve the convention even for negative Frobenius degrees. -/
38 theorem geometric_zpow_map (n : ℤ) (x : k') :
39     (geometric k E ^ n) (algebraMap k' E x) =
40       algebraMap k' E ((geometric k k' ^ n) x) := by
41   cases n with
42   | ofNat n =>
43     change (geometric k E ^ (n : ℤ)) (algebraMap k' E x) =
44       algebraMap k' E ((geometric k k' ^ (n : ℤ)) x)
45     simpa only [zpow_natCast] using geometric_pow_map k k' E n x
46   | negSucc n =>
47     simp only [zpow_negSucc, geometric, inv_pow, inv_inv]
48     simp only [arithmetic_pow_apply, map_pow]
49 
50 /-- Fixing all elements of the finite residue extension detects exact degree divisibility. -/
51 theorem fixes_subfield_iff (m : ℤ) :
52     (∀ x : k', (geometric k E ^ m) (algebraMap k' E x) = algebraMap k' E x) ↔
53       (Module.finrank k k' : ℤ) ∣ m := by
54   rw [← geometric_zpow_eq_one k k' m]
55   constructor
56   · intro h
57     apply RingEquiv.ext
58     intro x
59     apply (algebraMap k' E).injective
60     rw [← geometric_zpow_map]
61     exact h x
62   · intro h x
63     rw [geometric_zpow_map, h]
64     rfl
65 
66 section Group
67 variable {D : Type*} [Group D]
68 
69 /-- The genuine pointwise stabilizer of the embedded residue field. -/
70 def fixing (r : D →* RingAut E) : Subgroup D where
71   carrier := {g | ∀ x : k', r g (algebraMap k' E x) = algebraMap k' E x}
72   one_mem' := by intro x; simp
73   mul_mem' := by
74     intro g h hg hh x
75     rw [map_mul]
76     change r g (r h (algebraMap k' E x)) = _
77     rw [hh, hg]
78   inv_mem' := by
79     intro g hg x
80     rw [map_inv]
81     apply (r g).injective
82     change r g ((r g).symm (algebraMap k' E x)) = _
83     rw [(r g).apply_symm_apply, hg]
84 
85 omit [Field k] [Fintype k] [Fintype k'] [Algebra k k'] [Algebra k E]
86   [Algebra.IsAlgebraic k E] in
87 theorem kernel_le_fixing (r : D →* RingAut E) : r.ker ≤ fixing k' E r := by
88   intro g hg x
89   change r g = 1 at hg
90   rw [hg]
91   rfl
92 
93 /-- A lift fixes k' exactly when its integer Frobenius degree is divisible by [k':k]. -/
94 theorem projection_mem_iff (r : D →* RingAut E) (w : Pullback r (geometric k E)) :
95     projection r (geometric k E) w ∈ fixing k' E r ↔
96       (Module.finrank k k' : ℤ) ∣ Multiplicative.toAdd (degree r (geometric k E) w) := by
97   change (∀ x : k', r w.val.1 (algebraMap k' E x) = algebraMap k' E x) ↔ _
98   rw [w.property]
99   exact fixes_subfield_iff k k' E _
100 
101 variable [Algebra.IsAlgebraic k' E]
102 
103 /-- Under its own residue Frobenius, every pullback element fixes the residue base. -/
104 theorem projection_fixes (r : D →* RingAut E) (w : Pullback r (geometric k' E)) :
105     projection r (geometric k' E) w ∈ fixing k' E r := by
106   apply (projection_mem_iff k' k' E r w).mpr
107   simp
108 
109 /-- Restricting the decomposition action to the actual field-fixing subgroup loses no
110 pullback elements for geometric |k'|-Frobenius. -/
111 def fixingEquiv (r : D →* RingAut E) :
112     Pullback (r.comp (fixing k' E r).subtype) (geometric k' E) ≃*
113       Pullback r (geometric k' E) where
114   toFun w := ⟨(w.val.1.val, w.val.2), w.property⟩
115   invFun w := ⟨(⟨w.val.1, projection_fixes k' E r w⟩, w.val.2), w.property⟩
116   left_inv _ := rfl
117   right_inv _ := rfl
118   map_mul' _ _ := rfl
119 
120 /-- The source-facing residue-extension attachment. The left-hand subgroup is defined
121 by fixing the actual embedded field, while the right-hand one is a degree kernel. -/
122 def unramifiedEquiv (r : D →* RingAut E) :
123     Pullback (r.comp (fixing k' E r).subtype) (geometric k' E) ≃*
124       periodSubgroup r (geometric k E) (Module.finrank k k') :=
125   (fixingEquiv k' E r).trans (pullbackEquiv k E k' r)
126 
127 end Group
128 end PaperXI.FiniteResidueSubgroup

Back to source controls