Module

FiniteKummerCupCoefficientSquare.lean

Nyll.GaloisCohomology.Kummer.FiniteKummerCupCoefficientSquare

9 declarations indexed from sourceView source ↗

Module documentation

The finite Kummer cup-product coefficient square

For a finite Galois extension, changing the coefficients of the ordinary degree-two character cup class by a chosen primitive root is represented by applying the chosen-root homomorphism pointwise to its two-cocycle. Combining this square with the discrete continuous/ordinary comparison gives the same description for the continuous character cup.

This is only a coefficient-change statement. It neither assumes the Galois group is cyclic nor identifies the resulting class with a norm or Hilbert symbol.

Imports3

Nyll.GaloisCohomology.ProP.DiscreteH2Comparison
Nyll.GaloisCohomology.Kummer.FiniteKummerCoefficientH2
Mathlib.FieldTheory.KrullTopology

Imported by3

def

finiteKummerCupCoefficientTwoCocycle

L37 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCupCoefficientTwoCocycle

Documentation

The ordinary character cup cocycle after applying the chosen-root coefficient homomorphism pointwise.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

def finiteKummerCupCoefficientTwoCocycle
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K L)

theorem

finiteKummerCupCoefficientTwoCocycle_apply

L46 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCupCoefficientTwoCocycle_apply

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCupCoefficientTwoCocycle_apply
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K)))
    (sigma tau : Gal(L/K)) :
    finiteKummerCupCoefficientTwoCocycle K L p hmu chi psi (sigma, tau) =
      finiteKummerCoefficientAddHom K L p hmu
        (ULift.up
          (chi (Additive.ofMul sigma) * psi (Additive.ofMul tau)))

def

finiteKummerCupCoefficientCocycle

L58 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCupCoefficientCocycle

Documentation

The same coefficient-changed cup cocycle in the general Fin 2 inhomogeneous-cochain model.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

def finiteKummerCupCoefficientCocycle
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    groupCohomology.cocycles (Rep.ofAlgebraAutOnUnits K L) 2

theorem

finiteKummerCupCoefficientCocycle_apply

L70 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCupCoefficientCocycle_apply

Documentation

In the general inhomogeneous-cochain model, the coefficient-changed cup cocycle is obtained by applying the chosen-root map pointwise.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCupCoefficientCocycle_apply
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K)))
    (x : Fin 2 → Gal(L/K)) :
    groupCohomology.iCocycles (Rep.ofAlgebraAutOnUnits K L) 2
        (finiteKummerCupCoefficientCocycle K L p hmu chi psi) x =
      finiteKummerCoefficientAddHom K L p hmu
        (groupCohomology.iCocycles
          (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2
          ((groupCohomology.isoCocycles₂
            (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ))))).inv
            (Cohomology.ordinaryH1CupTwoCocycle chi psi)) x)

theorem

finiteKummerCupCoefficientCocycle_isoCocycles₂_hom

L86 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCupCoefficientCocycle_isoCocycles₂_hom

Documentation

The general and pair-shaped presentations of the coefficient-changed cup cocycle agree.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCupCoefficientCocycle_isoCocycles₂_hom
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    (groupCohomology.isoCocycles₂ (Rep.ofAlgebraAutOnUnits K L)).hom
        (finiteKummerCupCoefficientCocycle K L p hmu chi psi) =
      finiteKummerCupCoefficientTwoCocycle K L p hmu chi psi

theorem

finiteKummerCoefficientH2Map_H2π

L98 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_H2π

Documentation

Naturality of H²π for the chosen-root coefficient morphism.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientH2Map_H2π
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : groupCohomology.cocycles₂
      (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ))))) :
    finiteKummerCoefficientH2Map K L p hmu
        (groupCohomology.H2π
          (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) z) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
        (groupCohomology.mapCocycles₂ (MonoidHom.id (Gal(L/K)))
          (finiteKummerCoefficientRepHom K L p hmu) z)

theorem

finiteKummerCoefficientH2Map_ordinaryH1CupClass_quotient

L119 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_ordinaryH1CupClass_quotient

Documentation

The quotient-model version of the ordinary coefficient square.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientH2Map_ordinaryH1CupClass_quotient
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    finiteKummerCoefficientH2Map K L p hmu
        (Cohomology.ordinaryH1CupClass chi psi) =
      groupCohomology.π (Rep.ofAlgebraAutOnUnits K L) 2
        (finiteKummerCupCoefficientCocycle K L p hmu chi psi)

theorem

finiteKummerCoefficientH2Map_ordinaryH1CupClass

L137 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_ordinaryH1CupClass

Documentation

The chosen-root coefficient map sends the ordinary character cup class to the class of the pointwise chosen-root cup cocycle.

Source context 6 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientH2Map_ordinaryH1CupClass
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    finiteKummerCoefficientH2Map K L p hmu
        (Cohomology.ordinaryH1CupClass chi psi) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
        (finiteKummerCupCoefficientTwoCocycle K L p hmu chi psi)

theorem

finiteKummerCoefficientH2Map_discreteContinuousH1Cup

L154 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_discreteContinuousH1Cup

Documentation

For a finite Galois extension, the discrete comparison followed by the chosen-root coefficient map sends the continuous character cup to the class of the pointwise chosen-root ordinary cup cocycle.

Source context 8 commands

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

open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (p : ℕ+)
section FiniteGalois
variable [FiniteDimensional K L]

Lean source · statement

theorem finiteKummerCoefficientH2Map_discreteContinuousH1Cup
    [IsGalois K L]
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(L/K))) :
    finiteKummerCoefficientH2Map K L p hmu
        (Cohomology.discreteContinuousH2AddEquiv
          (Cohomology.continuousH1CupProductLifted chi psi)) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
        (finiteKummerCupCoefficientTwoCocycle K L p hmu chi psi)

Module documentation

The finite Kummer cup-product coefficient square

Declarations