NYLL
Module

FinitePGroupLocalUnitsH2Structure.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePGroupLocalUnitsH2Structure
5 declarations indexed from sourceView source ↗

Module documentation

Cyclic unit H² of finite local Galois p-extensions

The unramified field of the same degree supplies the auxiliary cyclic extension. Its compositum with the given field is unramified of degree equal to the ramification index. The resulting cyclicity proof transports from an actual intermediate field in the separable closure to any finite Galois p-extension.

Imports15
Imported by2

Declarations

theorem

standardUnramified_isCyclic

L42 ↗
ClassFieldTower.Martinet.Shafarevich.standardUnramified_isCyclic
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory ClassFieldTower.Cohomology LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardUnramified_isCyclic (d : ℕ) (hd : 0 < d) :
    IsCyclic Gal((localFiniteUnramifiedField K d hd)/K)
theorem

cyclic_generator_order

L50 ↗
ClassFieldTower.Martinet.Shafarevich.cyclic_generator_order
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory ClassFieldTower.Cohomology LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem cyclic_generator_order
    (M : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K M] [IsGalois K M] [IsCyclic Gal(M/K)] :
    ∃ c : groupCohomology (Rep.ofAlgebraAutOnUnits K M) 2,
      addOrderOf c = Module.finrank K M
theorem

intermediateFieldUnitsH2_isAddCyclic

L64 ↗
ClassFieldTower.Martinet.Shafarevich.intermediateFieldUnitsH2_isAddCyclic
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory ClassFieldTower.Cohomology LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem intermediateFieldUnitsH2_isAddCyclic
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (p : ℕ) [Fact p.Prime] (hP : IsPGroup p Gal(F/K)) :
    IsAddCyclic (groupCohomology (Rep.ofAlgebraAutOnUnits K F) 2)
theorem

finitePGroupLocalUnitsH2_isAddCyclic

L115 ↗
ClassFieldTower.Martinet.Shafarevich.finitePGroupLocalUnitsH2_isAddCyclic
Documentation

Unit-coefficient H² of every finite local Galois p-extension is cyclic.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory ClassFieldTower.Cohomology LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem finitePGroupLocalUnitsH2_isAddCyclic
    (p : ℕ) [Fact p.Prime] (L : Type) [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] (hP : IsPGroup p Gal(L/K)) :
    IsAddCyclic (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2)
theorem

finitePGroupLocalUnitsH2_torsion_natCard_le

L129 ↗
ClassFieldTower.Martinet.Shafarevich.finitePGroupLocalUnitsH2_torsion_natCard_le
Documentation

Positive n-torsion in local p-extension unit H² has at most n elements.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory ClassFieldTower.Cohomology LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem finitePGroupLocalUnitsH2_torsion_natCard_le
    (p : ℕ) [Fact p.Prime] (L : Type) [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] (hP : IsPGroup p Gal(L/K))
    (n : ℕ) (hn : 0 < n) :
    Nat.card {x : groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 // n • x = 0} ≤ n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.