Module

FiniteKummerAbsoluteLift.lean

Nyll.GaloisCohomology.Kummer.FiniteKummerAbsoluteLift

5 declarations indexed from sourceView source ↗

Module documentation

Absolute lifts of finite Kummer cocycle extensions

A finite field-unit primitive is first corrected, by the proved Hilbert-90 construction, to a continuous natural mu_p primitive. The existing primitive-root trivialization then turns it into a lifted ZMod p primitive. Its negative coefficient coordinate gives an explicit continuous homomorphism into the finite cocycle extension.

The final endpoint accepts exactly the ordinary field-unit boundary supplied by the supported-idele and degree-two injection results. The normalized cocycle is packaged here as an ordinary two-cocycle; no unproved comparison or existence hypothesis is introduced. No new instances are introduced.

Imports3

Imported by3

def

absoluteFiniteGaloisRestriction

L42 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteFiniteGaloisRestriction

Documentation

Continuous restriction from the absolute Galois group to an actual finite Galois intermediate field.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP FreeProPH2Cocycle
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
omit [CharZero K] in

Lean source · full declaration

def absoluteFiniteGaloisRestriction :
    Field.absoluteGaloisGroup K →ₜ* Gal(E/K) where
  toMonoidHom := (AlgEquiv.restrictNormalHom E.toIntermediateField).comp
    (absoluteGaloisGroupContinuousMulEquiv K).toMonoidHom
  continuous_toFun :=
    (InfiniteGalois.restrictNormalHom_continuous E.toIntermediateField).comp
      (absoluteGaloisGroupContinuousMulEquiv K).continuous

theorem

exists_absoluteZModP_primitive_of_finiteKummerUnit_boundary

L52 ↗

ClassFieldTower.Martinet.Shafarevich.exists_absoluteZModP_primitive_of_finiteKummerUnit_boundary

Documentation

A finite unit primitive yields a continuous lifted ZMod p primitive when the base contains the supplied primitive root.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP FreeProPH2Cocycle
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · statement

theorem exists_absoluteZModP_primitive_of_finiteKummerUnit_boundary
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (c : Gal(E/K) → Gal(E/K) → ULift.{0} (ZMod (p : ℕ)))
    (b : Gal(E/K) → Eˣ)
    (hb : ∀ s t : Gal(E/K),
      Units.map s (b t) * b s / b (s * t) =
        (finiteKummerCoefficientAddHom K E p hmu (c s t)).toMul) :
    ∃ a : C(Field.absoluteGaloisGroup K, ULift.{0} (ZMod (p : ℕ))),
      ∀ s t, a t + a s - a (s * t) =
        c (absoluteFiniteGaloisRestriction K E s)
          (absoluteFiniteGaloisRestriction K E t)

theorem

exists_absoluteLift_of_finiteKummerUnit_boundary

L100 ↗

ClassFieldTower.Martinet.Shafarevich.exists_absoluteLift_of_finiteKummerUnit_boundary

Documentation

The corrected primitive gives a genuine continuous lift into the cocycle extension, with the prescribed finite restriction as projection.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP FreeProPH2Cocycle
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · statement

theorem exists_absoluteLift_of_finiteKummerUnit_boundary
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : Cohomology.trivialZModPCocyclesLifted (p : ℕ) Gal(E/K) 2)
    (b : Gal(E/K) → Eˣ)
    (hb : ∀ s t : Gal(E/K),
      Units.map s (b t) * b s / b (s * t) =
        (finiteKummerCoefficientAddHom K E p hmu
          (normalizedCocycle z s t)).toMul) :
    ∃ s : Field.absoluteGaloisGroup K →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s =
        absoluteFiniteGaloisRestriction K E

def

normalizedFiniteKummerTwoCocycle

L140 ↗

ClassFieldTower.Martinet.Shafarevich.normalizedFiniteKummerTwoCocycle

Documentation

The normalized continuous cocycle, viewed in the ordinary pair-shaped degree-two cochain model used by finite Kummer coefficient change.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP FreeProPH2Cocycle
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
omit [CharZero K] in

Lean source · statement

def normalizedFiniteKummerTwoCocycle
    (z : Cohomology.trivialZModPCocyclesLifted (p : ℕ) Gal(E/K) 2) :
    groupCohomology.cocycles₂
      (Rep.trivial ℤ Gal(E/K) (ULift.{0} (ZMod (p : ℕ))))

theorem

exists_absoluteLift_of_finiteKummerTwoCocycle_boundary

L154 ↗

ClassFieldTower.Martinet.Shafarevich.exists_absoluteLift_of_finiteKummerTwoCocycle_boundary

Documentation

A boundary in the actual field-unit representation supplies the continuous absolute lift of the original central cocycle extension.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP FreeProPH2Cocycle
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · statement

theorem exists_absoluteLift_of_finiteKummerTwoCocycle_boundary
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : Cohomology.trivialZModPCocyclesLifted (p : ℕ) Gal(E/K) 2)
    (b : Gal(E/K) → Additive Eˣ)
    (hb : (groupCohomology.d₁₂ (Rep.ofAlgebraAutOnUnits K E)).hom b =
      (groupCohomology.mapCocycles₂ (MonoidHom.id Gal(E/K))
        (finiteKummerCoefficientRepHom K E p hmu)
        (normalizedFiniteKummerTwoCocycle K p E z)).1) :
    ∃ s : Field.absoluteGaloisGroup K →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s =
        absoluteFiniteGaloisRestriction K E

Module documentation

Absolute lifts of finite Kummer cocycle extensions

Declarations

absoluteFiniteGaloisRestriction

exists_absoluteZModP_primitive_of_finiteKummerUnit_boundary

exists_absoluteLift_of_finiteKummerUnit_boundary

normalizedFiniteKummerTwoCocycle

exists_absoluteLift_of_finiteKummerTwoCocycle_boundary