Finite places under constant-field extension

If R → S is integral and both rings act compatibly on a common overring L, then an element of L is integral over R exactly when it is integral over S. Thus the two integral closures are canonically ring-equivalent by the identity on L.

For a plane-curve constant extension this identifies the integral closure of K[X] in the enlarged function field with the integral closure of E[X] in that same field. It therefore gives an equivalence between the finite-place types based on K(X) and E(X).

This file concerns only finite places. The valuation rings at infinity and the comparison of place degrees are separate boundaries.

def BGS.HasseWeil.integralClosureRingEquivOfIntegralTower (R : Type u_1) (S : Type u_2) (L : Type u_3) [CommRing R] [CommRing S] [CommRing L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [Algebra.IsIntegral R S] : ↥(integralClosure R L) ≃+* ↥(integralClosure S L)

Integral closures in a common overring agree after enlarging the base by an integral extension. The equivalence is the identity on the overring.

Equations

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

def BGS.HasseWeil.integralClosureAlgEquivOfIntegralTower (R : Type u_1) (S : Type u_2) (L : Type u_3) [CommRing R] [CommRing S] [CommRing L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [Algebra.IsIntegral R S] : ↥(integralClosure R L) ≃ₐ[R] ↥(integralClosure S L)

Algebra-equivalence form of the integral-closure identity.

Equations

• BGS.HasseWeil.integralClosureAlgEquivOfIntegralTower R S L = { toEquiv := (BGS.HasseWeil.integralClosureRingEquivOfIntegralTower R S L).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem BGS.HasseWeil.integralClosureRingEquivOfIntegralTower_coe (R : Type u_1) (S : Type u_2) (L : Type u_3) [CommRing R] [CommRing S] [CommRing L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [Algebra.IsIntegral R S] (x : ↥(integralClosure R L)) : ↑((integralClosureRingEquivOfIntegralTower R S L) x) = ↑x

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantFieldFinitePolynomialCoefficientAlgebra (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] : Algebra (Polynomial K) (Polynomial E)

The algebra structure from K[X] to E[X] used in the constant field finite place construction.

Equations

• BGS.HasseWeil.constantFieldFinitePolynomialCoefficientAlgebra K E = (Polynomial.mapRingHom (algebraMap K E)).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteBasePolynomialAlgebra (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the constant field finite place construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteExtensionPolynomialAlgebra (E : Type u_2) (L : Type u_3) [Field E] [Field L] [Algebra (RatFunc E) L] : Algebra (Polynomial E) L

The algebra structure from E[X] to L used in the constant field finite place construction.

Equations

• BGS.HasseWeil.finiteExtensionPolynomialAlgebra E L = ((algebraMap (RatFunc E) L).comp (algebraMap (Polynomial E) (RatFunc E))).toAlgebra

noncomputable def BGS.HasseWeil.ratFuncFiniteIntegralClosureRingEquiv (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [Algebra.IsIntegral K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) : ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L) ≃+* ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E L)

Compatible coefficient extension identifies the two finite integral closures inside the common top function field.

Equations

• BGS.HasseWeil.ratFuncFiniteIntegralClosureRingEquiv K E L hcomm = BGS.HasseWeil.integralClosureRingEquivOfIntegralTower (Polynomial K) (Polynomial E) L

noncomputable def BGS.HasseWeil.planeCurveFiniteIntegralClosureBaseChangeRingEquiv (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 hx := ⋯; have hpartialSecondE := ⋯; have hxE := ⋯; ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K (CorvajaZannier.PlaneCurveFunctionField fE)) ≃+* ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E (CorvajaZannier.PlaneCurveFunctionField fE))

The finite integral closures for a plane curve before and after constant extension are canonically ring-equivalent inside the enlarged function field.

Equations

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

noncomputable def BGS.HasseWeil.planeCurveFinitePlaceBaseChangeEquiv (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 hx := ⋯; have hpartialSecondE := ⋯; have hxE := ⋯; CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField fE) ≃ CorvajaZannier.FiniteExtensionFinitePlace E (CorvajaZannier.PlaneCurveFunctionField fE)

The identity equivalence of finite integral closures transports their height-one spectra, giving the finite-place base-change equivalence.

Equations

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