Module

FiniteExtensionClassFieldAxiom.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteExtensionClassFieldAxiom

3 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity

The local class-field-axiom theorem on finite extensions of a local field.

Mathlib's local-field predicate is topology-first, while the local class-field-axiom theorem also needs a compatible local-field structure on the finite extension. This file constructs that structure from the spectral norm. In particular, the target valuation ring is proved integral over the base valuation ring; no local-field structure on the target is assumed.

Imports6

Mathlib.SetTheory.Cardinal.Finite
Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Mathlib.Topology.Algebra.Module.FiniteDimension
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ChevalleyExtension
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ValuedTopology
Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.Main

Imported by6

structure

UnitsTateCardinalityData

L43 ↗

LocalClassFieldTheory.UnitsTateCardinalityData

Documentation

Finite-cardinality data for the two actual unit Tate groups. Bundling the H⁰ finiteness proof keeps Nat.card honest when the local-field structure on the extension is constructed inside a theorem.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open ValuationTheory
open CyclicCohomology
noncomputable section
open scoped NNReal ValuativeRel

Lean source · full declaration

structure UnitsTateCardinalityData
    (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] where
  /-- Finiteness of the degree-zero Tate cohomology group of the unit representation. -/
  finiteH0 : Finite (tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0)
  /-- The degree-zero unit Tate group has cardinality equal to the extension degree. -/
  cardH0 :
    letI := finiteH0
    Nat.card (tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0) = Module.finrank K L
  /-- The degree-minus-one unit Tate group is trivial at the level of cardinality. -/
  cardHminusOne : Nat.card (tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1)) = 1

theorem

finiteExtensionUnits_tate_card_of_generator

L57 ↗

LocalClassFieldTheory.finiteExtensionUnits_tate_card_of_generator

Documentation

The local class-field-axiom theorem for an arbitrary finite Galois extension of a nonarchimedean local field. All local-field data on the extension is constructed from the spectral norm.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open ValuationTheory
open CyclicCohomology
noncomputable section
open scoped NNReal ValuativeRel

Lean source · statement

theorem finiteExtensionUnits_tate_card_of_generator
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g) :
    UnitsTateCardinalityData K L

theorem

finiteTowerUnits_tate_card_of_generator

L180 ↗

LocalClassFieldTheory.finiteTowerUnits_tate_card_of_generator

Documentation

Tower form of the local class-field-axiom theorem. It is enough that the lower field of the cyclic extension be finite over a nonarchimedean local field; its local-field structure is again supplied by the spectral norm.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open ValuationTheory
open CyclicCohomology
noncomputable section
open scoped NNReal ValuativeRel

Lean source · statement

theorem finiteTowerUnits_tate_card_of_generator
    (k K L : Type) [Field k] [Field K] [Field L]
    [Algebra k K] [FiniteDimensional k K]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel k] [TopologicalSpace k] [IsNonarchimedeanLocalField k]
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g) :
    UnitsTateCardinalityData K L

Module documentation

Finite local reciprocity

Declarations

UnitsTateCardinalityData

finiteExtensionUnits_tate_card_of_generator

finiteTowerUnits_tate_card_of_generator