ConstructedFieldFrobenius.lean

1 import PaperXI.SpectralGeometricFrobenius
2 import PaperXI.SpectralLocalField
3 
4 /-!
5 # Specialization to Paper XI's constructed spectral local field
6 
7 The base of the finite Galois extension is the literal UpperField(K,s) from the
8 verified predecessor. The base residue cardinality in geometric normalization
9 is identified with the residue cardinality of that same field, by equality of
10 integer subrings and the induced residue equivalence.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.ConstructedFieldFrobenius
15 open ValuativeRel IsLocalRing
16 open PaperXI.SpectralGeometricFrobenius
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] [FiniteDimensional 𝓀[K] s]
21 
22 abbrev BaseField := PaperXI.SpectralLocalField.UpperField K s
23 
24 variable (L : Type*) [Field L] [Algebra (BaseField K s) L]
25   [FiniteDimensional (BaseField K s) L]
26 
27 /-- The restricted extension valuation recovers this very base's integer subring. -/
28 theorem restricted_integer_subring :
29     ((integers (BaseField K s) L).comap
30       (algebraMap (BaseField K s) (SpectralExtension (BaseField K s) L))).toSubring =
31       (ValuativeRel.valuation (BaseField K s)).integer := by
32   rw [integers_comap]
33   exact (PaperXI.SpectralLocalField.relation_integer_eq_norm_integer K s).symm
34 
35 /-- The underlying base integer rings are equal, not merely equicardinal. -/
36 def baseIntegerEquiv :
37     (integers (BaseField K s) L).comap
38       (algebraMap (BaseField K s) (SpectralExtension (BaseField K s) L)) ≃+*
39         𝒪[BaseField K s] :=
40   RingEquiv.subringCongr (restricted_integer_subring K s L)
41 
42 /-- Residue identification obtained from that literal integer-subring equality. -/
43 def baseResidueEquiv : BaseResidue (BaseField K s) L ≃+* 𝓀[BaseField K s] :=
44   IsLocalRing.ResidueField.mapEquiv (baseIntegerEquiv K s L)
45 
46 theorem baseResidue_card :
47     Nat.card (BaseResidue (BaseField K s) L) = Nat.card 𝓀[BaseField K s] :=
48   Nat.card_congr (baseResidueEquiv K s L).toEquiv
49 
50 variable [IsGalois (BaseField K s) L]
51 
52 /-- An actual automorphism lifting geometric Frobenius normalized by the residue
53 cardinality of Paper XI's constructed base field. -/
54 theorem exists_normalized_field_automorphism :
55     ∃ g : SpectralExtension (BaseField K s) L ≃ₐ[BaseField K s]
56         SpectralExtension (BaseField K s) L,
57       residueAction (BaseField K s) L g = geometricFrobenius (BaseField K s) L ∧
58       ∀ x : ExtensionResidue (BaseField K s) L,
59         (residueAction (BaseField K s) L g x) ^ Nat.card 𝓀[BaseField K s] = x := by
60   refine ⟨geometricLift (BaseField K s) L, residue_geometricLift _ _, ?_⟩
61   intro x
62   rw [← baseResidue_card K s L]
63   exact geometricLift_normalized (BaseField K s) L x
64 
65 end PaperXI.ConstructedFieldFrobenius

Back to source controls