AlgebraicCurve.cyclicUnitsH2_eq_zero_of_transcendental_of_finiteDimensional
Actual unit-coefficient H² vanishes for every finite cyclic Galois extension of a one-variable function field over an algebraically closed field.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AlgebraicCurveLean source · statement
theorem cyclicUnitsH2_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)
(hsep : Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F)
(E : Type) [Field E] [Algebra F E] [FiniteDimensional F E]
[IsGalois F E] [IsCyclic Gal(E/F)]
(c : groupCohomology (Rep.ofAlgebraAutOnUnits F E) 2) : c = 0