LocalClassFieldTheory.finiteCyclicUnitsH2_inflation_restriction_eq_zero
A cyclic lower-field H² class becomes zero after inflation to an unramified relative extension whose degree divides the lower ramification index.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
open scoped ValuativeRel
namespace LocalClassFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField ClassFieldTower.CohomologyLean source · statement
theorem finiteCyclicUnitsH2_inflation_restriction_eq_zero
(K N : Type)
[Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[Field N] [Algebra K N] [ValuativeRel N] [TopologicalSpace N]
[IsNonarchimedeanLocalField N]
(L M : IntermediateField K N)
[ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
[FiniteDimensional K L] [Algebra.IsSeparable K L]
[FiniteDimensional L N] [IsGalois L N]
[FiniteDimensional K M] [IsGalois K M] [IsCyclic Gal(M/K)]
[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]) :
finiteGaloisUnitsH2Inflation K N M ≫ finiteGaloisUnitsH2Restriction K N L = 0