Genus invariance under exact constant extension

Equality of the presented total-different multiplicities preserves the total different degree. Riemann--Hurwitz and preservation of the rational-function extension degree then identify the two chart genera.

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactConstantGenusInvarianceRatFuncDecidableEq (K : Type u_4) [Field K] : DecidableEq (RatFunc K)

Classical equality on rational functions over the enlarged constants for genus invariance.

Equations

• BGS.HasseWeil.exactConstantGenusInvarianceRatFuncDecidableEq K = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants K

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.exactConstantGenusInvarianceBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.exactConstantGenusInvarianceBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

@[instance_reducible]

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

The polynomial algebra on the original extension field used to compare genera.

Equations

• BGS.HasseWeil.exactConstantGenusInvarianceBasePolynomialAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap (Polynomial C) (RatFunc C))).toAlgebra

theorem BGS.HasseWeil.exactConstantGenusInvarianceBasePolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower (Polynomial C) (RatFunc C) N

theorem BGS.HasseWeil.exactConstantGenusInvarianceBaseConstantPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (Polynomial C) N

theorem BGS.HasseWeil.exactConstantExtension_chart_genus_eq_of_presentedMultiplicity (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : let E := ExactConstantExtension C N S; let extendedConstantAlgebra := ((algebraMap (RatFunc S) E).comp (algebraMap S (RatFunc S))).toAlgebra; let tensorConstantAlgebra := Algebra.TensorProduct.leftAlgebra; have hconstantMap := ⋯; have htensorPolynomialMap := ⋯; (∀ (q : ExactConstantExtensionPresentedPlace C S N), (finiteExtensionTotalDifferentEffectiveDivisor S E) ((exactConstantExtensionPresentedUpstairsPlaceEquiv C S N hExact) q) = (finiteExtensionTotalDifferentEffectiveDivisor C N) (exactConstantExtensionPresentedDownstairsPlace C S N hExact q)) → MarkoffRiemannRoch.FunctionField.Chart.genus S E = MarkoffRiemannRoch.FunctionField.Chart.genus C N

Exact finite extension of constants preserves chart genus once the pointwise total-different multiplicity compatibility is known.