Module

LocalClassFieldAxiom.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.LocalClassFieldAxiom

2 declarations indexed from sourceView source ↗

Module documentation

The local multiplicative group satisfies the class-field axiom

For a finite cyclic abstract tower L / K / k, the closed subgroups are replaced by their concrete fixed fields. The lower fixed field is finite over the local ground field and the upper fixed field is finite Galois over it. The finite-tower form of the local class-field-axiom theorem therefore applies. The fixed unit representation and cyclic Tate-complex comparisons then transport its two cardinality statements back to the abstract class-field-axiom predicate.

Imports4

Imported by5

theorem

galoisAmbientUnits_satisfiesClassFieldAxiom

L41 ↗

LocalClassFieldTheory.galoisAmbientUnits_satisfiesClassFieldAxiom

Documentation

The local class-field-axiom theorem, abstract class-field-axiom form.

For any Galois ambient field over a nonarchimedean local field, its ambient unit representation satisfies the abstract class-field-axiom predicate. The predicate ranges only over towers whose lower field is finite over the distinguished base, in the fixed-separable-closure model.

Source context 5 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology ClassFormation
open LocalFieldTheory
noncomputable section
open CategoryTheory

Lean source · statement

theorem galoisAmbientUnits_satisfiesClassFieldAxiom
    (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
    [ValuativeRel k] [TopologicalSpace k] [IsNonarchimedeanLocalField k] :
    SatisfiesClassFieldAxiom (galoisAmbientUnitsRep k Ω)

theorem

separableClosureUnits_isClassFormation

L147 ↗

LocalClassFieldTheory.separableClosureUnits_isClassFormation