Module

FinitePGroupLocalUnitsH2Cyclic.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePGroupLocalUnitsH2Cyclic

2 declarations indexed from sourceView source ↗

Module documentation

Cyclicity of local p-extension unit H² from an unramified tower

A generator of the cyclic auxiliary field's H² inflates into the kernel of relative restriction. Middle exactness lifts it to the p-extension's H², and injectivity preserves its order. The proven cardinality bound then makes that lifted element a generator.

Imports12

Nyll.GaloisCohomology.Kummer.FiniteGaloisTowerUnitsH2
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicLocalUnitsH2
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicUnramifiedTowerH2Restriction
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePGroupLocalUnitsH2
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Group.TypeTags.Basic
Mathlib.Data.Fintype.Card
Mathlib.FieldTheory.Galois.Basic
Mathlib.GroupTheory.OrderOfElement
Mathlib.GroupTheory.PGroup
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.SetTheory.Cardinal.Finite

Imported by2

theorem

finitePGroupLocalUnitsH2_isAddCyclic_of_unramified_tower

L57 ↗

ClassFieldTower.Martinet.Shafarevich.finitePGroupLocalUnitsH2_isAddCyclic_of_unramified_tower

Documentation

An actual unramified auxiliary tower proves cyclicity of the unit H² of a finite local Galois p-extension.

Source context 7 commands

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

open CategoryTheory
open scoped ValuativeRel
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology LocalClassFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K L M N : Type)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [Field L] [Field M] [Field N]
  [Algebra K L] [Algebra L N] [Algebra K N] [IsScalarTower K L N]
  [Algebra K M] [Algebra M N] [IsScalarTower K M N]
  [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [ValuativeRel N] [TopologicalSpace N] [IsNonarchimedeanLocalField N]
  [FiniteDimensional K L] [IsGalois K L] [FiniteDimensional L N] [IsGalois K 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]
  (p : ℕ) [Fact p.Prime] (hP : IsPGroup p Gal(L/K))
  (hd : Module.finrank L N ∣ (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K])
  (hdegree : Module.finrank K L ≤ Module.finrank K M)
include hP hd hdegree

Lean source · statement

theorem finitePGroupLocalUnitsH2_isAddCyclic_of_unramified_tower :
    IsAddCyclic (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2)

theorem

finitePGroupLocalUnitsH2_torsion_natCard_le_of_unramified_tower

L93 ↗

ClassFieldTower.Martinet.Shafarevich.finitePGroupLocalUnitsH2_torsion_natCard_le_of_unramified_tower