Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionGenusDegree

Genus and extension degree under exact constant extension #

This file records two numerical consequences needed to compare a function field with an exact finite extension of its constants. First, cotrace canonicality identifies the total finite-and-infinite trace-different degree with the Riemann--Hurwitz expression. Second, extending the constants from C to S preserves the degree over the corresponding rational function field.

@[instance_reducible]

noncomputable def BGS.HasseWeil.genusDegreeFintype (K : Type u_1) [Finite K] :

A finite enumeration of K used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.genusDegreeFintype K = Fintype.ofFinite K

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.genusDegreeDecidableEq (K : Type u_1) :

Decidable equality on K used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.genusDegreeDecidableEq K = Classical.decEq K

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.genusDegreeRatFuncDecidableEq (K : Type u_1) [Field K] :

DecidableEq (RatFunc K)

Decidable equality on (RatFunc K) used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.genusDegreeRatFuncDecidableEq K = Classical.decEq (RatFunc K)

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.genusDegreeConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

The algebra structure from K to L used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.genusDegreeConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

Instances For

theorem BGS.HasseWeil.genusDegreeConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

IsScalarTower K (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.genusDegreePolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.genusDegreePolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

Instances For

theorem BGS.HasseWeil.genusDegreePolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.HasseWeil.genusDegreeConstantPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

IsScalarTower K (Polynomial K) L

theorem BGS.HasseWeil.finiteExtension_totalDifferentDegree_eq_two_finrank_add_two_genus_sub_two (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] :

↑(CorvajaZannier.finiteExtensionFiniteDifferentDegree K L ⋯) + ↑(CorvajaZannier.infinityDifferentDegree K L) = 2 * ↑(Module.finrank (RatFunc K) L) + 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2

Cotrace canonicality gives the Riemann--Hurwitz equality for the weighted finite and infinite trace-different degrees.

theorem BGS.HasseWeil.finiteExtension_totalDifferentDegree_eq_two_finrank_add_two_genus_sub_two_intrinsic (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] :

↑(CorvajaZannier.finiteExtensionFiniteDifferentDegree K L ⋯) + ↑(CorvajaZannier.infinityDifferentDegree K L) = 2 * ↑(Module.finrank (RatFunc K) L) + 2 * ↑(MarkoffRiemannRoch.FunctionField.genus K L) - 2

The same Riemann--Hurwitz identity stated with the intrinsic genus. This form no longer remembers which compatible polynomial chart was installed.

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibleGenusDegreeFintype (K : Type u_1) [Finite K] :

A finite enumeration of K used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.compatibleGenusDegreeFintype K = Fintype.ofFinite K

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibleGenusDegreeDecidableEq (K : Type u_1) :

Decidable equality on K used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.compatibleGenusDegreeDecidableEq K = Classical.decEq K

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibleGenusDegreeRatFuncDecidableEq (K : Type u_1) [Field K] :

DecidableEq (RatFunc K)

Decidable equality on (RatFunc K) used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.compatibleGenusDegreeRatFuncDecidableEq K = Classical.decEq (RatFunc K)

Instances For

@[instance_reducible]

noncomputable def BGS.HasseWeil.compatibleGenusDegreeConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

The algebra structure from K to L used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.compatibleGenusDegreeConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

Instances For

theorem BGS.HasseWeil.compatibleGenusDegreeConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.finiteExtension_totalDifferentDegree_eq_two_finrank_add_two_genus_sub_two_of_compatibleChart (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra (Polynomial K) L] [IsScalarTower (Polynomial K) (RatFunc K) L] [IsScalarTower K (Polynomial K) L] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] :

↑(CorvajaZannier.finiteExtensionFiniteDifferentDegree K L ⋯) + ↑(CorvajaZannier.infinityDifferentDegree K L) = 2 * ↑(Module.finrank (RatFunc K) L) + 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2

Riemann--Hurwitz for any polynomial chart whose action is compatible with the fixed rational-function-field action. This is the same statement as finiteExtension_totalDifferentDegree_eq_two_finrank_add_two_genus_sub_two, but it keeps an explicitly installed chart instead of replacing it by the induced one.

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionGenusConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :

The algebra structure from C to N used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.exactConstantExtensionGenusConstantAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap C (RatFunc C))).toAlgebra

Instances For

theorem BGS.HasseWeil.exactConstantExtension_extended_algebraicClosure_eq_bot (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite C] [Finite S] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) :

let L := ExactConstantExtension C N S; algebraicClosure S L = ⊥

Exactness of the extended constants for the constant algebra induced by the canonical S(X)-algebra structure on the exact constant extension.

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionDegreeConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :

The algebra structure from C to N used in the exact constant extension genus degree construction.

Equations

BGS.HasseWeil.exactConstantExtensionDegreeConstantAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap C (RatFunc C))).toAlgebra

Instances For

theorem BGS.HasseWeil.exactConstantExtension_finrank_over_extendedRatFunc_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) :

let L := ExactConstantExtension C N S; Module.finrank (RatFunc S) L = Module.finrank (RatFunc C) N

Exact finite extension of the constants preserves the function-field degree: [S ⊗_C N : S(X)] = [N : C(X)].