LocalClassFieldTheory.finiteCyclicTowerUnitsH2_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 finiteCyclicTowerUnitsH2_inflation_restriction_eq_zero
(K L M N : Type)
[Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[Field N] [Algebra K N] [ValuativeRel N] [TopologicalSpace N]
[IsNonarchimedeanLocalField N]
[Field L] [Field M]
[Algebra K L] [Algebra L N] [IsScalarTower K L N]
[Algebra K M] [Algebra M N] [IsScalarTower K M 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]) :
finiteGaloisTowerUnitsH2Inflation K M N ≫ finiteGaloisTowerUnitsH2Restriction K L N = 0