Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.FractionalIdealDivisor.Effectivity

Effective divisors and integral fractional ideals #

For a Dedekind domain R with fraction field K, fractionalIdealDivisorAddEquiv R K identifies invertible fractional ideals with Weil divisors on the height-one spectrum of R. This file proves that the equivalence respects the positive parts on both sides: a fractional ideal is contained in R exactly when all of its height-one multiplicities are nonnegative.

Thus the affine Weil--Cartier dictionary restricts to an additive equivalence between integral invertible fractional ideals and effective Weil divisors. This directly advances the Weil ≃ Cartier divisor dictionary in Layer A of TauCetiRoadmap/JacobianChallenge/README.md.

The reverse implication uses Mathlib's factorization of a nonzero fractional ideal as the finite product of its height-one prime powers. No external formalization is copied.

source
def TauCeti.AlgebraicGeometry.WeilDivisor.integralFractionalIdealSubmonoid (R : Type u_1) [CommRing R] (K : Type u_2) [CommRing K] [Algebra R K] :
AddSubmonoid (Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ)

The additive submonoid of invertible fractional ideals contained in R.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_integralFractionalIdealSubmonoid (R : Type u_1) [CommRing R] (K : Type u_2) [CommRing K] [Algebra R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
    I ∈ integralFractionalIdealSubmonoid R K ↔ ↑(Additive.toMul I) ≤ 1

    Membership in integralFractionalIdealSubmonoid means that the fractional ideal is contained in the base ring.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_fractionalIdealDivisor_of_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) (hI : ↑(Additive.toMul I) ≤ 1) :
    ((fractionalIdealDivisor R K) I).IsEffective

    The divisor of an integral fractional ideal (one contained in R, i.e. ≤ 1) is effective: integral ideals have no poles, only zeros. This is the affine "effective divisor ↔ integral ideal" half of the dictionary.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.le_one_of_isEffective_fractionalIdealDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) (hI : ((fractionalIdealDivisor R K) I).IsEffective) :
    ↑(Additive.toMul I) ≤ 1

    If the divisor of an invertible fractional ideal is effective, then the fractional ideal is integral. This is the converse of isEffective_fractionalIdealDivisor_of_le_one.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_fractionalIdealDivisor_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
    ((fractionalIdealDivisor R K) I).IsEffective ↔ ↑(Additive.toMul I) ≤ 1

    An invertible fractional ideal is integral exactly when its associated Weil divisor is effective.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_fractionalIdealDivisor_iff_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
    ((fractionalIdealDivisor R K) I).IsEffective ↔ I ∈ integralFractionalIdealSubmonoid R K

    The divisor of an invertible fractional ideal is effective exactly when that ideal belongs to the integral fractional-ideal submonoid.

    source
    noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.integralFractionalIdealDivisorAddEquiv (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] :
    ↥(integralFractionalIdealSubmonoid R K) ≃+ ↥(effectiveSubmonoid (IsDedekindDomain.HeightOneSpectrum R))

    The affine Weil--Cartier equivalence restricted to positive objects: integral invertible fractional ideals correspond exactly to effective Weil divisors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.WeilDivisor.coe_integralFractionalIdealDivisorAddEquiv (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (I : ↥(integralFractionalIdealSubmonoid R K)) :
      ↑((integralFractionalIdealDivisorAddEquiv R K) I) = (fractionalIdealDivisor R K) ↑I

      The restricted equivalence agrees with fractionalIdealDivisor after forgetting effectivity.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.WeilDivisor.coe_integralFractionalIdealDivisorAddEquiv_symm (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (D : ↥(effectiveSubmonoid (IsDedekindDomain.HeightOneSpectrum R))) :
      ↑((integralFractionalIdealDivisorAddEquiv R K).symm D) = (fractionalIdealDivisorAddEquiv R K).symm ↑D

      The inverse restricted equivalence agrees with the unrestricted inverse after forgetting integrality.