NYLL
Module

Hilbert90.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.Hilbert90
1 declaration indexed from sourceView source ↗

Module documentation

Hilbert 90 and negative Tate cohomology of field units

For a finite field extension with a chosen generator of its automorphism group, the cyclic comparison between first group cohomology and negative Tate cohomology transports Hilbert 90 to the statement that the latter group has cardinality one.

Imports2
Imported by3

Declarations

theorem

unitsTateHminusOne_card_eq_one

L27 ↗
LocalClassFieldTheory.unitsTateHminusOne_card_eq_one
Documentation

The i = -1 half of the local class-field-axiom theorem on the actual field-unit representation. This is Hilbert 90 transported through the cyclic H¹ ≃ H⁻¹ comparison.

Source context 3 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
Lean source · statement
theorem unitsTateHminusOne_card_eq_one
    (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (g : Gal(L/K)) (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g) :
    Nat.card (tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1)) = 1

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