Module

FiniteCyclicUnitsH2PeriodicEvaluation.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicUnitsH2PeriodicEvaluation

8 declarations indexed from sourceView source ↗

Module documentation

Evaluating the finite-cyclic periodic unit class

For a finite cyclic Galois extension, a unit fixed by the chosen generator is fixed by the whole Galois group. This file evaluates its class in the periodic degree-two model through the existing comparison with degree-zero Tate cohomology and the field norm quotient.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicLocalUnitsH2

Imported by2

def

finiteCyclicGeneratorFixedUnitInvariant

L29 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicGeneratorFixedUnitInvariant

Documentation

A unit fixed by a generator, regarded canonically as a Galois-invariant unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicGeneratorFixedUnitInvariant
    (K L : Type) [Field K] [Field L] [Algebra K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    unitsInvariantSubmodule K L

def

finiteCyclicGeneratorFixedBaseUnit

L46 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicGeneratorFixedBaseUnit

Documentation

The base-field unit canonically represented by a generator-fixed unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicGeneratorFixedBaseUnit
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) : Kˣ

def

finiteCyclicUnitsH2PeriodicClass

L58 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2PeriodicClass

Documentation

The positive-even periodic class represented by a generator-fixed unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicUnitsH2PeriodicClass
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2

def

finiteCyclicUnitsTateHZeroPeriodicClass

L83 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsTateHZeroPeriodicClass

Documentation

The Tate degree-zero class represented by the same generator-fixed unit in the finite-cyclic periodic short complex.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicUnitsTateHZeroPeriodicClass
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0

theorem

finiteCyclicUnitsH0Arithmetic_mk

L108 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH0Arithmetic_mk

Documentation

The arithmetic part of the unit Tate comparison sends an invariant-unit quotient representative to the norm class of the corresponding base unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

theorem finiteCyclicUnitsH0Arithmetic_mk
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (x : unitsInvariantSubmodule K L) :
    (H0TateUnitsIsoNormQuotient K L).hom
        ((tateUnitsH0IsoInvariantsQuotient K L).inv
          (Submodule.Quotient.mk x)) =
      Additive.ofMul
        (normClass K L
          (Additive.toMul (invariantsUnitsAddEquivBaseUnits K L x)))

theorem

finiteCyclicUnitsTateHZeroPeriodicClass_eq

L158 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsTateHZeroPeriodicClass_eq

Documentation

The finite-cyclic periodic Tate representative is the invariant-unit quotient class of the same underlying fixed unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

theorem finiteCyclicUnitsTateHZeroPeriodicClass_eq
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    finiteCyclicUnitsTateHZeroPeriodicClass K L g hg a =
      (tateUnitsH0IsoInvariantsQuotient K L).inv
        (Submodule.Quotient.mk
          (finiteCyclicGeneratorFixedUnitInvariant K L g hg a))

theorem

H0TateUnitsIsoNormQuotient_periodicClass

L296 ↗

ClassFieldTower.Martinet.Shafarevich.H0TateUnitsIsoNormQuotient_periodicClass

Documentation

The arithmetic Tate comparison evaluates the finite-cyclic periodic representative as the norm class of its canonical base-field unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

theorem H0TateUnitsIsoNormQuotient_periodicClass
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    (H0TateUnitsIsoNormQuotient K L).hom
        (finiteCyclicUnitsTateHZeroPeriodicClass K L g hg a) =
      Additive.ofMul
        (normClass K L
          (finiteCyclicGeneratorFixedBaseUnit K L g hg a))

theorem

finiteCyclicUnitsH2IsoNormQuotient_periodicClass

L316 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2IsoNormQuotient_periodicClass

Documentation

The finite-cyclic H² ≅ Tate H⁰ ≅ Kˣ/N(Lˣ) comparison sends the periodic class of a generator-fixed unit to the norm class of its canonical base-field value.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

theorem finiteCyclicUnitsH2IsoNormQuotient_periodicClass
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ σ : Gal(L / K), σ ∈ Subgroup.zpowers g)
    (a : LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)) :
    (finiteCyclicUnitsH2IsoNormQuotient K L g hg).hom
        (finiteCyclicUnitsH2PeriodicClass K L g hg a) =
      Additive.ofMul
        (normClass K L
          (finiteCyclicGeneratorFixedBaseUnit K L g hg a))

Module documentation

Evaluating the finite-cyclic periodic unit class

Declarations