LocalFieldResidueExtension.lean

1 import PaperXI.FiniteFreeCompletion
2 import Mathlib.FieldTheory.Finite.Extension
3 import Mathlib.NumberTheory.LocalField.Basic
4 
5 /-! Specialization at the actual ring of integers of a nonarchimedean local field.
6 The output ring, its residue and degree are constructed for every positive degree.
7 Absolute Weil groups and their smooth induction remain separate attachments. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.LocalFieldResidueExtension
11 open IsLocalRing ValuativeRel
12 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
13   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
14 variable (s : Type*) [Field s] [Algebra 𝓀[K] s] [FiniteDimensional 𝓀[K] s]
15 
16 abbrev ring := ResidueExtensionRealization.ring 𝒪[K] s
17 abbrev field := ResidueExtensionRealization.field 𝒪[K] s
18 
19 instance baseAlgebra : Algebra K (field K s) :=
20   (IsFractionRing.lift (K := K) (FaithfulSMul.algebraMap_injective 𝒪[K] (field K s))).toAlgebra
21 
22 instance baseTower : IsScalarTower 𝒪[K] K (field K s) :=
23   .of_algebraMap_eq fun x =>
24     (IsFractionRing.lift_algebraMap
25       (K := K) (FaithfulSMul.algebraMap_injective 𝒪[K] (field K s)) x).symm
26 
27 omit [IsUniformAddGroup K] in
28 theorem degree : Module.finrank K (field K s) = Module.finrank 𝓀[K] s := by
29   rw [IsFractionRing.finrank_eq 𝒪[K] K (ring K s) (field K s)]
30   exact ResidueExtensionRealization.rank 𝒪[K] s
31 
32 instance finiteExtension : FiniteDimensional K (field K s) :=
33   .of_finrank_pos ((degree K s).symm ▸ Module.finrank_pos)
34 
35 theorem source :
36     Module.Finite 𝒪[K] (ring K s) ∧
37     IsDiscreteValuationRing (ring K s) ∧
38     Algebra.Etale 𝒪[K] (ring K s) ∧
39     IsAdicComplete (maximalIdeal (ring K s)) (ring K s) ∧
40     Nonempty (ResidueField (ring K s) ≃ₐ[𝓀[K]] s) ∧
41     Module.finrank K (field K s) = Module.finrank 𝓀[K] s ∧
42     (maximalIdeal (ring K s)).ramificationIdx 𝒪[K] = 1 :=
43   ⟨inferInstance, inferInstance, ResidueExtensionRealization.etale 𝒪[K] s,
44     CompleteResidueRealization.complete 𝒪[K] s,
45     ⟨ResidueExtensionRealization.residueEquiv 𝒪[K] s⟩,
46     degree K s, ResidueExtensionRealization.ramificationIdx_one 𝒪[K] s⟩
47 
48 variable (p n : ℕ) [Fact p.Prime] [CharP 𝓀[K] p] [NeZero n]
49 
50 abbrev residueExtension := FiniteField.Extension 𝓀[K] p n
51 
52 theorem every_positive_degree :
53     Module.finrank K (field K (residueExtension K p n)) = n ∧
54     Algebra.Etale 𝒪[K] (ring K (residueExtension K p n)) ∧
55     IsAdicComplete (maximalIdeal (ring K (residueExtension K p n)))
56       (ring K (residueExtension K p n)) ∧
57     (maximalIdeal (ring K (residueExtension K p n))).ramificationIdx 𝒪[K] = 1 := by
58   exact ⟨(degree K _).trans (FiniteField.finrank_extension 𝓀[K] p n),
59     ResidueExtensionRealization.etale 𝒪[K] _,
60     CompleteResidueRealization.complete 𝒪[K] _,
61     ResidueExtensionRealization.ramificationIdx_one 𝒪[K] _⟩
62 
63 end PaperXI.LocalFieldResidueExtension

Back to source controls