Contracting a (-1)-index of a numerical type

Let e be a (-1)-index of a numerical type T, so that gₑ = 0 and aₑₑ = -wₑ. On a proper regular model this is the numerical shadow of an exceptional curve of the first kind, and contracting that curve produces a new regular model. This file constructs the numerical type T' of the contracted model (Stacks, Tag 0C77). Its components are those of T other than e, and for such components i, j:

• m'ᵢ = mᵢ;
• a'ᵢⱼ = aᵢⱼ - aᵢₑaⱼₑ / aₑₑ = aᵢⱼ + aᵢₑaⱼₑ / wₑ;
• w'ᵢ = wᵢ / 2 if aᵢₑ / wₑ is even and aᵢₑ / wᵢ is odd, and w'ᵢ = wᵢ otherwise;
• g'ᵢ = (wᵢ / w'ᵢ) (gᵢ - 1) + 1 + (aᵢₑ² - wₑaᵢₑ) / (2w'ᵢwₑ).

All divisions are exact, and the choice of w'ᵢ is exactly what makes g'ᵢ a nonnegative integer. The contraction has the same signed genus as T.

Main definitions

• TauCeti.NumericalType.contract: the numerical type obtained by contracting a (-1)-index.

Main results

• TauCeti.NumericalType.contractGenus_eq: the formula for g'ᵢ above.
• TauCeti.NumericalType.genusContribution_contract: the genus contribution of a remaining component drops by mᵢaᵢₑ / 2.
• TauCeti.NumericalType.arithmeticGenus_contract: contracting a (-1)-index does not change the signed genus.

References

Stacks, Lemma 55.3.9. The weight condition is stated here without divisions: aᵢₑ / wₑ is even exactly when 2wₑ ∣ aᵢₑ, and aᵢₑ / wᵢ is odd exactly when 2wᵢ ∤ aᵢₑ.

Arithmetic of the contracted data

def TauCeti.NumericalType.ContractHalvesWeight {T : NumericalType} (e : T.Component) (i : { i : T.Component // i ≠ e }) : Prop

The condition under which contracting the (-1)-index e halves the weight of the component i: aᵢₑ / wₑ is even and aᵢₑ / wᵢ is odd.

Equations

• TauCeti.NumericalType.ContractHalvesWeight e i = (2 * ↑↑(T.weight e) ∣ T.intersection (↑i) e ∧ ¬2 * ↑↑(T.weight ↑i) ∣ T.intersection (↑i) e)

@[instance_reducible]

instance TauCeti.NumericalType.instDecidableContractHalvesWeight {T : NumericalType} (e : T.Component) (i : { i : T.Component // i ≠ e }) : Decidable (ContractHalvesWeight e i)

Equations

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

theorem TauCeti.NumericalType.ContractHalvesWeight.two_dvd_weight {T : NumericalType} {e : T.Component} {i : { i : T.Component // i ≠ e }} (h : ContractHalvesWeight e i) : 2 ∣ ↑(T.weight ↑i)

The weight of a component whose weight is halved by the contraction is even.

def TauCeti.NumericalType.contractWeight {T : NumericalType} (e : T.Component) (i : { i : T.Component // i ≠ e }) : ℕ+

The weight w'ᵢ of a component i after contracting the (-1)-index e.

Equations

• TauCeti.NumericalType.contractWeight e i = if h : TauCeti.NumericalType.ContractHalvesWeight e i then ⟨↑(T.weight ↑i) / 2, ⋯⟩ else T.weight ↑i

theorem TauCeti.NumericalType.two_mul_contractWeight {T : NumericalType} {e : T.Component} {i : { i : T.Component // i ≠ e }} (h : ContractHalvesWeight e i) : 2 * ↑↑(contractWeight e i) = ↑↑(T.weight ↑i)

A halved weight is half of the original weight.

@[simp]

theorem TauCeti.NumericalType.contractWeight_of_not {T : NumericalType} {e : T.Component} {i : { i : T.Component // i ≠ e }} (h : ¬ContractHalvesWeight e i) : contractWeight e i = T.weight ↑i

A weight that is not halved is unchanged.

theorem TauCeti.NumericalType.contractWeight_dvd_weight {T : NumericalType} {e : T.Component} (i : { i : T.Component // i ≠ e }) : ↑↑(contractWeight e i) ∣ ↑↑(T.weight ↑i)

The contracted weight divides the original weight.

def TauCeti.NumericalType.contractGenus {T : NumericalType} (e : T.Component) (i : { i : T.Component // i ≠ e }) : ℕ

The genus g'ᵢ of a component i after contracting the (-1)-index e.

Equations

• TauCeti.NumericalType.contractGenus e i = (TauCeti.NumericalType.contractGenusNumerator✝ e i / (2 * ↑↑(TauCeti.NumericalType.contractWeight e i)) + 1).toNat

theorem TauCeti.NumericalType.contractGenus_eq {T : NumericalType} {e : T.Component} {i : { i : T.Component // i ≠ e }} : ↑(contractGenus e i) = ↑↑(T.weight ↑i) / ↑↑(contractWeight e i) * (↑(T.genus ↑i) - 1) + 1 + (↑(T.intersection (↑i) e) ^ 2 - ↑↑(T.weight e) * ↑(T.intersection (↑i) e)) / (2 * ↑↑(contractWeight e i) * ↑↑(T.weight e))

The genus of a component other than e after contracting e, in the form of Stacks, Lemma 55.3.9: g'ᵢ = (wᵢ / w'ᵢ) (gᵢ - 1) + 1 + (aᵢₑ² - wₑaᵢₑ) / (2w'ᵢwₑ).

Intersection numbers

def TauCeti.NumericalType.contractIntersection {T : NumericalType} (e : T.Component) : Matrix { i : T.Component // i ≠ e } { i : T.Component // i ≠ e } ℤ

The intersection matrix a'ᵢⱼ = aᵢⱼ - aᵢₑaⱼₑ / aₑₑ on the components other than e, after contracting the (-1)-index e. Since aₑₑ = -wₑ it is written aᵢⱼ + aᵢₑaⱼₑ / wₑ.

Equations

• TauCeti.NumericalType.contractIntersection e i j = T.intersection ↑i ↑j + T.intersection (↑i) e * T.intersection (↑j) e / ↑↑(T.weight e)

@[simp]

theorem TauCeti.NumericalType.contractIntersection_apply {T : NumericalType} {e : T.Component} (i j : { i : T.Component // i ≠ e }) : contractIntersection e i j = T.intersection ↑i ↑j + T.intersection (↑i) e * T.intersection (↑j) e / ↑↑(T.weight e)

Unfolding of TauCeti.NumericalType.contractIntersection.

theorem TauCeti.NumericalType.weight_mul_contractIntersection {T : NumericalType} {e : T.Component} (i j : { i : T.Component // i ≠ e }) : ↑↑(T.weight e) * contractIntersection e i j = ↑↑(T.weight e) * T.intersection ↑i ↑j + T.intersection (↑i) e * T.intersection (↑j) e

The contracted intersection numbers with the exact division by wₑ cleared.

theorem TauCeti.NumericalType.contractIntersection_isSymm {T : NumericalType} {e : T.Component} : (contractIntersection e).IsSymm

The contracted intersection matrix is symmetric.

theorem TauCeti.NumericalType.intersection_le_contractIntersection {T : NumericalType} {e : T.Component} (i j : { i : T.Component // i ≠ e }) : T.intersection ↑i ↑j ≤ contractIntersection e i j

Contracting e does not decrease the intersection number of two components other than e.

theorem TauCeti.NumericalType.contractIntersection_pos {T : NumericalType} {e : T.Component} {i j : { i : T.Component // i ≠ e }} (hij : i ≠ j) (hi : 0 < T.intersection (↑i) e) (hj : 0 < T.intersection (↑j) e) : 0 < contractIntersection e i j

Two distinct components both meeting e meet after contracting e.

theorem TauCeti.NumericalType.exists_contractIntersection_pos {T : NumericalType} {e : T.Component} (s : Set { i : T.Component // i ≠ e }) (hne : s.Nonempty) (hs : s ≠ Set.univ) : ∃ i ∈ s, ∃ j ∉ s, i ≠ j ∧ 0 < contractIntersection e i j

The no-disconnected-cut condition for the contracted intersection numbers: every nonempty proper set of components other than e meets its complement after contracting e.

theorem TauCeti.NumericalType.sum_multiplicity_mul_contractIntersection {T : NumericalType} {e : T.Component} (he : T.intersection e e = -↑↑(T.weight e)) (i : { i : T.Component // i ≠ e }) : ∑ j : { i : T.Component // i ≠ e }, ↑↑(T.multiplicity ↑j) * contractIntersection e i j = 0

The contracted intersection matrix kills the multiplicity vector: the fibre relation.

The contracted numerical type

def TauCeti.NumericalType.contract (T : NumericalType) {e : T.Component} (he : T.IsMinusOneIndex e) : NumericalType

The numerical type obtained by contracting a (-1)-index e of a numerical type T (Stacks, Lemma 55.3.9).

Its components are those of T other than e, with the same multiplicities, intersection matrix TauCeti.NumericalType.contractIntersection, weights TauCeti.NumericalType.contractWeight and genera TauCeti.NumericalType.contractGenus. On a proper regular model, it is the numerical type of the model obtained by contracting the exceptional curve corresponding to e.

Equations

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

@[simp]

theorem TauCeti.NumericalType.contract_multiplicity {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i : { i : T.Component // i ≠ e }) : (T.contract he).multiplicity i = T.multiplicity ↑i

@[simp]

theorem TauCeti.NumericalType.contract_weight {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i : { i : T.Component // i ≠ e }) : (T.contract he).weight i = contractWeight e i

@[simp]

theorem TauCeti.NumericalType.contract_intersection {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i j : { i : T.Component // i ≠ e }) : (T.contract he).intersection i j = contractIntersection e i j

@[simp]

theorem TauCeti.NumericalType.contract_genus {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i : { i : T.Component // i ≠ e }) : (T.contract he).genus i = contractGenus e i

theorem TauCeti.NumericalType.genusContribution_contract {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) (i : { i : T.Component // i ≠ e }) : (T.contract he).genusContribution i = T.genusContribution ↑i - ↑↑(T.multiplicity ↑i) * ↑(T.intersection (↑i) e) / 2

Contracting e lowers the genus contribution of every remaining component i by mᵢaᵢₑ / 2.

theorem TauCeti.NumericalType.arithmeticGenus_contract {T : NumericalType} {e : T.Component} (he : T.IsMinusOneIndex e) : (T.contract he).arithmeticGenus = T.arithmeticGenus

Contracting a (-1)-index does not change the signed genus (Stacks, Lemma 55.3.9).

A worked example