NYLL
Module

FiniteCyclicUnitsH2HasseLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicUnitsH2HasseLocalization
6 declarations indexed from sourceView source ↗

Module documentation

Hasse localization of finite-cyclic unit H²

For a cyclic extension of number fields, periodicity identifies degree-two cohomology of the unit representation with the global field-norm quotient. Composing this comparison with the concrete Hasse norm diagonal gives an injective all-place localization map. This is the cyclic global-duality input used by the Shafarevich obstruction calculation.

Imports2
Imported by1

Declarations

theorem

localNormSubgroup_eq_globalFieldNormSubgroup

L36 ↗
ClassFieldTower.Martinet.Shafarevich.localNormSubgroup_eq_globalFieldNormSubgroup
Source context 11 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
omit [NumberField K] [NumberField L] [IsGalois K L] in
Lean source · statement
theorem localNormSubgroup_eq_globalFieldNormSubgroup :
    localNormSubgroup K L = globalFieldNormSubgroup K L
def

finiteCyclicNormQuotientEquivGlobalNormQuotient

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicNormQuotientEquivGlobalNormQuotient
Documentation

The global norm quotient used by cyclic unit cohomology, identified with the source of the concrete Hasse norm diagonal.

Source context 10 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finiteCyclicNormQuotientEquivGlobalNormQuotient :
    NormQuotient K L ≃*
      Kˣ ⧸ globalFieldNormSubgroup K L
theorem

finiteCyclicNormQuotientEquivGlobalNormQuotient_normClass

L51 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicNormQuotientEquivGlobalNormQuotient_normClass
Source context 11 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
omit [NumberField K] [NumberField L] [IsGalois K L] in
Lean source · statement
theorem finiteCyclicNormQuotientEquivGlobalNormQuotient_normClass
    (a : Kˣ) :
    finiteCyclicNormQuotientEquivGlobalNormQuotient K L
        (normClass K L a) =
      QuotientGroup.mk' (globalFieldNormSubgroup K L) a
def

finiteCyclicUnitsH2HasseLocalization

L62 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2HasseLocalization
Documentation

Degree-two cyclic unit cohomology localized at all places through the concrete Hasse norm diagonal.

Source context 10 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finiteCyclicUnitsH2HasseLocalization
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 →+
      Additive
        (IdeleGroup K ⧸
          allPlaceLocalNormCondition (K := K) (L := L))
theorem

finiteCyclicUnitsH2HasseLocalization_carry_baseUnit

L77 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2HasseLocalization_carry_baseUnit
Documentation

On a normalized carry class with base-field coefficient, Hasse localization is represented by the corresponding principal idele.

Source context 10 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
theorem finiteCyclicUnitsH2HasseLocalization_carry_baseUnit
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g)
    (a : Kˣ) :
    letI := AlgEquiv.fintype K L
    let : IsCyclic (Gal(L / K)) :=
      isCyclic_of_generator g hg
    letI : CommGroup (Gal(L / K)) := IsCyclic.commGroup
    finiteCyclicUnitsH2HasseLocalization K L g hg
        (groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
          (finiteCyclicCarryTwoCocycle (Rep.ofAlgebraAutOnUnits K L)
            g hg (finiteCyclicBaseUnitFixed K L g a))) =
      Additive.ofMul
        (QuotientGroup.mk'
          (allPlaceLocalNormCondition (K := K) (L := L))
          (IdeleGroup.principalIdele K a)) := by
  dsimp only
  let := AlgEquiv.fintype K L
  let : IsCyclic (Gal(L / K)) :=
    isCyclic_of_generator g hg
  let : CommGroup (Gal(L / K)) := IsCyclic.commGroup
  apply Additive.toMul.injective
  change
    hasseNormDiagonal K L
        (finiteCyclicNormQuotientEquivGlobalNormQuotient K L
          (Additive.toMul
            ((finiteCyclicUnitsH2IsoNormQuotient K L g hg).hom
              (groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
                (finiteCyclicCarryTwoCocycle
                  (Rep.ofAlgebraAutOnUnits K L) g hg
                  (finiteCyclicBaseUnitFixed K L g a)))))) =
      QuotientGroup.mk'
        (allPlaceLocalNormCondition (K := K) (L := L))
        (IdeleGroup.principalIdele K a)
  rw [finiteCyclicUnitsH2IsoNormQuotient_carry_baseUnit]
  change
    hasseNormDiagonal K L
        (finiteCyclicNormQuotientEquivGlobalNormQuotient K L
          (normClass K L a)) = _
  rw [finiteCyclicNormQuotientEquivGlobalNormQuotient_normClass]
  exact hasseNormDiagonal_mk a
theorem

finiteCyclicUnitsH2HasseLocalization_injective

L121 ↗
ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2HasseLocalization_injective
Documentation

Hasse's norm theorem makes the cyclic unit-H² localization map injective.

Source context 10 commands

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

open CategoryTheory
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
open GlobalClassFieldTheory.ClassFieldAxiom
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem finiteCyclicUnitsH2HasseLocalization_injective
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g) :
    Function.Injective
      (finiteCyclicUnitsH2HasseLocalization K L g hg)

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