Module

FiniteCyclicUnitsH2NormSurjective.lean

Nyll.GaloisCohomology.Kummer.FiniteCyclicUnitsH2NormSurjective

1 declaration indexed from sourceView source ↗

Module documentation

Cyclic unit H² vanishes when the actual field norm is surjective

This uses the existing periodic H² calculation and base-unit representatives. The norm hypothesis is the actual algebra norm, rather than a separate cohomology model.

Imports2

Nyll.GaloisCohomology.Kummer.FiniteCyclicBaseUnitsH2
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Imported by3

theorem

finiteCyclicUnitsH2_eq_zero_of_norm_surjective

L23 ↗

ClassFieldTower.Cohomology.finiteCyclicUnitsH2_eq_zero_of_norm_surjective

Documentation

Surjectivity of the field norm kills actual degree-two unit cohomology for a finite cyclic Galois extension.

Source context 2 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology

Lean source · statement

theorem finiteCyclicUnitsH2_eq_zero_of_norm_surjective
    (K M : Type) [Field K] [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M] [IsCyclic Gal(M/K)]
    (hN : Function.Surjective (Algebra.norm K : M →* K))
    (c : groupCohomology (Rep.ofAlgebraAutOnUnits K M) 2) : c = 0

Module documentation

Cyclic unit H² vanishes when the actual field norm is surjective

Declarations

finiteCyclicUnitsH2_eq_zero_of_norm_surjective