Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.FixedDegree.Addition

Addition of fixed-degree effective Weil divisors #

This file records the degree-indexed addition operation on effective Weil divisors of fixed degree. Adding an effective divisor of degree d to one of degree e gives an effective divisor of degree d + e; under the equivalence with Mathlib's symmetric powers, this is exactly Sym.append.

This is formal divisor bookkeeping for the Jacobian challenge roadmap's Layer C symmetric-power lane (TauCetiRoadmap/JacobianChallenge/README.md, "Relative effective Cartier divisors and symmetric powers Symᵈ X"). It supplies the additive compatibility between unordered collections of points and the effective-divisor model used by Abel-map statements. No external mathematics is vendored.

source
@[reducible, inline]
noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
EffectiveDivisorOfDegree X (d + e)

Add fixed-degree effective divisors. The degree index records additivity of degree.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    ↑(D.add E) = ↑D + ↑E

    The underlying Weil divisor of a fixed-degree sum is the sum of the underlying divisors.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coeff_add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (x : X) :
    (↑(D.add E)).coeff x = (↑D).coeff x + (↑E).coeff x

    The coefficient of a fixed-degree sum is the sum of the coefficients.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.zero_add {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) :
    (zero X).add D = (EffectiveDivisorOfDegree.cast ⋯) D

    Zero is a left identity for fixed-degree effective-divisor addition.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_zero {X : Type u_1} {d : ℕ} (D : EffectiveDivisorOfDegree X d) :
    D.add (zero X) = (EffectiveDivisorOfDegree.cast ⋯) D

    Zero is a right identity for fixed-degree effective-divisor addition.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_comm {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    D.add E = (EffectiveDivisorOfDegree.cast ⋯) (E.add D)

    Fixed-degree effective-divisor addition is commutative, up to the degree-index cast.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_assoc {X : Type u_1} {d e n : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) (F : EffectiveDivisorOfDegree X n) :
    (D.add E).add F = (EffectiveDivisorOfDegree.cast ⋯) (D.add (E.add F))

    Fixed-degree effective-divisor addition is associative, up to the degree-index cast.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_ofFinsupp {X : Type u_1} {d e : ℕ} (m n : X →₀ ℕ) (hm : (m.sum fun (x : X) (k : ℕ) => k) = d) (hn : (n.sum fun (x : X) (k : ℕ) => k) = e) :
    (ofFinsupp m hm).add (ofFinsupp n hn) = ofFinsupp (m + n) ⋯

    Adding divisors built from finitely supported multiplicities corresponds to adding their multiplicity functions.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.multiplicityFinsupp_add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    (D.add E).multiplicityFinsupp = D.multiplicityFinsupp + E.multiplicityFinsupp

    The multiplicity function of a sum is the sum of the multiplicity functions.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_add {X : Type u_1} {d e : ℕ} (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    equivSym (D.add E) = (equivSym D).append (equivSym E)

    The symmetric-power equivalence sends fixed-degree divisor addition to Sym.append.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.add_ofSym {X : Type u_1} {d e : ℕ} (s : Sym X d) (t : Sym X e) :
    (ofSym s).add (ofSym t) = ofSym (s.append t)

    Adding the divisors associated to symmetric-power points is the divisor associated to their appended unordered collection.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.coe_ofSym_append {X : Type u_1} {d e : ℕ} (s : Sym X d) (t : Sym X e) :
    WeilDivisor.ofFinsupp ↑((Sym.equivNatSum X (d + e)) (s.append t)) = ↑(ofSym s) + ↑(ofSym t)

    The divisor associated to an appended symmetric-power point is the sum of the associated fixed-degree divisors.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.pushforward_add {X : Type u_1} {Y : Type u_2} {d e : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    pushforward f (D.add E) = (pushforward f D).add (pushforward f E)

    Pushforward commutes with addition of fixed-degree effective divisors.

    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.EffectiveDivisorOfDegree.equivSym_pushforward_add {X : Type u_1} {Y : Type u_2} {d e : ℕ} (f : X → Y) (D : EffectiveDivisorOfDegree X d) (E : EffectiveDivisorOfDegree X e) :
    equivSym (pushforward f (D.add E)) = (Sym.map f (equivSym D)).append (Sym.map f (equivSym E))

    On symmetric powers, pushforward compatibility for fixed-degree divisor addition is the usual compatibility of Sym.map with Sym.append.