NormalizedFrobeniusQuotient.lean

1 import PaperXI.SpectralGeometricFrobenius
2 import PaperXI.RamifiedUnramifiedQuotient
3 
4 /-!
5 # The field-normalized Frobenius pullback and its inertia quotient
6 
7 All valuation data below come from the same finite Galois spectral extension.
8 The degree-one element and surjectivity of degree are derived, not certificate
9 fields. The quotient remains a bounded pullback model, not an absolute Weil group.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 
14 namespace PaperXI.NormalizedFrobeniusQuotient
15 open IsLocalRing
16 open PaperXI.SpectralGeometricFrobenius
17 
18 variable (E L : Type*) [NontriviallyNormedField E] [IsUltrametricDist E]
19   [CompleteSpace E] [ProperSpace E] [Field L] [Algebra E L]
20   [FiniteDimensional E L]
21 
22 abbrev Decomposition := (integers E L).decompositionSubgroup E
23 abbrev residueHom : Decomposition E L →* RingAut (ExtensionResidue E L) :=
24   PaperXI.ResidueWeil.residueAction E (integers E L)
25 abbrev Weil := PaperXI.ResidueWeil.Pullback (residueHom E L) (geometricFrobenius E L)
26 abbrev degree : Weil E L →* Multiplicative ℤ :=
27   PaperXI.ResidueWeil.degree (residueHom E L) (geometricFrobenius E L)
28 abbrev Inertia := (degree E L).ker
29 
30 /-- Pullback inertia is the actual valuation inertia, without a cyclicity assumption. -/
31 def inertiaEquiv : Inertia E L ≃* (integers E L).inertiaSubgroup E :=
32   PaperXI.ResidueWeil.valuationInertiaEquiv E (integers E L) (geometricFrobenius E L)
33 
34 variable [IsGalois E L]
35 
36 /-- The derived geometric lift as an element of the actual decomposition group. -/
37 def decompositionLift : Decomposition E L :=
38   ⟨geometricLift E L, automorphism_stable E L (geometricLift E L)⟩
39 
40 theorem residue_decompositionLift :
41     residueHom E L (decompositionLift E L) = geometricFrobenius E L :=
42   residue_geometricLift E L
43 
44 /-- The former lifting premise is now a conclusion about this actual field extension. -/
45 theorem frobenius_mem_range : geometricFrobenius E L ∈ (residueHom E L).range :=
46   ⟨decompositionLift E L, residue_decompositionLift E L⟩
47 
48 /-- A geometric degree-one lift in the field-normalized pullback. -/
49 def weilGeometricLift : Weil E L :=
50   ⟨(decompositionLift E L, Multiplicative.ofAdd (1 : ℤ)), by
51     change residueHom E L (decompositionLift E L) = geometricFrobenius E L ^ (1 : ℤ)
52     rw [zpow_one, residue_decompositionLift]⟩
53 
54 @[simp]
55 theorem degree_geometricLift :
56     degree E L (weilGeometricLift E L) = Multiplicative.ofAdd (1 : ℤ) := rfl
57 
58 /-- The chosen geometric lift is normalized by the full residue size of E. -/
59 theorem lift_inverse_power (x : ExtensionResidue E L) :
60     (residueHom E L (decompositionLift E L) x) ^ Nat.card (BaseResidue E L) = x := by
61   rw [residue_decompositionLift]
62   exact geometric_inverse_power E L x
63 
64 /-- Arithmetic Frobenius is the inverse of this geometric lift. -/
65 def weilArithmeticLift : Weil E L := (weilGeometricLift E L)⁻¹
66 
67 @[simp]
68 theorem degree_arithmeticLift :
69     degree E L (weilArithmeticLift E L) = Multiplicative.ofAdd (-1 : ℤ) := by
70   rw [weilArithmeticLift, map_inv, degree_geometricLift]
71   rfl
72 
73 /-- All integer degrees occur: no degree-surjectivity hypothesis remains. -/
74 theorem degree_surjective : Function.Surjective (degree E L) :=
75   PaperXI.RamifiedUnramifiedQuotient.degree_surjective_of_frobenius_mem_range
76     (residueHom E L) (geometricFrobenius E L) (frobenius_mem_range E L)
77 
78 /-- The v0.44 quotient theorem instantiated with a proved field-side lift. -/
79 def quotientEquivIntegerDegree : Weil E L ⧸ Inertia E L ≃* Multiplicative ℤ :=
80   PaperXI.RamifiedUnramifiedQuotient.quotientEquivIntegerDegree
81     (residueHom E L) (geometricFrobenius E L) (frobenius_mem_range E L)
82 
83 @[simp]
84 theorem quotientEquivIntegerDegree_mk (w : Weil E L) :
85     quotientEquivIntegerDegree E L (QuotientGroup.mk w) = degree E L w :=
86   PaperXI.RamifiedUnramifiedQuotient.quotientEquivIntegerDegree_mk
87     (residueHom E L) (geometricFrobenius E L) (frobenius_mem_range E L) w
88 
89 @[simp]
90 theorem quotient_geometricLift :
91     quotientEquivIntegerDegree E L (QuotientGroup.mk (weilGeometricLift E L)) =
92       Multiplicative.ofAdd (1 : ℤ) := by
93   rw [quotientEquivIntegerDegree_mk, degree_geometricLift]
94 
95 section FixedVectors
96 omit [IsGalois E L]
97 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
98 variable (ρ : Representation ℂ (Weil E L) V)
99 
100 /-- The coarse inertia-fixed channel cannot distinguish degree-one lifts.
101 No such assertion is made on ramified detail channels. -/
102 theorem degree_one_action_eq_on_invariants
103     (a b : Weil E L)
104     (ha : degree E L a = Multiplicative.ofAdd (1 : ℤ))
105     (hb : degree E L b = Multiplicative.ofAdd (1 : ℤ))
106     (v : Representation.invariants (ρ.comp (Inertia E L).subtype)) :
107     ρ a (v : V) = ρ b (v : V) := by
108   have hd : b⁻¹ * a ∈ Inertia E L := by
109     change degree E L (b⁻¹ * a) = 1
110     rw [map_mul, map_inv, ha, hb]
111     simp
112   have hv : ρ (b⁻¹ * a) (v : V) = (v : V) := v.property ⟨b⁻¹ * a, hd⟩
113   calc
114     ρ a (v : V) = ρ b (ρ (b⁻¹ * a) (v : V)) := by
115       rw [← Module.End.mul_apply, ← map_mul]
116       simp
117     _ = ρ b (v : V) := congrArg (fun x => ρ b x) hv
118 
119 end FixedVectors
120 end PaperXI.NormalizedFrobeniusQuotient

Back to source controls