Leading coefficients at a single place

Compare residue-field degrees and lift constant residues through the local rings of finite and infinite places.

theorem BGS.CorvajaZannier.localizationAtPrime_constantResidue_surjective {C : Type u_1} {R : Type u_2} {S : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [Algebra C R] [CommRing S] [Algebra R S] [Algebra C S] [IsScalarTower C R S] (q : IsDedekindDomain.HeightOneSpectrum R) [IsLocalization q.asIdeal.primeCompl S] [IsLocalRing S] (hresidue : Function.Surjective ⇑(algebraMap C q.asIdeal.ResidueField)) : Function.Surjective ⇑(algebraMap C (IsLocalRing.maximalIdeal S).ResidueField)

Surjectivity of constants onto a height-one residue field is preserved when the Dedekind domain is localized at that place.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.onePointPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointFiniteConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointFiniteConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.CorvajaZannier.onePointFiniteConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointInfinityConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.CorvajaZannier.onePointInfinityConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsScalarTower K (↥(RatFuncInfinityIntegers K)) (RatFunc K)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointInfinityClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the one point leading coefficient construction.

Equations

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

theorem BGS.CorvajaZannier.onePointInfinityClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.ratFuncFinitePlaceDegree_eq_finrank_residueField (K : Type u_1) [Field K] [DecidableEq K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ratFuncFinitePlaceDegree p = Module.finrank K p.asIdeal.ResidueField

The degree of a rational-function finite place is the dimension of its residue field over the constant field.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_degree_eq_finrank_residueField (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : FiniteExtensionFinitePlace K L) : finiteExtensionPlaceDegree K L (Sum.inl q) = Module.finrank K q.asIdeal.ResidueField

At a finite extension place, the exhaustive place degree is exactly the constant-field dimension of the residue field.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_degree_eq_finrank_residueField (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (P : ↑(FiniteExtensionInfinityPlace K L)) : finiteExtensionPlaceDegree K L (Sum.inr P) = Module.finrank K (↑P).ResidueField

At an infinity extension place, the exhaustive place degree is exactly the constant-field dimension of the residue field.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_constantResidue_surjective_of_degree_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : FiniteExtensionFinitePlace K L) (hq : finiteExtensionPlaceDegree K L (Sum.inl q) = 1) : Function.Surjective ⇑(algebraMap K q.asIdeal.ResidueField)

Degree one forces constants to fill the residue field at a finite extension place.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_constantResidue_surjective_of_degree_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (P : ↑(FiniteExtensionInfinityPlace K L)) (hP : finiteExtensionPlaceDegree K L (Sum.inr P) = 1) : Function.Surjective ⇑(algebraMap K (↑P).ResidueField)

Degree one forces constants to fill the residue field at an infinity extension place.

theorem BGS.CorvajaZannier.exists_constant_finitePlaceOrder_sub_mul_eq_zero_or_lt_of_residue {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] (q : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C q.asIdeal.ResidueField)) (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (horder : finitePlaceOrder q x = finitePlaceOrder q y) : ∃ (c : C), x - (algebraMap C L) c * y = 0 ∨ finitePlaceOrder q x < finitePlaceOrder q (x - (algebraMap C L) c * y)

Global height-one cancellation obtained by applying the DVR theorem after localizing at the chosen Dedekind place.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointCancellationConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointCancellationConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.onePointCancellationConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointCancellationPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointCancellationPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.onePointCancellationPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointCancellationFiniteConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the one point leading coefficient construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointCancellationInfinityBaseConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the one point leading coefficient construction.

Equations

• BGS.CorvajaZannier.onePointCancellationInfinityBaseConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.onePointCancellationInfinityConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the one point leading coefficient construction.

Equations

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

theorem BGS.CorvajaZannier.onePointCancellationFiniteIsDedekindDomain (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.onePointCancellationFiniteIsFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncFiniteIntegralClosure K L)) L

theorem BGS.CorvajaZannier.onePointCancellationInfinityIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.onePointCancellationInfinityIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncInfinityIntegralClosure K L)) L

theorem BGS.CorvajaZannier.onePointCancellationInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(RatFuncInfinityIntegers K)) L

theorem BGS.CorvajaZannier.onePointCancellationInfinityIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.onePointCancellationFiniteConstantTowerToField (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (↥(RatFuncFiniteIntegralClosure K L)) L

theorem BGS.CorvajaZannier.onePointCancellationInfinityConstantTowerToField (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (↥(RatFuncInfinityIntegralClosure K L)) L

theorem BGS.CorvajaZannier.exists_constant_finiteExtensionPlaceOrder_sub_mul_eq_zero_or_lt (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (hP : finiteExtensionPlaceDegree K L P = 1) (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (horder : (finiteExtensionPrincipalDivisor K L x) P = (finiteExtensionPrincipalDivisor K L y) P) : ∃ (c : K), x - (algebraMap K L) c * y = 0 ∨ (finiteExtensionPrincipalDivisor K L x) P < (finiteExtensionPrincipalDivisor K L (x - (algebraMap K L) c * y)) P

At a degree-one exhaustive place, equal-order nonzero functions admit a strict constant leading-term cancellation.

theorem BGS.CorvajaZannier.exists_constant_sub_mul_mem_onePointRiemannSpace_pred (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (hP : finiteExtensionPlaceDegree K L P = 1) {n : ℕ} (hn : 0 < n) {x y : L} (hx : x ∈ finiteExtensionOnePointRiemannSpace K L P n) (hy : y ∈ finiteExtensionOnePointRiemannSpace K L P n) (hx0 : x ≠ 0) (hy0 : y ≠ 0) (hxOrder : (finiteExtensionPrincipalDivisor K L x) P = -↑n) (hyOrder : (finiteExtensionPrincipalDivisor K L y) P = -↑n) : ∃ (c : K), x - (algebraMap K L) c * y = 0 ∨ x - (algebraMap K L) c * y ∈ finiteExtensionOnePointRiemannSpace K L P (n - 1)

At a degree-one place, cancelling the common leading coefficient of two nonzero sections with exact pole order n either gives zero or lowers the allowed pole order by one.

theorem BGS.CorvajaZannier.exists_onePointRiemannSpace_pivot_of_lt (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (hP : finiteExtensionPlaceDegree K L P = 1) (n : ℕ) (hstrict : finiteExtensionOnePointRiemannSpace K L P n < finiteExtensionOnePointRiemannSpace K L P (n + 1)) : ∃ y ∈ finiteExtensionOnePointRiemannSpace K L P (n + 1), (finiteExtensionPrincipalDivisor K L y) P = -↑(n + 1) ∧ ∀ x ∈ finiteExtensionOnePointRiemannSpace K L P (n + 1), ∃ (c : K), x - c • y ∈ finiteExtensionOnePointRiemannSpace K L P n

If the degree-one one-point filtration grows at level n + 1, one new section is a pivot for the whole quotient. Its pole order is exactly -(n + 1), and every section of the larger space becomes a scalar multiple of it modulo the preceding space.