LocalClassFieldTheory.finiteTowerBaseUnitsH2Map_eq_zero_of_finrank_dvd_ramificationIdx
The coefficient map from base-field units vanishes when the unramified top degree divides the ramification index of the lower extension.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open ClassFieldTower.CohomologyLean source · statement
theorem finiteTowerBaseUnitsH2Map_eq_zero_of_finrank_dvd_ramificationIdx
(K L N : Type)
[Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[Field L] [ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
[Field N] [ValuativeRel N] [TopologicalSpace N]
[IsNonarchimedeanLocalField N]
[Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
[Algebra L N] [FiniteDimensional L N] [IsGalois L N]
[Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation L)]
[Valuation.HasExtension (ValuativeRel.valuation L)
(ValuativeRel.valuation N)]
[Module.Finite 𝒪[L] 𝒪[N]] [IsUnramifiedValuedExtension L N]
(hd : Module.finrank L N ∣
(𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K]) :
finiteTowerBaseUnitsH2Map K L N = 0