Module

PGroupH2OfTsen.lean

Nyll.AlgebraicCurves.FunctionFields.PGroupH2OfTsen

1 declaration indexed from sourceView source ↗

Module documentation

Unit H² of finite Galois p-extensions of curve function fields

A central prime-order subgroup supplies an actual intermediate field. Tsen kills the cyclic upper extension, induction kills the lower extension, and the existing unit H² inflation-restriction exactness kills the original class.

Imports5

Nyll.AlgebraicCurves.FunctionFields.NormSurjectiveOfTsen
Nyll.GaloisCohomology.Kummer.FiniteCyclicUnitsH2NormSurjective
Nyll.GaloisCohomology.Kummer.FiniteGaloisTowerUnitsH2
Nyll.GaloisCohomology.GroupTheory.PGroupGaloisTower
Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Imported by2

theorem

pGroupUnitsH2_eq_zero_of_transcendental_of_finiteDimensional

L27 ↗

AlgebraicCurve.pGroupUnitsH2_eq_zero_of_transcendental_of_finiteDimensional

Documentation

Actual unit-coefficient H² vanishes for finite Galois p-extensions of one-variable function fields over algebraically closed fields.

Source context 2 commands

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

open CategoryTheory
namespace AlgebraicCurve

Lean source · statement

theorem pGroupUnitsH2_eq_zero_of_transcendental_of_finiteDimensional
    (K : Type) [Field K] [IsAlgClosed 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]
    (E : Type) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E]
    (hP : IsPGroup p Gal(E/F))
    (c : groupCohomology (Rep.ofAlgebraAutOnUnits F E) 2) : c = 0

Module documentation

Unit H² of finite Galois p-extensions of curve function fields

Declarations

pGroupUnitsH2_eq_zero_of_transcendental_of_finiteDimensional