NYLL
Module

FinitePGroupLocalUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePGroupLocalUnitsH2
3 declarations indexed from sourceView source ↗

Module documentation

Finite unit cohomology in local Galois p-extensions

Induction on the actual extension degree uses a central prime-order subgroup of the Galois group. The resulting upper extension is cyclic, so local reciprocity computes its unit H². The lower extension has smaller degree. Middle exactness then bounds the cardinality by the product of these two degrees and proves finiteness at the same time.

Imports18
Imported by2

Declarations

theorem

finite_natCard_le_mul_of_ker_le_range

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finite_natCard_le_mul_of_ker_le_range
Source context 3 commands

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

open CategoryTheory Module
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology LocalFieldTheory
Lean source · statement
theorem finite_natCard_le_mul_of_ker_le_range
    {A B C : Type*} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C]
    (f : A →+ B) (g : B →+ C) (h : g.ker ≤ f.range)
    [Finite A] [Finite C] :
    Finite B ∧ Nat.card B ≤ Nat.card A * Nat.card C
theorem

finiteCyclicLocalUnitsH2_finite_card

L62 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicLocalUnitsH2_finite_card
Source context 3 commands

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

open CategoryTheory Module
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology LocalFieldTheory
Lean source · statement
theorem finiteCyclicLocalUnitsH2_finite_card
    (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic Gal(L/K)] :
    Finite (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2) ∧
      Nat.card (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2) = finrank K L
theorem

finitePGroupLocalUnitsH2_finite_natCard_le_finrank

L79 ↗
ClassFieldTower.Martinet.Shafarevich.finitePGroupLocalUnitsH2_finite_natCard_le_finrank
Documentation

Unit-coefficient H² of a finite local Galois p-extension is finite, with cardinality at most the actual extension degree.

Source context 3 commands

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

open CategoryTheory Module
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology LocalFieldTheory
Lean source · statement
theorem finitePGroupLocalUnitsH2_finite_natCard_le_finrank
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (p : ℕ) [Fact p.Prime]
    (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (hP : IsPGroup p Gal(L/K)) :
    Finite (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2) ∧
      Nat.card (groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2) ≤ finrank K L

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