Transporting normalization ideals to finite places

The project's finite places are height-one prime ideals in RatFuncFiniteIntegralClosure S T. Constant-extension arguments naturally produce another normalization model together with an equivalence over S[X]. This file transports height-one ideals, residue fields, residue degrees, and contractions across such an equivalence.

There is one typeclass subtlety. A canonical embedding RatFunc S → T induces an S[X]-algebra structure on T, while a geometric construction may already carry a propositionally equal polynomial algebra structure. The algebra-map bridge below turns a pointwise compatibility theorem into an equivalence with RatFuncFiniteIntegralClosure S T; it does not assume the two structures are definitionally equal.

def BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv {C : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B] (e : A ≃ₐ[C] B) : IsDedekindDomain.HeightOneSpectrum A ≃ IsDedekindDomain.HeightOneSpectrum B

An algebra equivalence transports height-one prime ideals.

Equations

• BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv e = IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e.toRingEquiv

@[simp]

theorem BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv_asIdeal {C : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B] (e : A ≃ₐ[C] B) (q : IsDedekindDomain.HeightOneSpectrum A) : ((heightOneSpectrumEquivOfAlgEquiv e) q).asIdeal = Ideal.comap e.symm q.asIdeal

noncomputable def BGS.HasseWeil.heightOneSpectrumResidueFieldAlgEquiv {C : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B] (e : A ≃ₐ[C] B) (q : IsDedekindDomain.HeightOneSpectrum A) : q.asIdeal.ResidueField ≃ₐ[C] ((heightOneSpectrumEquivOfAlgEquiv e) q).asIdeal.ResidueField

Residue fields at corresponding height-one ideals are equivalent over the common coefficient ring.

Equations

• BGS.HasseWeil.heightOneSpectrumResidueFieldAlgEquiv e q = q.asIdeal.residueFieldAlgEquiv ((BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv e) q).asIdeal e ⋯

theorem BGS.HasseWeil.heightOneSpectrum_residueField_finrank_eq {k : Type u_5} {A : Type u_6} {B : Type u_7} [Field k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃ₐ[k] B) (q : IsDedekindDomain.HeightOneSpectrum A) : Module.finrank k q.asIdeal.ResidueField = Module.finrank k ((heightOneSpectrumEquivOfAlgEquiv e) q).asIdeal.ResidueField

Corresponding residue fields have the same degree over the common coefficient field.

@[simp]

theorem BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv_under {A : Type u_2} {B : Type u_3} {R : Type u_4} [CommRing A] [CommRing B] [CommRing R] [IsDedekindDomain R] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] (e : A ≃ₐ[R] B) (q : IsDedekindDomain.HeightOneSpectrum A) : IsDedekindDomain.HeightOneSpectrum.under R ((heightOneSpectrumEquivOfAlgEquiv e) q) = IsDedekindDomain.HeightOneSpectrum.under R q

Transport by an equivalence over the base ring preserves the prime ideal below a height-one ideal.

theorem BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv_under_of_algebraMap_eq {C : Type u_1} {A : Type u_2} {B : Type u_3} {R : Type u_4} [CommRing C] [CommRing A] [CommRing B] [CommRing R] [Algebra C A] [Algebra C B] [IsDedekindDomain R] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] (e : A ≃ₐ[C] B) (h : e.toRingEquiv.toRingHom.comp (algebraMap R A) = algebraMap R B) (q : IsDedekindDomain.HeightOneSpectrum A) : IsDedekindDomain.HeightOneSpectrum.under R ((heightOneSpectrumEquivOfAlgEquiv e) q) = IsDedekindDomain.HeightOneSpectrum.under R q

The same contraction result when the equivalence is over a smaller coefficient ring and compatibility with the base algebra maps is supplied separately.

@[reducible]

noncomputable def BGS.HasseWeil.ratFuncInducedPolynomialAlgebra (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] : Algebra (Polynomial S) T

The polynomial algebra structure on T induced by its RatFunc S-algebra structure.

Equations

• BGS.HasseWeil.ratFuncInducedPolynomialAlgebra S T = ((algebraMap (RatFunc S) T).comp (algebraMap (Polynomial S) (RatFunc S))).toAlgebra

theorem BGS.HasseWeil.ratFuncInducedPolynomialAlgebra_eq (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] (a : Algebra (Polynomial S) T) (h : ∀ (p : Polynomial S), (algebraMap (RatFunc S) T) ((algebraMap (Polynomial S) (RatFunc S)) p) = (algebraMap (Polynomial S) T) p) : ratFuncInducedPolynomialAlgebra S T = a

Pointwise compatibility of polynomial algebra maps identifies a chosen S[X]-algebra structure with the structure induced from RatFunc S.

noncomputable def BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfEq (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] (a : Algebra (Polynomial S) T) (h : ratFuncInducedPolynomialAlgebra S T = a) : ↥(integralClosure (Polynomial S) T) ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

Equality of the ambient polynomial algebra structures identifies their integral closures, one of which is the project's rational-function model.

Equations

• BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfEq S T a h = h ▸ AlgEquiv.refl

noncomputable def BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfAlgebraMap (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] (a : Algebra (Polynomial S) T) (h : ∀ (p : Polynomial S), (algebraMap (RatFunc S) T) ((algebraMap (Polynomial S) (RatFunc S)) p) = (algebraMap (Polynomial S) T) p) : ↥(integralClosure (Polynomial S) T) ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

A polynomial restriction formula for RatFunc S → T gives the normalization equivalence needed by the finite-place model.

Equations

• BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfAlgebraMap S T a h = BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfEq S T a ⋯

noncomputable def BGS.HasseWeil.normalizationAlgEquivRatFuncFiniteOfAlgebraMap (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] (A : Type u_7) [CommRing A] [Algebra (Polynomial S) A] (a : Algebra (Polynomial S) T) (e : A ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) T)) (h : ∀ (p : Polynomial S), (algebraMap (RatFunc S) T) ((algebraMap (Polynomial S) (RatFunc S)) p) = (algebraMap (Polynomial S) T) p) : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

Compose a geometric normalization equivalence with the polynomial algebra bridge, landing in RatFuncFiniteIntegralClosure S T.

Equations

• BGS.HasseWeil.normalizationAlgEquivRatFuncFiniteOfAlgebraMap S T A a e h = e.trans (BGS.HasseWeil.integralClosureAlgEquivRatFuncFiniteOfAlgebraMap S T a h)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finitePlacePolynomialTopAlgebra (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] : Algebra (Polynomial S) T

The algebra structure from S[X] to T used in the finite place normalization transport construction.

Equations

• BGS.HasseWeil.finitePlacePolynomialTopAlgebra S T = BGS.HasseWeil.ratFuncInducedPolynomialAlgebra S T

@[instance_reducible]

noncomputable def BGS.HasseWeil.finitePlaceSourceConstantAlgebra (S : Type u_5) (A : Type u_7) [Field S] [CommRing A] [Algebra (Polynomial S) A] : Algebra S A

The algebra structure from S to A used in the finite place normalization transport construction.

Equations

• BGS.HasseWeil.finitePlaceSourceConstantAlgebra S A = ((algebraMap (Polynomial S) A).comp (algebraMap S (Polynomial S))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.finitePlaceTargetConstantAlgebra (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] : Algebra S ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

The algebra structure from S to (RatFuncFiniteIntegralClosure S T) used in the finite place normalization transport construction.

Equations

• BGS.HasseWeil.finitePlaceTargetConstantAlgebra S T = ((algebraMap (Polynomial S) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure S T)).comp (algebraMap S (Polynomial S))).toAlgebra

theorem BGS.HasseWeil.finitePlaceSourceConstantTower (S : Type u_5) (A : Type u_7) [Field S] [CommRing A] [Algebra (Polynomial S) A] : IsScalarTower S (Polynomial S) A

theorem BGS.HasseWeil.finitePlaceTargetConstantTower (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] : IsScalarTower S (Polynomial S) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

theorem BGS.HasseWeil.finitePlaceTargetIntegral (S : Type u_5) (T : Type u_6) [Field S] [Field T] [Algebra (RatFunc S) T] : Algebra.IsIntegral (Polynomial S) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)

noncomputable def BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv (S : Type u_5) (T : Type u_6) (A : Type u_7) [Field S] [Field T] [CommRing A] [Algebra (RatFunc S) T] [Algebra (Polynomial S) A] (e : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)) : IsDedekindDomain.HeightOneSpectrum A ≃ CorvajaZannier.FiniteExtensionFinitePlace S T

An equivalence of normalization models over S[X] transports their height-one ideals to the project's finite-place type.

Equations

• BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv S T A e = BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv (AlgEquiv.restrictScalars S e)

@[simp]

theorem BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv_asIdeal (S : Type u_5) (T : Type u_6) (A : Type u_7) [Field S] [Field T] [CommRing A] [Algebra (RatFunc S) T] [Algebra (Polynomial S) A] (e : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)) (q : IsDedekindDomain.HeightOneSpectrum A) : ((finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv S T A e) q).asIdeal = Ideal.comap e.symm q.asIdeal

noncomputable def BGS.HasseWeil.finiteExtensionFinitePlaceResidueFieldAlgEquivOfNormalization (S : Type u_5) (T : Type u_6) (A : Type u_7) [Field S] [Field T] [CommRing A] [Algebra (RatFunc S) T] [Algebra (Polynomial S) A] (e : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)) (q : IsDedekindDomain.HeightOneSpectrum A) : q.asIdeal.ResidueField ≃ₐ[S] ((finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv S T A e) q).asIdeal.ResidueField

A normalization equivalence transports the residue field at each height-one ideal as an S-algebra.

Equations

• BGS.HasseWeil.finiteExtensionFinitePlaceResidueFieldAlgEquivOfNormalization S T A e q = BGS.HasseWeil.heightOneSpectrumResidueFieldAlgEquiv (AlgEquiv.restrictScalars S e) q

theorem BGS.HasseWeil.finiteExtensionFinitePlace_residueField_finrank_eq_of_normalization (S : Type u_5) (T : Type u_6) (A : Type u_7) [Field S] [Field T] [CommRing A] [Algebra (RatFunc S) T] [Algebra (Polynomial S) A] (e : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)) (q : IsDedekindDomain.HeightOneSpectrum A) : Module.finrank S q.asIdeal.ResidueField = Module.finrank S ((finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv S T A e) q).asIdeal.ResidueField

The constant-field residue degree is unchanged when replacing a normalization by an equivalent model.

@[simp]

theorem BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv_under (S : Type u_5) (T : Type u_6) (A : Type u_7) [Field S] [Field T] [CommRing A] [Algebra (RatFunc S) T] [Algebra (Polynomial S) A] [IsDomain A] [Algebra.IsIntegral (Polynomial S) A] (e : A ≃ₐ[Polynomial S] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure S T)) (q : IsDedekindDomain.HeightOneSpectrum A) : IsDedekindDomain.HeightOneSpectrum.under (Polynomial S) ((finiteExtensionFinitePlaceEquivOfNormalizationAlgEquiv S T A e) q) = IsDedekindDomain.HeightOneSpectrum.under (Polynomial S) q

The finite place below a transported ideal agrees with the contraction of the source ideal to S[X].