Integral models along an extension of valued fields

For a compatible extension L/K of valued fields (ValuativeExtension K L), the valuation ring of K maps into that of L compatibly with K → L. So WeierstrassCurve.IsIntegral.baseChange applies: an equation integral over the valuation ring of K has a base change to L integral over the valuation ring of L. This is what gives the points over L of such a base change a reduction, and a subgroup E₀(L) of points with nonsingular reduction.

Main results

• WeierstrassCurve.isIntegral_valuationSubring: integrality over 𝒪[K] also supplies integrality over the valuation subring, as used by the valuation reduction API.
• WeierstrassCurve.isIntegral_valuationSubring_baseChange: along a compatible extension L/K of valued fields, an equation integral over the valuation ring of K stays integral over that of L.
• WeierstrassCurve.integralModel_valuationSubring_maximalPrime: for a nonarchimedean local field L, the same holds over the valuation ring of the adic valuation of the maximal ideal TauCeti.maximalPrime L of 𝒪[L], where the integral model of the base change is the image of the integral model over the valuation ring of K.

instance WeierstrassCurve.isIntegral_valuationSubring {K : Type u_1} [Field K] [ValuativeRel K] (W : WeierstrassCurve K) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] : IsIntegral (↥(ValuativeRel.valuation K).valuationSubring) W

An equation integral over 𝒪[K] is integral over the valuation subring of K.

instance WeierstrassCurve.isIntegral_valuationSubring_baseChange {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] (W : WeierstrassCurve K) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] : IsIntegral (↥(ValuativeRel.valuation L).valuationSubring) (W.baseChange L)

Integrality along an extension of valued fields. If L/K is a compatible extension of valued fields, the base change to L of an equation with coefficients in the valuation ring of K has coefficients in the valuation ring of L, so its points over L have a reduction and a subgroup E₀(L) of points with nonsingular reduction.

The statements over the fraction field of a Dedekind domain apply over a local field L at the maximal ideal TauCeti.maximalPrime L of 𝒪[L]. The valuation ring of its adic valuation is 𝒪[L] again, and the declarations below supply the integral model of W over it.

instance WeierstrassCurve.isIntegral_valuationSubring_maximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (W : WeierstrassCurve K) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] : IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.valuation L (TauCeti.maximalPrime L)).valuationSubring) (W.baseChange L)

The base change of an equation integral over 𝒪[K] is integral over the valuation ring of the adic valuation of the maximal ideal of 𝒪[L].

theorem WeierstrassCurve.integralModel_valuationSubring_maximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (W : WeierstrassCurve K) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] : integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation L (TauCeti.maximalPrime L)).valuationSubring) (W.baseChange L) = (integralModel (↥(ValuativeRel.valuation K).integer) W).map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(IsDedekindDomain.HeightOneSpectrum.valuation L (TauCeti.maximalPrime L)).valuationSubring)

The integral model of the base change of W over the valuation ring of the adic valuation of the maximal ideal of 𝒪[L] is the image of the integral model of W over 𝒪[K].