ClassFieldTower.Martinet.Shafarevich.finiteCyclicLocalUnitsH2_torsion_natCard_le
The n-torsion of the actual unit-coefficient H² of a finite cyclic local Galois extension has at most n elements.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.ShafarevichLean source · statement
theorem finiteCyclicLocalUnitsH2_torsion_natCard_le
(K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
(g : Gal(L/K))
(hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g)
(n : ℕ) (hn : 0 < n) :
Nat.card {x : groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 // n • x = 0} ≤ n