Module

GaloisH2OfTsen.lean

Nyll.AlgebraicCurves.FunctionFields.GaloisH2OfTsen

1 declaration indexed from sourceView source ↗

Module documentation

Unit H² of arbitrary finite Galois extensions of curve function fields

The Sylow fixed fields remain one-variable function fields. Their relative Galois groups are p-groups, so the previously proved vanishing applies. The finite-index trace detects vanishing in the original actual group-cohomology object.

Imports3

Imported by2

theorem

galoisUnitsH2_eq_zero_of_transcendental_of_finiteDimensional

L25 ↗

AlgebraicCurve.galoisUnitsH2_eq_zero_of_transcendental_of_finiteDimensional

Documentation

Actual unit H² vanishes for every finite Galois extension of a one-variable function field over an algebraically closed field.

Source context 2 commands

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

open CategoryTheory
namespace AlgebraicCurve

Lean source · statement

theorem galoisUnitsH2_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)
    (E : Type) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E]
    (c : groupCohomology (Rep.ofAlgebraAutOnUnits F E) 2) : c = 0

Module documentation

Unit H² of arbitrary finite Galois extensions of curve function fields

Declarations

galoisUnitsH2_eq_zero_of_transcendental_of_finiteDimensional