ResidueFrobeniusAttachment.lean

1 import PaperXI.IntegerRingComparison
2 import Mathlib.FieldTheory.Finite.Basic
3 import Mathlib.FieldTheory.Galois.Basic
4 import Mathlib.GroupTheory.SpecificGroups.Cyclic
5 
6 /-! # Frobenius attachment to the constructed residue field -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperXI.FiniteUnramifiedWeil
12 
13 open PaperXI.LocalFieldResidueExtension
14 open PaperXI.IntegerRingComparison
15 open ValuativeRel
16 open scoped Classical Polynomial
17 
18 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
19   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
20 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
21   [FiniteDimensional 𝓀[K] s]
22 
23 abbrev UpperField := LocalFieldResidueExtension.field K s
24 abbrev BaseResidue := 𝓀[K]
25 abbrev UpperResidue := 𝓀[UpperField K s]
26 abbrev ResidueGalois := UpperResidue K s ≃ₐ[BaseResidue K] UpperResidue K s
27 abbrev ResidueDegree := Module.finrank K (UpperField K s)
28 
29 private local instance baseResidueFintype : Fintype (BaseResidue K) :=
30   Fintype.ofFinite _
31 
32 private local instance upperResidueFintype : Fintype (UpperResidue K s) :=
33   Fintype.ofFinite _
34 
35 /-- Arithmetic Frobenius on the actual residue field of the constructed local field. -/
36 noncomputable def arithmeticFrobenius : ResidueGalois K s :=
37   FiniteField.frobeniusAlgEquivOfAlgebraic (BaseResidue K) (UpperResidue K s)
38 
39 /-- Geometric Frobenius is the inverse of arithmetic Frobenius. -/
40 noncomputable def geometricFrobenius : ResidueGalois K s :=
41   (arithmeticFrobenius K s)⁻¹
42 
43 @[simp]
44 theorem arithmeticFrobenius_apply (x : UpperResidue K s) :
45     arithmeticFrobenius K s x = x ^ Fintype.card (BaseResidue K) :=
46   rfl
47 
48 @[simp]
49 theorem geometricFrobenius_inverse_power (x : UpperResidue K s) :
50     geometricFrobenius K s x ^ Fintype.card (BaseResidue K) = x := by
51   rw [← arithmeticFrobenius_apply K s]
52   exact (arithmeticFrobenius K s).apply_symm_apply x
53 
54 /-- Arithmetic Frobenius has order equal to the spectral residue degree. -/
55 theorem arithmeticFrobenius_order :
56     orderOf (arithmeticFrobenius K s) =
57       Module.finrank (BaseResidue K) (UpperResidue K s) :=
58   FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic _ _
59 
60 /-- Geometric Frobenius has the same exact order. -/
61 theorem geometricFrobenius_order :
62     orderOf (geometricFrobenius K s) =
63       Module.finrank (BaseResidue K) (UpperResidue K s) := by
64   rw [geometricFrobenius, orderOf_inv, arithmeticFrobenius_order]
65 
66 /-- Frobenius order agrees with the degree of the constructed local-field extension. -/
67 theorem arithmeticFrobenius_order_eq_fieldDegree :
68     orderOf (arithmeticFrobenius K s) = ResidueDegree K s := by
69   rw [arithmeticFrobenius_order]
70   exact (upper_degree_eq_spectral_residue_finrank K s).symm
71 
72 /-- Geometric Frobenius order agrees with the field degree. -/
73 theorem geometricFrobenius_order_eq_fieldDegree :
74     orderOf (geometricFrobenius K s) = ResidueDegree K s := by
75   rw [geometricFrobenius_order]
76   exact (upper_degree_eq_spectral_residue_finrank K s).symm
77 
78 /-- The residue Galois group has cardinality equal to the upper field degree. -/
79 theorem natCard_residueGalois :
80     Nat.card (ResidueGalois K s) = ResidueDegree K s := by
81   rw [IsGalois.card_aut_eq_finrank]
82   exact (upper_degree_eq_spectral_residue_finrank K s).symm
83 
84 /-- Every residue automorphism is an integral power of arithmetic Frobenius. -/
85 theorem arithmeticFrobenius_mem_zpowers (σ : ResidueGalois K s) :
86     σ ∈ Subgroup.zpowers (arithmeticFrobenius K s) := by
87   obtain ⟨n, hn⟩ :=
88     (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow
89       (BaseResidue K) (UpperResidue K s)).2 σ
90   rw [Subgroup.mem_zpowers_iff]
91   refine ⟨(n.1 : ℤ), ?_⟩
92   simpa [arithmeticFrobenius, zpow_natCast] using hn
93 
94 /-- Arithmetic Frobenius generates the full residue Galois group. -/
95 theorem arithmeticFrobenius_zpowers_eq_top :
96     Subgroup.zpowers (arithmeticFrobenius K s) = ⊤ := by
97   rw [Subgroup.eq_top_iff']
98   exact arithmeticFrobenius_mem_zpowers K s
99 
100 /-- Geometric Frobenius also generates the full residue Galois group. -/
101 theorem geometricFrobenius_zpowers_eq_top :
102     Subgroup.zpowers (geometricFrobenius K s) = ⊤ := by
103   rw [geometricFrobenius, Subgroup.zpowers_inv,
104     arithmeticFrobenius_zpowers_eq_top]
105 
106 /-- Explicit cyclic coordinates in which one is geometric Frobenius. -/
107 noncomputable def geometricCycleEquiv :
108     Multiplicative (ZMod (ResidueDegree K s)) ≃* ResidueGalois K s :=
109   zmodMulEquivOfGenerator
110     (fun σ => by
111       rw [geometricFrobenius_zpowers_eq_top K s]
112       trivial)
113     (natCard_residueGalois K s)
114 
115 @[simp]
116 theorem geometricCycleEquiv_one :
117     geometricCycleEquiv K s (Multiplicative.ofAdd 1) = geometricFrobenius K s :=
118   zmodMulEquivOfGenerator_apply_ofAdd_one _ _
119 
120 /-- Galois groups of the spectral residue field and the prescribed residue field
121 are conjugate through the checked residue-field equivalence. -/
122 noncomputable def prescribedResidueGaloisEquiv :
123     ResidueGalois K s ≃* (s ≃ₐ[BaseResidue K] s) :=
124   AlgEquiv.autCongr (spectralResidueAlgEquiv K s)
125 
126 /-- Arithmetic Frobenius is transported literally to arithmetic Frobenius on `s`. -/
127 theorem prescribedResidueGaloisEquiv_arithmetic :
128     prescribedResidueGaloisEquiv K s (arithmeticFrobenius K s) =
129       FiniteField.frobeniusAlgEquivOfAlgebraic (BaseResidue K) s := by
130   apply AlgEquiv.ext
131   intro x
132   let e := spectralResidueAlgEquiv K s
133   change e ((e.symm x) ^ Fintype.card (BaseResidue K)) =
134     x ^ Fintype.card (BaseResidue K)
135   rw [map_pow, e.apply_symm_apply]
136 
137 /-- Geometric Frobenius is transported literally to geometric Frobenius on `s`. -/
138 theorem prescribedResidueGaloisEquiv_geometric :
139     prescribedResidueGaloisEquiv K s (geometricFrobenius K s) =
140       (FiniteField.frobeniusAlgEquivOfAlgebraic (BaseResidue K) s)⁻¹ := by
141   rw [geometricFrobenius, map_inv, prescribedResidueGaloisEquiv_arithmetic]
142 
143 
144 end PaperXI.FiniteUnramifiedWeil

Back to source controls