Module

FiniteCyclicBaseUnitsH2.lean

Nyll.GaloisCohomology.Kummer.FiniteCyclicBaseUnitsH2

4 declarations indexed from sourceView source ↗

Module documentation

Base-unit representatives for cyclic field-unit H²

The inclusion of base-field units is equivariant for the trivial action. In a finite cyclic Galois extension, every H² class has a carry representative with invariant coefficient; Galois fixed-value descent makes that coefficient an actual base-field unit.

Imports15

Nyll.GaloisCohomology.ProP.FiniteCyclicH2CoefficientNorm
Nyll.GaloisCohomology.ProP.FiniteCyclicCarryCocycle
Nyll.GaloisCohomology.ProP.FiniteCyclicBarPeriodicH2Comparison
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Group.Units.Hom
Mathlib.Algebra.Module.LinearMap.Defs
Mathlib.FieldTheory.Fixed
Mathlib.FieldTheory.Galois.Basic
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.RepresentationTheory.Invariants
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Rep.Res
Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Imported by7

def

finiteGaloisBaseUnitsRepHom

L41 ↗

ClassFieldTower.Cohomology.finiteGaloisBaseUnitsRepHom

Documentation

Inclusion of base units, from the trivial action to the actual Galois action.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K M : Type) [Field K] [Field M] [Algebra K M]

Lean source · statement

def finiteGaloisBaseUnitsRepHom :
    Rep.trivial ℤ Gal(M/K) (Additive Kˣ) ⟶ Rep.ofAlgebraAutOnUnits K M

def

finiteGaloisBaseUnitsH2Map

L52 ↗

ClassFieldTower.Cohomology.finiteGaloisBaseUnitsH2Map

Documentation

The actual coefficient map on H² induced by including base-field units.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K M : Type) [Field K] [Field M] [Algebra K M]

Lean source · statement

def finiteGaloisBaseUnitsH2Map :
    groupCohomology (Rep.trivial ℤ Gal(M/K) (Additive Kˣ)) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits K M) 2

theorem

exists_baseUnit_of_fixed

L59 ↗

ClassFieldTower.Cohomology.exists_baseUnit_of_fixed

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K M : Type) [Field K] [Field M] [Algebra K M]
variable [FiniteDimensional K M] [IsGalois K M]

Lean source · statement

theorem exists_baseUnit_of_fixed (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ σ : Gal(M/K), (Rep.ofAlgebraAutOnUnits K M).ρ σ a = a) :
    ∃ b : Rep.trivial ℤ Gal(M/K) (Additive Kˣ),
      (finiteGaloisBaseUnitsRepHom K M).hom b = a

theorem

finiteCyclicBaseUnitsH2Map_surjective

L78 ↗

ClassFieldTower.Cohomology.finiteCyclicBaseUnitsH2Map_surjective

Documentation

Every actual unit-coefficient H² class in a finite cyclic Galois extension is supplied by a class with trivial base-unit coefficients.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K M : Type) [Field K] [Field M] [Algebra K M]
variable [FiniteDimensional K M] [IsGalois K M]

Lean source · statement

theorem finiteCyclicBaseUnitsH2Map_surjective [IsCyclic Gal(M/K)] :
    Function.Surjective (finiteGaloisBaseUnitsH2Map K M).hom

Module documentation

Base-unit representatives for cyclic field-unit H²

Declarations

finiteGaloisBaseUnitsRepHom

finiteGaloisBaseUnitsH2Map

exists_baseUnit_of_fixed

finiteCyclicBaseUnitsH2Map_surjective