Nyll.AlgebraicCurves.Models.FunctionFieldModPH2

Module documentation

Actual smooth-curve function fields have vanishing absolute mod-p H²

The field is the scheme's actual function field. Smooth relative dimension one supplies its separating transcendence parameter via the existing geometric Kähler-differential calculation. Tsen and the already proved continuous-cocycle argument then give the vanishing.

This is a function-field statement, not yet the comparison with the higher étale cohomology of the curve.

theorem

functionField_absoluteGalois_continuousH2_eq_zero

L34 ↗

AlgebraicCurve.functionField_absoluteGalois_continuousH2_eq_zero

Documentation

The actual function field of an integral smooth curve over an algebraically closed characteristic-zero field has zero absolute continuous mod-p H². No rational parameter or finite-extension presentation is assumed in the statement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicCurves.Models.Proofs
open IsCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one
namespace AlgebraicCurve

Lean source · statement

theorem functionField_absoluteGalois_continuousH2_eq_zero
    (K : Type) [Field K] [IsAlgClosed K] [CharZero K]
    {C : Scheme.{0}} [IsIntegral C] (c : C ⟶ Spec (.of K))
    [SmoothOfRelativeDimension 1 c]
    (p : ℕ+) [Fact (p : ℕ).Prime]
    (v : ClassFieldTower.Cohomology.continuousCohomologyZModPLifted
      (p : ℕ) (Field.absoluteGaloisGroup C.functionField) 2) : v = 0

Module documentation

Actual smooth-curve function fields have vanishing absolute mod-p H²

Declarations

functionField_absoluteGalois_continuousH2_eq_zero