Module

NormSurjectiveOfTsen.lean

Nyll.AlgebraicCurves.FunctionFields.NormSurjectiveOfTsen

3 declarations indexed from sourceView source ↗

Module documentation

Surjectivity of finite-extension norms over curve function fields

The actual algebra norm is represented by a homogeneous form of degree equal to the extension dimension. Tsen applied to N(Y) - a Z^d gives a nonzero point. Anisotropy of the field norm forces Z to be nonzero, so division by Z gives norm a.

Imports3

Imported by3

theorem

norm_surjective_of_transcendental_of_finiteDimensional

L27 ↗

AlgebraicCurve.norm_surjective_of_transcendental_of_finiteDimensional

Documentation

Every element of a one-variable function field over an algebraically closed field is a norm from each of its finite field extensions.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve

Lean source · statement

theorem norm_surjective_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] :
    Function.Surjective (Algebra.norm F : E →* F)

theorem

exists_separating_transcendental_over_finite_extension

L77 ↗

AlgebraicCurve.exists_separating_transcendental_over_finite_extension

Documentation

A finite extension of a one-variable function field has an actual separating transcendental parameter.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve

Lean source · statement

theorem exists_separating_transcendental_over_finite_extension
    (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)
    (L : Type*) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
    [FiniteDimensional F L] :
    ∃ y : L, Transcendental K y ∧
      FiniteDimensional (IntermediateField.adjoin K ({y} : Set L)) L ∧
      Algebra.IsSeparable (IntermediateField.adjoin K ({y} : Set L)) L

theorem

norm_surjective_over_finite_extension

L98 ↗

AlgebraicCurve.norm_surjective_over_finite_extension

Documentation

Norm surjectivity is preserved after a finite extension of the curve function field. The separating parameter is obtained from the existing perfect-field theorem.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve

Lean source · statement

theorem norm_surjective_over_finite_extension
    (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)
    (L : Type*) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
    [FiniteDimensional F L]
    (E : Type*) [Field E] [Algebra L E] [FiniteDimensional L E] :
    Function.Surjective (Algebra.norm L : E →* L)

Module documentation

Surjectivity of finite-extension norms over curve function fields

Declarations

norm_surjective_of_transcendental_of_finiteDimensional

exists_separating_transcendental_over_finite_extension

norm_surjective_over_finite_extension