Rational-function models under constant extension

This file proves that the scalar extension of a plane-curve function field is compatible with coefficient extension of its rational-function base. With the first coordinate as separating variable, the square

K(X) → K(C)

↓ ↓

E(X) → E(C_E)

commutes exactly. The induced K(X)-algebra on E(C_E) factors both through K(C) and through E(X). For finite constant extensions it is finite and separable over K(X), so the existing exhaustive place-tower API can be applied to K(C) ⊂ E(C_E).

No fixed-point or rational-place correspondence is asserted here.

theorem BGS.HasseWeil.planeCurveCoordinateRingBaseChangeAlgEquiv_includeRight (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (a : CorvajaZannier.PlaneCurveCoordinateRing f) : (planeCurveCoordinateRingBaseChangeAlgEquiv K E f) (Algebra.TensorProduct.includeRight a) = (CorvajaZannier.planeCurveCoordinateRingMap f) a

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgHom_function (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (i : Fin 2) : (planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) (CorvajaZannier.planeCurveFunction f i) = CorvajaZannier.planeCurveFunction ((MvPolynomial.map (algebraMap K E)) f) i

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChange_ratFunc_commutes (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) [Algebra.IsAlgebraic K E] : let fE := (MvPolynomial.map (algebraMap K E)) f; have hpartialSecondE := ⋯; have hx := ⋯; have hxE := ⋯; ∀ (z : RatFunc K), (planeCurveFunctionFieldBaseChangeAlgHom K E f hf hfE) ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)) z) = (algebraMap (RatFunc E) (CorvajaZannier.PlaneCurveFunctionField fE)) ((ratFuncCoefficientAlgHom K E) z)

@[reducible]

noncomputable def BGS.HasseWeil.planeCurveFunctionFieldBaseChangeRatFuncAlgebra (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) [Algebra.IsAlgebraic K E] (hx : Transcendental K (CorvajaZannier.planeCurveFunction f 0)) : Algebra (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))

The K(X)-algebra structure on the base-changed function field obtained through the original function field.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChangeRatFunc_isScalarTower (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) [Algebra.IsAlgebraic K E] : have hx := ⋯; IsScalarTower (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChangeCoefficientRatFunc_isScalarTower (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) [Algebra.IsAlgebraic K E] : let fE := (MvPolynomial.map (algebraMap K E)) f; have hpartialSecondE := ⋯; have hx := ⋯; have hxE := ⋯; IsScalarTower (RatFunc K) (RatFunc E) (CorvajaZannier.PlaneCurveFunctionField fE)

theorem BGS.HasseWeil.finiteDimensional_planeCurveFunctionFieldBaseChange_over_ratFunc (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) [Algebra.IsAlgebraic K E] [FiniteDimensional K E] : have hx := ⋯; FiniteDimensional (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))

theorem BGS.HasseWeil.separable_planeCurveFunctionFieldBaseChange_over_ratFunc (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) [Algebra.IsAlgebraic K E] [Finite K] [Finite E] : have hx := ⋯; Algebra.IsSeparable (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))