ClassFormation.ValuationData.abstractReciprocity_cyclicTotallyRamified_exponent_eq_zero
The exponent in the chosen cyclic decomposition is zero.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology
-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
-- The two fixed-field presentations have the same canonical addition.
-- Fix its homogeneous type before elaborating the bundled second operand.
local infixl:65 (priority := high) " + " =>
(fun {α : Type _} [Add α] (a b : α) => HAdd.hAdd a b)Lean source · full declaration
theorem abstractReciprocity_cyclicTotallyRamified_exponent_eq_zero
(v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
[IsTopologicalGroup G] [CompactSpace G] [T2Space G]
[TotallyDisconnectedSpace G]
(K : FiniteAbstractField G)
(E : FiniteCyclicSubextension K)
(hTot : E.IsTotallyRamified D)
(k : ℕ)
(hk : k < (E.toFiniteAbstractExtension.degree : ℕ))
(piSigma : ambientFixedAddSubgroup A
(D.frobeniusFixedField (K.toFiniteResidueAbstractField D)
E.field E.below
(D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
(K.toFiniteResidueAbstractField D)
E.toFiniteGaloisSubextension
hTot
E.galoisGenerator)))
(piL : ambientFixedAddSubgroup A E.field) :
let L := E.toFiniteAbstractFieldExtension.field
let KR := K.toFiniteResidueAbstractField D
letI : Finite
((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) KR.field
(le_baseField KR.field)) := by
change Finite
((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) K.field
(le_baseField K.field))
exact K.finite
let LG := E.toFiniteGaloisSubextension
letI : Finite
(KR.field.toSubgroup ⧸
extensionSubgroup KR.field LG.field LG.below) :=
LG.finite
let q := E.galoisGenerator
let hLGTot := hTot
let σ := D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
KR LG hLGTot q
let Sigma := D.frobeniusFixedField KR LG.field LG.below σ
let hSigmaK := D.frobeniusFixedField_le KR LG.field LG.below σ
letI : Finite
(K.field.toSubgroup ⧸ extensionSubgroup K.field Sigma hSigmaK) :=
D.frobeniusFixedField_finite KR LG.field LG.below σ
∀ (w : v.unitAddSubgroup L)
(_hpiL : v.IsPrimeElement L piL)
(_hnorm :
relativeNorm A K.field E.field E.below (k • piL + w.1) =
relativeNorm A K.field Sigma hSigmaK (k • piSigma)),
k = 0 := by
dsimp only
let L := E.toFiniteAbstractFieldExtension.field
let KR := K.toFiniteResidueAbstractField D
let LG := E.toFiniteGaloisSubextension
let hLGfinite : Finite
(KR.field.toSubgroup ⧸
extensionSubgroup KR.field LG.field LG.below) :=
LG.finite
let hLGfiniteOverK : Finite
(K.field.toSubgroup ⧸
extensionSubgroup K.field LG.field LG.below) := by
have h := hLGfinite
change Finite
(K.field.toSubgroup ⧸
extensionSubgroup K.field LG.field LG.below) at h
exact h
let q := E.galoisGenerator
let hLGTot := hTot
let hKRabsolute : Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) KR.field (le_baseField KR.field)) := by
change Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) K.field (le_baseField K.field))
exact K.finite
let σ := D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
KR LG hLGTot q
let Sigma := D.frobeniusFixedField KR LG.field LG.below σ
let hSigmaK := D.frobeniusFixedField_le KR LG.field LG.below σ
let hSigmaFinite : Finite
(K.field.toSubgroup ⧸ extensionSubgroup K.field Sigma hSigmaK) :=
D.frobeniusFixedField_finite KR LG.field LG.below σ
intro w hpiL hnorm
let M := D.abstractReciprocityTotallyRamifiedFiniteGaloisExtension
KR LG hLGTot q
let hMfinite : Finite
(KR.field.toSubgroup ⧸
extensionSubgroup KR.field M.field M.below) :=
M.finite
let S := M.inertiaImage D
let M₀ := M.maximalUnramifiedSubextension D
let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
M.field_le_intermediateField S
let hM₀K : M₀.toSubgroup ≤ K.field.toSubgroup :=
M.intermediateField_le_base S
let N := M.lowerFiniteGalois S
let hNnormal : (extensionSubgroup M₀ M.field hMM₀).Normal := N.normal
let hNfinite : Finite
(M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) :=
N.finite
let hM₀finite : Finite
(K.field.toSubgroup ⧸ extensionSubgroup K.field M₀ hM₀K) :=
M.intermediateField_finite S
let hM₀absolute : Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) M₀ (le_baseField M₀)) :=
FiniteGaloisSubextension.finite_extension_trans hM₀K (le_baseField K.field)
let hMabsolute : Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) M.field (le_baseField M.field)) :=
FiniteGaloisSubextension.finite_extension_trans M.below (le_baseField K.field)
let MF : FiniteAbstractField G := ⟨M.field, hMabsolute⟩
let M₀F : FiniteAbstractField G := ⟨M₀, hM₀absolute⟩
let EN : FiniteAbstractFieldExtension G :=
{ field := MF
base := M₀F
below := hMM₀
finiteQuotient := hNfinite }
obtain ⟨x, hx⟩ :=
v.abstractReciprocity_cyclicTotallyRamified_fixedSource hcf
K E hTot k piSigma piL w hpiL hnorm
have hkLower : k < (N.toFiniteAbstractExtension.degree : ℕ) := by
rw [D.abstractReciprocityTotallyRamifiedLowerDegree_eq
KR LG hLGTot q]
exact hk
exact abstractReciprocity_totallyRamified_valuation_forces_exponent_zero
v EN (by
simpa [EN, FiniteAbstractFieldExtension.IsTotallyRamified,
FiniteAbstractFieldExtension.toFiniteAbstractExtension] using
M.maximalUnramifiedSubextension_isTotallyRamified D)
k hkLower x hx