Documentation

TauCeti.AlgebraicGeometry.Curves.StableReduction.Picard.Contraction

The Picard group under contraction of a (-1)-index #

Let e be a (-1)-index of a numerical type T and let T' be the contracted numerical type TauCeti.NumericalType.contract, with components those of T other than e, weights w'ᵢ and intersection numbers a'ᵢⱼ = aᵢⱼ + aᵢₑaⱼₑ / wₑ. The map of multidegrees

p(d)ⱼ = dⱼ (wⱼ / w'ⱼ) + dₑ (aₑⱼ / w'ⱼ)

carries the multidegree of each component i ≠ e of T to that of i in T', and the multidegree of e to zero. It therefore descends to a homomorphism Pic(T) → Pic(T'), which is injective and whose cokernel is killed by 2, since each ratio wⱼ / w'ⱼ is 1 or 2 (Stacks, Lemma 55.4.4).

This reduces questions about the torsion of Pic(T) to minimal numerical types: the ℓ-torsion of Pic(T) has dimension at most that of Pic(T'). It also shows that the Picard group of a numerical type of nonpositive genus is infinite cyclic (Stacks, Lemma 55.4.5): such a type with more than one component is not minimal, and contracting a (-1)-index preserves the genus.

Main definitions #

Main results #

References #

The map p and the proofs of injectivity and of the bound on the cokernel follow Stacks, Lemma 55.4.4, and the induction on the number of components that of Stacks, Lemma 55.4.5, in Stacks, Section 55.4.

The map of multidegrees #

source
def TauCeti.NumericalType.contractMultidegree {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) :
(T.Component → ℤ) →ₗ[ℤ] (T.contract he).Component → ℤ

The map of multidegrees p(d)ⱼ = dⱼ (wⱼ / w'ⱼ) + dₑ (aₑⱼ / w'ⱼ) from a numerical type to its contraction along the (-1)-index e. It sends the multidegree of every component i ≠ e to the multidegree of i in the contraction and the multidegree of e to zero; see TauCeti.NumericalType.contractMultidegree_vecMul_weightedIntersection.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.NumericalType.contractMultidegree_apply {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (d : T.Component → ℤ) (j : { i : T.Component // i ≠ e }) :
    (contractMultidegree he) d j = ↑↑(T.weight ↑j) / ↑↑(contractWeight e j) * d ↑j + T.intersection e ↑j / ↑↑(contractWeight e j) * d e

    The coordinates of TauCeti.NumericalType.contractMultidegree.

    source
    theorem TauCeti.NumericalType.contractMultidegree_mul_contractWeight {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (d : T.Component → ℤ) (j : { i : T.Component // i ≠ e }) :
    (contractMultidegree he) d j * ↑↑(contractWeight e j) = d ↑j * ↑↑(T.weight ↑j) + d e * T.intersection e ↑j

    The coordinates of TauCeti.NumericalType.contractMultidegree with the exact divisions by w'ⱼ cleared: p(d)ⱼ w'ⱼ = dⱼwⱼ + dₑaₑⱼ.

    source
    @[simp]
    theorem TauCeti.NumericalType.contractMultidegree_row {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i : { i : T.Component // i ≠ e }) :
    (contractMultidegree he) (T.weightedIntersection ↑i) = (T.contract he).weightedIntersection i

    The map of multidegrees sends the multidegree of a component i ≠ e to the multidegree of i in the contraction.

    source
    @[simp]
    theorem TauCeti.NumericalType.contractMultidegree_row_self {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) :
    (contractMultidegree he) (T.weightedIntersection e) = 0

    The map of multidegrees kills the multidegree of the contracted component e.

    source
    @[simp]
    theorem TauCeti.NumericalType.contractMultidegree_vecMul_weightedIntersection {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (v : T.Component → ℤ) :
    (contractMultidegree he) (Matrix.vecMul v T.weightedIntersection) = Matrix.vecMul (fun (i : { i : T.Component // i ≠ e }) => v ↑i) (T.contract he).weightedIntersection

    The map of multidegrees intertwines the weighted intersection matrices: the image of a combination v of the multidegrees of the components of T is the same combination, with the coefficient of e dropped, of the multidegrees of the components of the contraction.

    source
    theorem TauCeti.NumericalType.mem_principalDivisors_of_contractMultidegree_eq_zero {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) {d : T.Component → ℤ} (hd : (contractMultidegree he) d = 0) :
    d ∈ T.principalDivisors

    A multidegree killed by the map of multidegrees is principal: it is a multiple of the multidegree of e.

    The homomorphism of Picard groups #

    source
    theorem TauCeti.NumericalType.principalDivisors_le_comap_contractMultidegree {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) :
    T.principalDivisors ≤ Submodule.comap (contractMultidegree he) (T.contract he).principalDivisors

    The principal multidegrees of T map to principal multidegrees of its contraction.

    source
    def TauCeti.NumericalType.picContract {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) :
    T.Pic →ₗ[ℤ] (T.contract he).Pic

    The homomorphism Pic(T) → Pic(T') from the Picard group of a numerical type to that of its contraction along a (-1)-index, induced by TauCeti.NumericalType.contractMultidegree (Stacks, Lemma 55.4.4).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.NumericalType.picContract_mk {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (d : T.Component → ℤ) :
      (picContract he) (Submodule.Quotient.mk d) = Submodule.Quotient.mk ((contractMultidegree he) d)

      The homomorphism of Picard groups on the class of a multidegree.

      source
      theorem TauCeti.NumericalType.picContract_injective {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) :
      Function.Injective ⇑(picContract he)

      The homomorphism Pic(T) → Pic(T') is injective (Stacks, Lemma 55.4.4).

      source
      theorem TauCeti.NumericalType.two_smul_mem_range_picContract {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (y : (T.contract he).Pic) :
      2 • y ∈ (picContract he).range

      The cokernel of Pic(T) → Pic(T') is killed by 2: twice every class of the contraction comes from Pic(T) (Stacks, Lemma 55.4.4).

      Consequences #

      source
      theorem TauCeti.NumericalType.finrank_torsion_le_contract {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] :
      Module.finrank (ZMod ℓ) ↥(T.torsion ℓ) ≤ Module.finrank (ZMod ℓ) ↥((T.contract he).torsion ℓ)

      The ℓ-torsion of Pic(T) has dimension at most that of Pic(T'), for every prime ℓ. This reduces bounds on the prime torsion of Picard groups of numerical types to minimal numerical types.

      source
      theorem TauCeti.NumericalType.nonempty_pic_linearEquiv_int (T : NumericalType) (hg : T.arithmeticGenus ≤ 0) :
      Nonempty (T.Pic ≃ₗ[ℤ] ℤ)

      The Picard group of a numerical type of genus at most zero is infinite cyclic (Stacks, Lemma 55.4.5).