Constant extensions of plane-curve function fields

This file constructs scalar extension at both the affine coordinate-ring and function-field levels. If E / K is algebraic and the base-changed plane curve stays irreducible, then

E ⊗[K] K(C) ≃ₐ[E] E(C_E).

The proof identifies the tensor product of E with the fraction field of the coordinate ring as the fraction field of the tensor-product coordinate ring. It then transports this fraction field through the explicit base-change equivalence for the plane-curve coordinate ring. No Galois, Frobenius, place, or point-counting assertion is made here.

@[reducible, inline]

abbrev BGS.HasseWeil.TensorFraction (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : Type (max u_2 u_3)

Tensor the fraction field of A with an extension field E / K.

Equations

• BGS.HasseWeil.TensorFraction K E A = TensorProduct K E (FractionRing A)

@[reducible, inline]

abbrev BGS.HasseWeil.TensorBase (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : Type (max u_2 u_3)

Tensor A itself with an extension field E / K.

Equations

• BGS.HasseWeil.TensorBase K E A = TensorProduct K E A

@[reducible, inline]

abbrev BGS.HasseWeil.TensorBaseLocalization (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : Type (max u_2 u_3)

Localize the tensor-product base ring at the images of the nonzero elements of A.

Equations

• BGS.HasseWeil.TensorBaseLocalization K E A = Localization (Submonoid.map Algebra.TensorProduct.includeRight (nonZeroDivisors A))

@[instance_reducible]

noncomputable instance BGS.HasseWeil.tensorBaseTensorFractionAlgebra (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : Algebra (TensorBase K E A) (TensorFraction K E A)

Equations

• BGS.HasseWeil.tensorBaseTensorFractionAlgebra K E A = (Algebra.TensorProduct.map (AlgHom.id K E) (IsScalarTower.toAlgHom K A (FractionRing A))).toAlgebra

theorem BGS.HasseWeil.tensorBaseTensorFraction_algebraMap_tmul (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] (e : E) (a : A) : (algebraMap (TensorBase K E A) (TensorFraction K E A)) (e ⊗ₜ[K] a) = e ⊗ₜ[K] (algebraMap A (FractionRing A)) a

instance BGS.HasseWeil.tensorBaseTensorFractionScalarTower (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : IsScalarTower E (TensorBase K E A) (TensorFraction K E A)

noncomputable def BGS.HasseWeil.tensorFractionLocalizationEquiv (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : TensorFraction K E A ≃ₐ[E] TensorBaseLocalization K E A

Tensoring the fraction field agrees with localizing the tensor-product base ring at the nonzero elements coming from A.

Equations

• BGS.HasseWeil.tensorFractionLocalizationEquiv K E A = IsLocalization.tensorProductEquivOfMapIncludeRight K E (nonZeroDivisors A) (FractionRing A) (BGS.HasseWeil.TensorBaseLocalization K E A)

theorem BGS.HasseWeil.tensorFractionLocalizationEquiv_algebraMap (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] (z : TensorBase K E A) : (tensorFractionLocalizationEquiv K E A) ((algebraMap (TensorBase K E A) (TensorFraction K E A)) z) = (algebraMap (TensorBase K E A) (TensorBaseLocalization K E A)) z

theorem BGS.HasseWeil.tensorFractionIsDomain (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] [IsDomain A] [IsDomain (TensorBase K E A)] : IsDomain (TensorFraction K E A)

@[instance_reducible]

noncomputable def BGS.HasseWeil.tensorFractionField (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] [IsDomain A] [IsDomain (TensorBase K E A)] [Algebra.IsAlgebraic K E] : Field (TensorFraction K E A)

The fraction-field structure on the tensor product after algebraic constant extension.

Equations

• BGS.HasseWeil.tensorFractionField K E A = ⋯.toField

theorem BGS.HasseWeil.tensorBaseTensorFractionFaithfulSMul (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] : FaithfulSMul (TensorBase K E A) (TensorFraction K E A)

theorem BGS.HasseWeil.tensorFraction_isFractionRing (K : Type u_1) (E : Type u_2) (A : Type u_3) [Field K] [Field E] [CommRing A] [Algebra K E] [Algebra K A] [IsDomain A] [IsDomain (TensorBase K E A)] [Algebra.IsAlgebraic K E] : IsFractionRing (TensorBase K E A) (TensorFraction K E A)

If the scalar-extended base ring is a domain and E / K is algebraic, then tensoring the fraction field produces the fraction field of the scalar-extended base ring.

noncomputable def BGS.HasseWeil.planeCurveCoordinateRingBaseChangeAlgEquiv (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) : TensorProduct K E (CorvajaZannier.PlaneCurveCoordinateRing f) ≃ₐ[E] CorvajaZannier.PlaneCurveCoordinateRing ((MvPolynomial.map (algebraMap K E)) f)

Scalar extension of a plane-curve coordinate ring, as an equivalence of algebras over the enlarged constant field.

Equations

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

theorem BGS.HasseWeil.planeCurveCoordinateRingBaseChange_isDomain (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) : IsDomain (TensorProduct K E (CorvajaZannier.PlaneCurveCoordinateRing f))

If the base-changed equation is irreducible, then its tensor-product coordinate ring is a domain.

noncomputable def BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgEquiv (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] : TensorProduct K E (CorvajaZannier.PlaneCurveFunctionField f) ≃ₐ[E] CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f)

Constant extension commutes with passing from an irreducible plane-curve coordinate ring to its function field.

Equations

• BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgEquiv K E f hf hfE = IsFractionRing.algEquivOfAlgEquiv (BGS.HasseWeil.planeCurveCoordinateRingBaseChangeAlgEquiv K E f)

theorem BGS.HasseWeil.planeCurveFunctionFieldBaseChangeAlgEquiv_tmul_one (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] (e : E) : (planeCurveFunctionFieldBaseChangeAlgEquiv K E f hf hfE) (e ⊗ₜ[K] 1) = (algebraMap E (CorvajaZannier.PlaneCurveFunctionField ((MvPolynomial.map (algebraMap K E)) f))) e