Module

FiniteKummerCyclicFactorSet.lean

Nyll.GaloisCohomology.Kummer.FiniteKummerCyclicFactorSet

10 declarations indexed from sourceView source ↗

Module documentation

Cyclic factor sets for finite Kummer cup products

Constructs carry cocycles from the negative Kummer character and compares them with cup-product classes and factor sets inflated from cyclic quotients.

Imports2

Imported by2

def

negativeCharacterCarryTwoCocycle

L31 ↗

ClassFieldTower.Martinet.Shafarevich.negativeCharacterCarryTwoCocycle

Documentation

The positive carry cocycle associated to the standard representatives of the negative of a Kummer character.

Source context 7 commands

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

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

Lean source · statement

def negativeCharacterCarryTwoCocycle
    (psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(M/K)))
    (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a) :
    groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K M)

theorem

negativeCharacterCarryTwoCocycle_apply

L72 ↗

ClassFieldTower.Martinet.Shafarevich.negativeCharacterCarryTwoCocycle_apply

Source context 7 commands

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

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

Lean source · statement

theorem negativeCharacterCarryTwoCocycle_apply
    (psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(M/K)))
    (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a)
    (sigma tau : Gal(M/K)) :
    negativeCharacterCarryTwoCocycle K M p psi a ha (sigma, tau) =
      Cohomology.zmodCarry
        (-psi (Additive.ofMul sigma))
        (-psi (Additive.ofMul tau)) • a

def

inflatedFiniteCyclicCarryTwoCocycle

L87 ↗

ClassFieldTower.Martinet.Shafarevich.inflatedFiniteCyclicCarryTwoCocycle

Documentation

The positive cyclic carry cocycle pulled back along a finite quotient.

Source context 7 commands

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

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

Lean source · statement

def inflatedFiniteCyclicCarryTwoCocycle
    {G : Type} [CommGroup G] [Fintype G]
    (q : Gal(M/K) →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a) :
    groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K M)

theorem

inflatedFiniteCyclicCarryTwoCocycle_apply

L109 ↗

ClassFieldTower.Martinet.Shafarevich.inflatedFiniteCyclicCarryTwoCocycle_apply

Source context 7 commands

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

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

Lean source · statement

theorem inflatedFiniteCyclicCarryTwoCocycle_apply
    {G : Type} [CommGroup G] [Fintype G]
    (q : Gal(M/K) →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a)
    (sigma tau : Gal(M/K)) :
    inflatedFiniteCyclicCarryTwoCocycle K M q g hg a ha (sigma, tau) =
      Cohomology.finiteCyclicCarry g hg (q sigma) (q tau) • a

theorem

negativeCharacterCarryTwoCocycle_eq_inflated

L125 ↗

ClassFieldTower.Martinet.Shafarevich.negativeCharacterCarryTwoCocycle_eq_inflated

Documentation

A quotient whose generator coordinate is the negative Kummer character has the same pulled-back carry cocycle. The value-coordinate formulation avoids any transport between definitionally different ZMod moduli.

Source context 7 commands

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

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

Lean source · statement

theorem negativeCharacterCarryTwoCocycle_eq_inflated
    {G : Type} [CommGroup G] [Fintype G]
    (psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(M/K)))
    (q : Gal(M/K) →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (hcard : Nat.card G = (p : ℕ))
    (hcoord : ∀ sigma : Gal(M/K),
      (Cohomology.finiteCyclicGeneratorCoordinate g hg (q sigma)).val =
        (-psi (Additive.ofMul sigma)).val)
    (a : Rep.ofAlgebraAutOnUnits K M)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a) :
    negativeCharacterCarryTwoCocycle K M p psi a ha =
      inflatedFiniteCyclicCarryTwoCocycle K M q g hg a ha

def

finiteKummerCoefficientElement

L153 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientElement

Documentation

The chosen-root coefficient as an element of the representation's exact underlying type.

Source context 7 commands

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

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

Lean source · statement

def finiteKummerCoefficientElement
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : ULift (ZMod (p : ℕ))) : Rep.ofAlgebraAutOnUnits K M

theorem

finiteKummerCoefficientElement_apply

L159 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientElement_apply

Source context 7 commands

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

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

Lean source · statement

theorem finiteKummerCoefficientElement_apply
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : ULift (ZMod (p : ℕ))) :
    finiteKummerCoefficientElement K M p hmu z =
      finiteKummerCoefficientAddHom K M p hmu z

theorem

coefficient_cup_eq_neg_coordinate_smul

L166 ↗

ClassFieldTower.Martinet.Shafarevich.coefficient_cup_eq_neg_coordinate_smul

Source context 7 commands

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

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

Lean source · statement

theorem coefficient_cup_eq_neg_coordinate_smul
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (x y : ZMod (p : ℕ)) :
    finiteKummerCoefficientElement K M p hmu (ULift.up (x * y)) =
      -((-y).val •
        finiteKummerCoefficientElement K M p hmu (ULift.up x))

theorem

finiteKummerCup_H2pi_eq_negativeCharacterCarry

L192 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCup_H2pi_eq_negativeCharacterCarry

Documentation

The coefficient-changed cup factor set equals the positive carry factor set in H². The explicit cobounding cochain is sigma ↦ -(-psi sigma).val • alpha.

The action hypothesis is the Kummer equation sigma(alpha) = zeta^(chi sigma) * alpha, written additively; the power hypothesis is alpha^p = a.

Source context 7 commands

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

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

Lean source · statement

theorem finiteKummerCup_H2pi_eq_negativeCharacterCarry
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(M/K)))
    (alpha a : Rep.ofAlgebraAutOnUnits K M)
    (halpha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma alpha =
        (finiteKummerCoefficientRepHom K M p hmu).hom
          (ULift.up (chi (Additive.ofMul sigma))) + alpha)
    (hpow : (p : ℕ) • alpha = a)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a) :
    groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
        (finiteKummerCupCoefficientTwoCocycle K M p hmu chi psi) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
        (negativeCharacterCarryTwoCocycle K M p psi a ha)

theorem

finiteKummerCup_H2pi_eq_inflatedFiniteCyclicCarry

L268 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCup_H2pi_eq_inflatedFiniteCyclicCarry

Documentation

Factor-set descent along a cyclic quotient. Its only quotient-specific input is the pointwise identification of the normalized generator coordinate with the negative Kummer character.

Source context 7 commands

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

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

Lean source · statement

theorem finiteKummerCup_H2pi_eq_inflatedFiniteCyclicCarry
    {G : Type} [CommGroup G] [Fintype G]
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (chi psi : ContinuousH1ZMod (p := (p : ℕ)) (G := Gal(M/K)))
    (q : Gal(M/K) →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (hcard : Nat.card G = (p : ℕ))
    (hcoord : ∀ sigma : Gal(M/K),
      (Cohomology.finiteCyclicGeneratorCoordinate g hg (q sigma)).val =
        (-psi (Additive.ofMul sigma)).val)
    (alpha a : Rep.ofAlgebraAutOnUnits K M)
    (halpha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma alpha =
        (finiteKummerCoefficientRepHom K M p hmu).hom
          (ULift.up (chi (Additive.ofMul sigma))) + alpha)
    (hpow : (p : ℕ) • alpha = a)
    (ha : ∀ sigma : Gal(M/K),
      (Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a) :
    groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
        (finiteKummerCupCoefficientTwoCocycle K M p hmu chi psi) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
        (inflatedFiniteCyclicCarryTwoCocycle K M q g hg a ha)

Module documentation

Cyclic factor sets for finite Kummer cup products

Declarations