Nonzero affine ideals as effective finite divisors

In a Dedekind domain, a nonzero ideal is uniquely determined by the multiplicity of every height-one prime in its factorization. This file packages that factorization as an equivalence between nonzero ideals and effective, finitely supported divisors.

Specializing to the normalization of K[X] in a finite separable extension of K(X) identifies nonzero affine ideals with effective divisors on the finite places of the function field. The equivalence is purely Dedekind factorization: it does not use Riemann--Roch or a zeta-function argument.

def BGS.HasseWeil.effectiveDivisorIdeal {R : Type u_1} [CommRing R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : Ideal R

The ideal represented by an effective divisor on the height-one primes of a Dedekind domain.

Equations

• BGS.HasseWeil.effectiveDivisorIdeal D = D.prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℕ) => v.asIdeal ^ e

@[simp]

theorem BGS.HasseWeil.effectiveDivisorIdeal_zero {R : Type u_1} [CommRing R] : effectiveDivisorIdeal 0 = ⊤

@[simp]

theorem BGS.HasseWeil.effectiveDivisorIdeal_single {R : Type u_1} [CommRing R] (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℕ) : effectiveDivisorIdeal (Finsupp.single v e) = v.asIdeal ^ e

theorem BGS.HasseWeil.effectiveDivisorIdeal_add {R : Type u_1} [CommRing R] (D E : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : effectiveDivisorIdeal (D + E) = effectiveDivisorIdeal D * effectiveDivisorIdeal E

theorem BGS.HasseWeil.isCoprime_effectiveDivisorIdeal_of_not_mem_support {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) (hv : v ∉ D.support) : IsCoprime v.asIdeal (effectiveDivisorIdeal D)

A height-one prime outside the support of an effective divisor is coprime to the ideal represented by that divisor.

theorem BGS.HasseWeil.cardQuot_effectiveDivisorIdeal_eq_prod {R : Type u_1} [CommRing R] [IsDedekindDomain R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : Submodule.cardQuot (effectiveDivisorIdeal D) = D.prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℕ) => Submodule.cardQuot v.asIdeal ^ e

The quotient cardinality of the ideal represented by an effective divisor is the product of the quotient cardinalities of its prime powers.

theorem BGS.HasseWeil.effectiveDivisorIdeal_ne_bot {R : Type u_1} [CommRing R] [IsDedekindDomain R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : effectiveDivisorIdeal D ≠ ⊥

A product of powers of height-one primes is a nonzero ideal.

theorem BGS.HasseWeil.effectiveDivisorIdeal_idealMultiplicityDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) (hI : I ≠ ⊥) : effectiveDivisorIdeal (CorvajaZannier.idealMultiplicityDivisor I hI) = I

Reconstructing a nonzero ideal from its prime multiplicities returns the original ideal.

theorem BGS.HasseWeil.multiplicity_effectiveDivisorIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) (v : IsDedekindDomain.HeightOneSpectrum R) : multiplicity v.asIdeal (effectiveDivisorIdeal D) = D v

The multiplicity of a prime in the ideal represented by an effective divisor is its coefficient in that divisor.

theorem BGS.HasseWeil.idealMultiplicityDivisor_effectiveDivisorIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : CorvajaZannier.idealMultiplicityDivisor (effectiveDivisorIdeal D) ⋯ = D

Taking prime multiplicities after constructing the ideal represented by an effective divisor recovers the divisor.

theorem BGS.HasseWeil.nonzeroIdeal_ne_bot {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) : ↑I ≠ ⊥

A nonzero ideal, regarded as an element of the non-zero-divisors submonoid, is not the bottom ideal.

noncomputable def BGS.HasseWeil.nonzeroIdealEffectiveDivisorEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] : ↥(nonZeroDivisors (Ideal R)) ≃ (IsDedekindDomain.HeightOneSpectrum R →₀ ℕ)

Dedekind factorization as an equivalence between nonzero ideals and effective finitely supported divisors on height-one primes.

Equations

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

@[simp]

theorem BGS.HasseWeil.nonzeroIdealEffectiveDivisorEquiv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) (v : IsDedekindDomain.HeightOneSpectrum R) : (nonzeroIdealEffectiveDivisorEquiv I) v = multiplicity v.asIdeal ↑I

@[simp]

theorem BGS.HasseWeil.nonzeroIdealEffectiveDivisorEquiv_symm_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ) : ↑(nonzeroIdealEffectiveDivisorEquiv.symm D) = effectiveDivisorIdeal D

@[instance_reducible]

noncomputable def BGS.HasseWeil.affineDivisorPolynomialAlgebra (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 finite extension affine ideal divisor construction.

Equations

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

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

theorem BGS.HasseWeil.affineDivisorFiniteClosureModuleFinite (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] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

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

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension affine ideal divisor construction.

Equations

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

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

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

theorem BGS.HasseWeil.affineDivisorPolynomialTorsionFreeTop (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] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.affineDivisorFiniteClosureTorsionFree (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] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.affineDivisorFiniteClosureDedekind (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 ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveFiniteDivisorDegree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) : ℕ

The degree of an effective finite divisor is the sum of its multiplicities weighted by the dimensions of the residue fields over the constant field.

Equations

• BGS.HasseWeil.finiteExtensionEffectiveFiniteDivisorDegree K L D = D.sum fun (v : BGS.CorvajaZannier.FiniteExtensionFinitePlace K L) (e : ℕ) => e * Module.finrank K v.asIdeal.ResidueField

theorem BGS.HasseWeil.finiteExtensionFinitePlace_cardQuot_eq_card_pow_degree (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (v : CorvajaZannier.FiniteExtensionFinitePlace K L) : Submodule.cardQuot v.asIdeal = Fintype.card K ^ Module.finrank K v.asIdeal.ResidueField

The quotient cardinality of a finite-place prime is the cardinality of the constant field raised to the residue-field degree.

theorem BGS.HasseWeil.effectiveDivisorIdeal_cardQuot_eq_card_pow_degree (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) : Submodule.cardQuot (effectiveDivisorIdeal D) = Fintype.card K ^ finiteExtensionEffectiveFiniteDivisorDegree K L D

Quotient cardinality is the constant-field cardinality raised to the degree of the represented effective finite divisor.

noncomputable def BGS.HasseWeil.finiteExtensionAffineIdealEffectiveDivisorEquiv (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] : ↥(FiniteExtensionAffineIdeal K L) ≃ (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ)

Nonzero affine ideals in the normalization of K[X] are exactly effective divisors on the finite places of the function field.

Equations

• BGS.HasseWeil.finiteExtensionAffineIdealEffectiveDivisorEquiv K L = BGS.HasseWeil.nonzeroIdealEffectiveDivisorEquiv

@[simp]

theorem BGS.HasseWeil.finiteExtensionAffineIdealEffectiveDivisorEquiv_apply (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] (I : ↥(FiniteExtensionAffineIdeal K L)) (v : CorvajaZannier.FiniteExtensionFinitePlace K L) : ((finiteExtensionAffineIdealEffectiveDivisorEquiv K L) I) v = multiplicity v.asIdeal ↑I

@[simp]

theorem BGS.HasseWeil.finiteExtensionAffineIdealEffectiveDivisorEquiv_symm_coe (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] (D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) : ↑((finiteExtensionAffineIdealEffectiveDivisorEquiv K L).symm D) = effectiveDivisorIdeal D

theorem BGS.HasseWeil.finiteExtensionAffineIdealDegree_equiv_symm (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] [Finite K] (D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) : finiteExtensionAffineIdealDegree K L ((finiteExtensionAffineIdealEffectiveDivisorEquiv K L).symm D) = finiteExtensionEffectiveFiniteDivisorDegree K L D

The affine ideal degree of the ideal represented by an effective finite divisor is its residue-degree-weighted divisor degree.

theorem BGS.HasseWeil.finiteExtensionAffineIdealDegree_eq_divisorDegree (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] [Finite K] (I : ↥(FiniteExtensionAffineIdeal K L)) : finiteExtensionAffineIdealDegree K L I = finiteExtensionEffectiveFiniteDivisorDegree K L ((finiteExtensionAffineIdealEffectiveDivisorEquiv K L) I)

The degree of a nonzero affine ideal is the residue-degree-weighted sum of its finite-place prime multiplicities.

theorem BGS.HasseWeil.finiteExtensionAffineIdealDegree_eq_sum_multiplicity_mul_residueDegree (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] [Finite K] (I : ↥(FiniteExtensionAffineIdeal K L)) : finiteExtensionAffineIdealDegree K L I = ((finiteExtensionAffineIdealEffectiveDivisorEquiv K L) I).sum fun (v : CorvajaZannier.FiniteExtensionFinitePlace K L) (e : ℕ) => e * Module.finrank K v.asIdeal.ResidueField

Expanded pointwise form of the affine ideal degree formula.

noncomputable def BGS.HasseWeil.finiteExtensionAffineIdealsOfDegreeEquivEffectiveFiniteDivisorsOfDegree (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : { I : ↥(FiniteExtensionAffineIdeal K L) // finiteExtensionAffineIdealDegree K L I = n } ≃ { D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ // finiteExtensionEffectiveFiniteDivisorDegree K L D = n }

The ideal/divisor equivalence restricts to each degree.

Equations

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

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finiteExtensionEffectiveFiniteDivisorsOfDegreeFintype (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : Fintype { D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ // finiteExtensionEffectiveFiniteDivisorDegree K L D = n }

Effective finite divisors of a fixed degree form a finite type, transported from the already-finite type of affine ideals of that degree.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveFiniteDivisorCount (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : ℕ

The effective-finite-divisor coefficient of degree n.

Equations

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

theorem BGS.HasseWeil.finiteExtensionAffineIdealCount_eq_effectiveFiniteDivisorCount (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : finiteExtensionAffineIdealCount K L n = finiteExtensionEffectiveFiniteDivisorCount K L n

The affine ideal coefficient sequence is exactly the effective finite-divisor coefficient sequence.