SpectralGeometricFrobenius.lean

1 import PaperXI.HenselianGaloisResidue
2 import PaperXI.HenselianLiftTower
3 import PaperXI.FiniteResidueBaseChange
4 import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
5 import Mathlib.Analysis.Normed.Module.FiniteDimension
6 import Mathlib.NumberTheory.LocalField.Basic
7 
8 /-!
9 # Geometric Frobenius for a finite Galois spectral extension
10 
11 The integer ring is constructed from the spectral norm of the actual extension.
12 Valuation stability, the Hensel property, and residue finiteness are derived.
13 The Frobenius-lift premise is then discharged by the inherited Galois/Hensel
14 surjectivity theorem. No full absolute Weil group or automorphic object is asserted.
15 -/
16 set_option autoImplicit false
17 noncomputable section
18 
19 namespace PaperXI.SpectralGeometricFrobenius
20 open IsLocalRing ValuativeRel
21 open scoped Pointwise
22 
23 variable (E L : Type*) [NontriviallyNormedField E] [IsUltrametricDist E]
24   [CompleteSpace E] [ProperSpace E] [Field L] [Algebra E L]
25   [FiniteDimensional E L]
26 
27 /-- A transparent copy of L recording which base supplies the spectral norm. -/
28 def SpectralExtension (_E L : Type*) := L
29 
30 instance spectralField : Field (SpectralExtension E L) := inferInstanceAs (Field L)
31 instance spectralAlgebra : Algebra E (SpectralExtension E L) := inferInstanceAs (Algebra E L)
32 instance spectralFinite : FiniteDimensional E (SpectralExtension E L) :=
33   inferInstanceAs (FiniteDimensional E L)
34 instance spectralGalois [IsGalois E L] : IsGalois E (SpectralExtension E L) :=
35   inferInstanceAs (IsGalois E L)
36 
37 /-- The copy has precisely the original field and base-algebra operations. -/
38 def originalFieldEquiv : SpectralExtension E L ≃ₐ[E] L := AlgEquiv.refl
39 
40 local notation "Lₛ" => SpectralExtension E L
41 
42 private local instance extensionNorm : NormedField Lₛ := spectralNorm.normedField E Lₛ
43 private local instance extensionNontrivial : NontriviallyNormedField Lₛ :=
44   spectralNorm.nontriviallyNormedField E Lₛ
45 private local instance extensionSpace : NormedSpace E Lₛ := spectralNorm.normedSpace E Lₛ
46 private local instance extensionAlgebra : NormedAlgebra E Lₛ := spectralNorm.normedAlgebra E Lₛ
47 private local instance extensionComplete : CompleteSpace Lₛ := spectralNorm.completeSpace E Lₛ
48 private local instance extensionProper : ProperSpace Lₛ := FiniteDimensional.proper E Lₛ
49 private local instance extensionUltra : IsUltrametricDist Lₛ := by
50   constructor
51   intro x y z
52   change (spectralNorm E Lₛ (x-z) : ℝ) ≤
53     max (spectralNorm E Lₛ (x-y) : ℝ) (spectralNorm E Lₛ (y-z) : ℝ)
54   rw [← sub_add_sub_cancel x y z]
55   exact_mod_cast isNonarchimedean_spectralNorm (K := E) (L := Lₛ) (x-y) (y-z)
56 private local instance extensionValued : Valued Lₛ NNReal := NormedField.toValued
57 private local instance extensionRel : ValuativeRel Lₛ :=
58   ValuativeRel.ofValuation (NormedField.valuation (K := Lₛ))
59 private local instance extensionCompatible : (NormedField.valuation (K := Lₛ)).Compatible :=
60   Valuation.Compatible.ofValuation _
61 private local instance extensionTopology : IsValuativeTopology Lₛ := by
62   exact IsValuativeTopology.of_mem_nhds_zero_iff_vle
63     (NormedField.valuation (K := Lₛ)) (by intro U; exact Valued.mem_nhds_zero)
64 private local instance extensionValNontrivial : ValuativeRel.IsNontrivial Lₛ := by
65   exact (ValuativeRel.isNontrivial_iff_isNontrivial
66     (NormedField.valuation (K := Lₛ))).mpr inferInstance
67 private local instance extensionLocalField : IsNonarchimedeanLocalField Lₛ where
68   toIsValuativeTopology := inferInstance
69   toLocallyCompactSpace := inferInstance
70   toIsNontrivial := inferInstance
71 
72 /-- The actual spectral valuation ring in the given extension field. -/
73 def integers : ValuationSubring Lₛ := (ValuativeRel.valuation Lₛ).valuationSubring
74 
75 /-- The base integer ring, using the original norm on E. -/
76 def baseIntegers : ValuationSubring E := (NormedField.valuation (K := E)).valuationSubring
77 
78 omit [ProperSpace E] in
79 /-- Spectral integrality is norm at most one. -/
80 theorem mem_integers (x : Lₛ) : x ∈ integers E L ↔ spectralNorm E Lₛ x ≤ 1 := by
81   change ValuativeRel.valuation Lₛ x ≤ 1 ↔ _
82   have h := ValuativeRel.isEquiv (NormedField.valuation (K := Lₛ))
83     (ValuativeRel.valuation Lₛ) x 1
84   have h' : (ValuativeRel.valuation Lₛ x ≤ 1 ↔ ‖x‖₊ ≤ 1) := by
85     simpa using h.symm
86   rw [h']
87   change ‖x‖₊ ≤ 1 ↔ ‖x‖ ≤ 1
88   exact NNReal.coe_le_coe
89 
90 omit [ProperSpace E] in
91 /-- Restricting this valuation ring recovers the original norm-integer ring. -/
92 theorem integers_comap : (integers E L).comap (algebraMap E Lₛ) = baseIntegers E := by
93   ext x
94   change algebraMap E Lₛ x ∈ integers E L ↔ _
95   rw [mem_integers]
96   change spectralNorm E Lₛ (algebraMap E Lₛ x) ≤ 1 ↔ ‖x‖₊ ≤ 1
97   exact_mod_cast (show spectralNorm E Lₛ (algebraMap E Lₛ x) ≤ 1 ↔ ‖x‖ ≤ 1 by
98     rw [spectralNorm_extends (K := E) (L := Lₛ)])
99 
100 omit [ProperSpace E] in
101 /-- Every base-field automorphism of the extension preserves its spectral integers. -/
102 theorem automorphism_stable (g : Lₛ ≃ₐ[E] Lₛ) :
103     g ∈ (integers E L).decompositionSubgroup E := by
104   change g • integers E L = integers E L
105   ext x
106   rw [ValuationSubring.mem_smul_pointwise_iff_exists]
107   constructor
108   · rintro ⟨y, hy, rfl⟩
109     rw [mem_integers] at hy ⊢
110     exact (spectralNorm_eq_of_equiv g y) ▸ hy
111   · intro hx
112     refine ⟨g.symm x, ?_, g.apply_symm_apply x⟩
113     rw [mem_integers] at hx ⊢
114     exact (spectralNorm_eq_of_equiv g.symm x) ▸ hx
115 
116 instance integersDVR : IsDiscreteValuationRing (integers E L) := by
117   change IsDiscreteValuationRing 𝒪[Lₛ]
118   infer_instance
119 
120 instance integersFiniteResidue : Finite (ResidueField (integers E L)) := by
121   change Finite 𝓀[Lₛ]
122   infer_instance
123 
124 instance integersHenselian : HenselianLocalRing (integers E L) := by
125   change HenselianLocalRing 𝒪[Lₛ]
126   exact HenselianLiftTower.henselian_of_complete
127 
128 abbrev BaseResidue := ResidueField ((integers E L).comap (algebraMap E Lₛ))
129 abbrev ExtensionResidue := ResidueField (integers E L)
130 
131 private local instance baseFinite : Finite (BaseResidue E L) :=
132   Finite.of_injective (ValuationResidueEmbedding.residueMap (integers E L) (algebraMap E Lₛ))
133     (ValuationResidueEmbedding.residueMap_injective (integers E L) (algebraMap E Lₛ))
134 private local instance baseFintype : Fintype (BaseResidue E L) := Fintype.ofFinite _
135 private local instance upperFintype : Fintype (ExtensionResidue E L) := Fintype.ofFinite _
136 private local instance residueAlgebra : Algebra (BaseResidue E L) (ExtensionResidue E L) :=
137   (ValuationResidueEmbedding.residueMap (integers E L) (algebraMap E Lₛ)).toAlgebra
138 
139 /-- Geometric residue Frobenius is the inverse of the actual cardinality-power map. -/
140 def geometricFrobenius : RingAut (ExtensionResidue E L) :=
141   FiniteResidueBaseChange.geometric (BaseResidue E L) (ExtensionResidue E L)
142 
143 /-- Arithmetic residue Frobenius uses the original full base residue field. -/
144 def arithmeticFrobenius : RingAut (ExtensionResidue E L) :=
145   FiniteResidueBaseChange.arithmetic (BaseResidue E L) (ExtensionResidue E L)
146 
147 theorem arithmetic_apply (x : ExtensionResidue E L) :
148     arithmeticFrobenius E L x = x ^ Nat.card (BaseResidue E L) := by
149   simpa only [arithmeticFrobenius, Nat.card_eq_fintype_card] using
150     FiniteResidueBaseChange.arithmetic_apply (BaseResidue E L) (ExtensionResidue E L) x
151 
152 theorem geometric_inverse_power (x : ExtensionResidue E L) :
153     geometricFrobenius E L x ^ Nat.card (BaseResidue E L) = x := by
154   simpa only [geometricFrobenius, Nat.card_eq_fintype_card] using
155     FiniteResidueBaseChange.geometric_inverse_power (BaseResidue E L) (ExtensionResidue E L) x
156 
157 /-- The actual action on the residue field induced by field automorphisms. -/
158 def residueAction : (Lₛ ≃ₐ[E] Lₛ) →* RingAut (ExtensionResidue E L) :=
159   HenselianGaloisResidue.residueAction E (integers E L) (automorphism_stable E L)
160 
161 variable [IsGalois E L]
162 
163 /-- A normalized geometric Frobenius lift exists; no residue-surjectivity premise is supplied. -/
164 theorem exists_geometric_lift : ∃ g : Lₛ ≃ₐ[E] Lₛ,
165     residueAction E L g = geometricFrobenius E L := by
166   apply HenselianGaloisResidue.lift_automorphism E (integers E L) (automorphism_stable E L)
167   intro x
168   exact (FiniteField.frobeniusAlgEquivOfAlgebraic (BaseResidue E L)
169     (ExtensionResidue E L)).symm.commutes x
170 
171 /-- A selected actual field automorphism lifting geometric Frobenius. -/
172 def geometricLift : Lₛ ≃ₐ[E] Lₛ := (exists_geometric_lift E L).choose
173 
174 theorem residue_geometricLift :
175     residueAction E L (geometricLift E L) = geometricFrobenius E L :=
176   (exists_geometric_lift E L).choose_spec
177 
178 /-- Arithmetic normalization of the same lift, expressed as a residue equation. -/
179 theorem geometricLift_normalized (x : ExtensionResidue E L) :
180     (residueAction E L (geometricLift E L) x) ^ Nat.card (BaseResidue E L) = x := by
181   rw [residue_geometricLift]
182   exact geometric_inverse_power E L x
183 
184 end PaperXI.SpectralGeometricFrobenius

Back to source controls