Coordinate-free divisors and degree

This file transports the two-chart divisor group to intrinsic places and identifies the transported degree with the residue-field weighted sum.

Main definitions

• FunctionField.Divisor: divisors indexed by intrinsic places.
• FunctionField.divisorEquivChart: equivalence with the two-chart divisor group.
• FunctionField.Divisor.deg: intrinsic divisor degree.
• FunctionField.principalDivisor: coordinate-free principal divisors.

@[instance_reducible]

noncomputable def FunctionField.instDecidableEqRatFuncCoordinateFreeDivisor (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

Classical decidable equality for the coordinate rational function field.

Equations

• FunctionField.instDecidableEqRatFuncCoordinateFreeDivisor k = Classical.decEq (RatFunc k)

@[instance_reducible]

noncomputable def FunctionField.Place.finiteVspAlgebra (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : Algebra k ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w)

Constant-field algebra structure on a finite-place valuation subring.

Equations

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

theorem FunctionField.Place.finiteVspTower (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : IsScalarTower k ↥(ringOfIntegers k K) ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w)

Scalar-tower compatibility for a finite-place valuation subring.

noncomputable def FunctionField.Place.finiteValuationSubringAlgEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w) ≃ₐ[k] ↥(ofChart k K (Sum.inl w)).toValuationSubring

The finite-chart valuation subring is the valuation subring of the intrinsic place.

Equations

• FunctionField.Place.finiteValuationSubringAlgEquiv k K w = { toEquiv := (RingEquiv.subringCongr ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def FunctionField.Place.finiteResidueAlgEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : (↥(ringOfIntegers k K) ⧸ w.asIdeal) ≃ₐ[k] (ofChart k K (Sum.inl w)).residueField

The finite-chart residue field is the intrinsic residue field.

Equations

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

theorem FunctionField.Place.finite_degree_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : (ofChart k K (Sum.inl w)).degree = Chart.placeDegree k K (Sum.inl w)

@[instance_reducible]

noncomputable def FunctionField.Place.infiniteVspAlgebra (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : Algebra k ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w)

Constant-field algebra structure on an infinite-place valuation subring.

Equations

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

theorem FunctionField.Place.infiniteVspTower (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : IsScalarTower k ↥(Chart.infiniteIntegers k K) ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w)

Scalar-tower compatibility for an infinite-place valuation subring.

noncomputable def FunctionField.Place.infiniteValuationSubringAlgEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K w) ≃ₐ[k] ↥(ofChart k K (Sum.inr w)).toValuationSubring

The infinite-chart valuation subring is the valuation subring of the intrinsic place.

Equations

• FunctionField.Place.infiniteValuationSubringAlgEquiv k K w = { toEquiv := (RingEquiv.subringCongr ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def FunctionField.Place.infiniteResidueAlgEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : (↥(Chart.infiniteIntegers k K) ⧸ w.asIdeal) ≃ₐ[k] (ofChart k K (Sum.inr w)).residueField

The infinite-chart residue field is the intrinsic residue field.

Equations

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

theorem FunctionField.Place.infinite_degree_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : (ofChart k K (Sum.inr w)).degree = Chart.placeDegree k K (Sum.inr w)

theorem FunctionField.placeDegree_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : Chart.placeDegree k K w = ((chartToPlace k K) w).degree

The chart degree agrees with the intrinsic residue-field degree.

@[reducible, inline]

abbrev FunctionField.Divisor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Type u_2

Divisors indexed by coordinate-free places.

Equations

• FunctionField.Divisor k K = (FunctionField.Place k K →₀ ℤ)

noncomputable def FunctionField.divisorEquivChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Chart.DivisorA k K ≃+ Divisor k K

Reindex a chart divisor by the chart/intrinsic place equivalence.

Equations

• FunctionField.divisorEquivChart k K = Finsupp.domCongr (FunctionField.chartToPlace k K)

noncomputable def FunctionField.principalDivisor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Additive Kˣ →+ Divisor k K

The coordinate-free principal-divisor homomorphism.

Equations

• FunctionField.principalDivisor k K = (FunctionField.divisorEquivChart k K).toAddMonoidHom.comp (FunctionField.Chart.principalDivisorA k K)

noncomputable def FunctionField.Divisor.deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : ℤ

The intrinsic weighted degree of a divisor.

Equations

• FunctionField.Divisor.deg k K D = Finsupp.sum D fun (v : FunctionField.Place k K) (n : ℤ) => n * ↑v.degree

theorem FunctionField.Divisor.deg_formula (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : deg k K D = Finsupp.sum D fun (v : Place k K) (n : ℤ) => n * ↑v.degree

The degree is the intrinsic residue-degree weighted sum.

theorem FunctionField.Divisor.deg_add (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D E : Divisor k K) : deg k K (D + E) = deg k K D + deg k K E

theorem FunctionField.Divisor.deg_equivChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Chart.DivisorA k K) : deg k K ((divisorEquivChart k K) D) = Chart.deg k K D

theorem FunctionField.Divisor.deg_principal_eq_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) : deg k K ((principalDivisor k K) (Additive.ofMul x)) = 0

Principal divisors have degree zero.