Module

AbsoluteModPTwoCocycleOfTsen.lean

Nyll.AlgebraicCurves.FunctionFields.AbsoluteModPTwoCocycleOfTsen

2 declarations indexed from sourceView source ↗

Module documentation

Continuous mod-p two-cocycle primitives over curve function fields

A continuous finite-valued cocycle descends to an actual finite Galois intermediate field. Tsen supplies vanishing of its actual field-unit H² class. The existing Hilbert-90 and Kummer correction gives a continuous mod-p primitive on the absolute Galois group.

This proves an absolute-Galois statement. It does not assert the still separate comparison with higher étale cohomology of a curve.

Imports5

Nyll.AlgebraicCurves.FunctionFields.GaloisH2OfTsen
Nyll.GaloisCohomology.Kummer.FiniteKummerAbsoluteLift
Nyll.GaloisCohomology.Topology.GaloisFiniteStageFunctions
Nyll.GaloisCohomology.Topology.ContinuousCohomologyRepresentatives
Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Imported by2

theorem

exists_continuous_modP_twoCocycle_primitive_of_transcendental_of_finiteDimensional

L35 ↗

AlgebraicCurve.exists_continuous_modP_twoCocycle_primitive_of_transcendental_of_finiteDimensional

Documentation

Every continuous mod-p two-cocycle on the actual absolute Galois group of a characteristic-zero curve function field is a continuous coboundary. No finite-stage norm or vanishing hypothesis is required.

Source context 4 commands

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

open CategoryTheory
open scoped Topology
namespace AlgebraicCurve
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

theorem exists_continuous_modP_twoCocycle_primitive_of_transcendental_of_finiteDimensional
    (K : Type) [Field K] [IsAlgClosed K] [CharZero K]
    {F : Type} [Field F] [Algebra K F]
    (x : F) (hx : Transcendental K x)
    (hfin : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (p : ℕ+) [Fact (p : ℕ).Prime]
    (c : C(Field.absoluteGaloisGroup F × Field.absoluteGaloisGroup F,
      ULift.{0} (ZMod (p : ℕ))))
    (hc : ∀ s t u : Field.absoluteGaloisGroup F,
      c (s * t, u) + c (s, t) = c (t, u) + c (s, t * u)) :
    ∃ a : C(Field.absoluteGaloisGroup F, ULift.{0} (ZMod (p : ℕ))),
      ∀ s t, a t + a s - a (s * t) = c (s, t)

theorem

absoluteGalois_continuousH2_eq_zero_of_transcendental_of_finiteDimensional

L99 ↗

AlgebraicCurve.absoluteGalois_continuousH2_eq_zero_of_transcendental_of_finiteDimensional