Minimal numerical types and their genus contributions

The signed genus of a numerical type T is a sum of contributions of its components,

g(T) = 1 + ∑ᵢ Φᵢ, where Φᵢ = mᵢ (wᵢ (gᵢ - 1) - aᵢᵢ / 2).

As soon as T has more than one component, the sign of a single contribution is controlled by the component alone: Φᵢ < 0 exactly when gᵢ = 0 and aᵢᵢ = -wᵢ, a (-1)-index, and Φᵢ = 0 exactly when gᵢ = 0 and aᵢᵢ = -2wᵢ, a (-2)-index. On a proper regular model these are the numerical shadows of exceptional curves of the first kind and of (-2)-curves. A numerical type is minimal when it has no (-1)-index, so that every contribution is nonnegative.

This file develops that analysis and the resulting bounds on minimal numerical types: in a minimal type of genus g with more than one component, there are at most 2g - 2 components that are not (-2)-indices, every component genus is below g, and the multiplicity-weighted self-intersection and pairwise intersection numbers at a component that is not a (-2)-index are at most 6g - 6. These are the first steps of the bound on the multiplicities of a minimal numerical type which, in the Artin–Winters argument, bounds the ℓ-torsion of its Picard group.

Main definitions

• TauCeti.NumericalType.IsMinusOneIndex: gᵢ = 0 and aᵢᵢ = -wᵢ.
• TauCeti.NumericalType.IsMinusTwoIndex: gᵢ = 0 and aᵢᵢ = -2wᵢ.
• TauCeti.NumericalType.IsMinimal: there is no (-1)-index.
• TauCeti.NumericalType.genusContribution: the contribution Φᵢ of a component to the signed genus, a rational number which need not be an integer.

Main results

• TauCeti.NumericalType.arithmeticGenus_eq_one_add_sum_genusContribution: g = 1 + ∑ᵢ Φᵢ.
• TauCeti.NumericalType.genusContribution_neg_iff and TauCeti.NumericalType.genusContribution_eq_zero_iff: with more than one component, the negative contributions are those of the (-1)-indices and the zero contributions those of the (-2)-indices (Stacks, Tag 0C75 and Stacks, Tag 0C7D).
• TauCeti.NumericalType.IsMinimal.one_le_arithmeticGenus: a minimal numerical type with more than one component has genus at least one (Stacks, Tag 0C7B).
• TauCeti.NumericalType.IsMinimal.card_filter_not_isMinusTwoIndex_le, TauCeti.NumericalType.IsMinimal.genus_lt_arithmeticGenus, TauCeti.NumericalType.IsMinimal.multiplicity_mul_abs_intersection_self_le and TauCeti.NumericalType.IsMinimal.multiplicity_mul_intersection_le: the four bounds on a minimal numerical type listed above (Stacks, Tag 0C9V).

References

The statements follow the sections Numerical types and Bounding invariants of numerical types of the Stacks Project chapter on semistable reduction. The bounds of Stacks, Tag 0C9V are stated there for genus at least two; the arguments do not use that hypothesis, and the second bound is stated there only for components that are not (-2)-indices, which is not needed either.

Special indices and minimality

def TauCeti.NumericalType.IsMinusOneIndex (T : NumericalType) (i : T.Component) : Prop

A component of a numerical type is a (-1)-index when its genus is zero and its self-intersection is minus its weight (Stacks, Tag 0C76).

Equations

• T.IsMinusOneIndex i = (T.genus i = 0 ∧ T.intersection i i = -↑↑(T.weight i))

def TauCeti.NumericalType.IsMinusTwoIndex (T : NumericalType) (i : T.Component) : Prop

A component of a numerical type is a (-2)-index when its genus is zero and its self-intersection is minus twice its weight (Stacks, Tag 0C7E).

Equations

• T.IsMinusTwoIndex i = (T.genus i = 0 ∧ T.intersection i i = -(2 * ↑↑(T.weight i)))

def TauCeti.NumericalType.IsMinimal (T : NumericalType) : Prop

A numerical type is minimal when it has no (-1)-index (Stacks, Tag 0C7A).

Equations

• T.IsMinimal = ∀ (i : T.Component), ¬T.IsMinusOneIndex i

theorem TauCeti.NumericalType.isMinusOneIndex_iff (T : NumericalType) {i : T.Component} : T.IsMinusOneIndex i ↔ T.genus i = 0 ∧ T.intersection i i = -↑↑(T.weight i)

Unfolding of TauCeti.NumericalType.IsMinusOneIndex.

theorem TauCeti.NumericalType.isMinusTwoIndex_iff (T : NumericalType) {i : T.Component} : T.IsMinusTwoIndex i ↔ T.genus i = 0 ∧ T.intersection i i = -(2 * ↑↑(T.weight i))

Unfolding of TauCeti.NumericalType.IsMinusTwoIndex.

@[instance_reducible]

instance TauCeti.NumericalType.instDecidablePredComponentIsMinusOneIndex (T : NumericalType) : DecidablePred T.IsMinusOneIndex

Equations

• T.instDecidablePredComponentIsMinusOneIndex x✝ = decidable_of_iff (T.genus x✝ = 0 ∧ T.intersection x✝ x✝ = -↑↑(T.weight x✝)) ⋯

@[instance_reducible]

instance TauCeti.NumericalType.instDecidablePredComponentIsMinusTwoIndex (T : NumericalType) : DecidablePred T.IsMinusTwoIndex

Equations

• T.instDecidablePredComponentIsMinusTwoIndex x✝ = decidable_of_iff (T.genus x✝ = 0 ∧ T.intersection x✝ x✝ = -(2 * ↑↑(T.weight x✝))) ⋯

theorem TauCeti.NumericalType.isMinimal_iff (T : NumericalType) : T.IsMinimal ↔ ∀ (i : T.Component), ¬T.IsMinusOneIndex i

Unfolding of TauCeti.NumericalType.IsMinimal.

@[simp]

theorem TauCeti.NumericalType.isMinusOneIndex_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (i : C) : (T.reindex e).IsMinusOneIndex i ↔ T.IsMinusOneIndex (e.symm i)

Reindexing preserves and reflects (-1)-indices.

@[simp]

theorem TauCeti.NumericalType.isMinusTwoIndex_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (i : C) : (T.reindex e).IsMinusTwoIndex i ↔ T.IsMinusTwoIndex (e.symm i)

Reindexing preserves and reflects (-2)-indices.

@[simp]

theorem TauCeti.NumericalType.isMinimal_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) : (T.reindex e).IsMinimal ↔ T.IsMinimal

Minimality is invariant under reindexing.

theorem TauCeti.NumericalType.IsMinusTwoIndex.not_isMinusOneIndex (T : NumericalType) {i : T.Component} (h : T.IsMinusTwoIndex i) : ¬T.IsMinusOneIndex i

A (-2)-index is not a (-1)-index.

Numerical types with one component

theorem TauCeti.NumericalType.isMinimal_of_card_eq_one (T : NumericalType) (h : Fintype.card T.Component = 1) : T.IsMinimal

A numerical type with a single component is minimal.

theorem TauCeti.NumericalType.IsMinusOneIndex.one_lt_card (T : NumericalType) {i : T.Component} (h : T.IsMinusOneIndex i) : 1 < Fintype.card T.Component

A numerical type with a (-1)-index has more than one component.

Genus contributions

def TauCeti.NumericalType.genusContribution (T : NumericalType) (i : T.Component) : ℚ

The contribution mᵢ (wᵢ (gᵢ - 1) - aᵢᵢ / 2) of a component to the signed genus of a numerical type. It is a half-integer, which need not be an integer.

Equations

• T.genusContribution i = ↑↑(T.multiplicity i) * (↑↑(T.weight i) * (↑(T.genus i) - 1) - ↑(T.intersection i i) / 2)

theorem TauCeti.NumericalType.genusContribution_def (T : NumericalType) (i : T.Component) : T.genusContribution i = ↑↑(T.multiplicity i) * (↑↑(T.weight i) * (↑(T.genus i) - 1) - ↑(T.intersection i i) / 2)

The defining formula of the contribution of a component to the signed genus.

@[simp]

theorem TauCeti.NumericalType.genusContribution_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (i : C) : (T.reindex e).genusContribution i = T.genusContribution (e.symm i)

Genus contributions are invariant under reindexing.

theorem TauCeti.NumericalType.arithmeticGenus_eq_one_add_sum_genusContribution (T : NumericalType) : ↑T.arithmeticGenus = 1 + ∑ i : T.Component, T.genusContribution i

The signed genus is one plus the sum of the contributions of the components.

theorem TauCeti.NumericalType.genusContribution_neg_iff (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : T.genusContribution i < 0 ↔ T.IsMinusOneIndex i

With more than one component, the contribution of a component to the signed genus is negative exactly when it is a (-1)-index (Stacks, Tag 0C75).

theorem TauCeti.NumericalType.genusContribution_eq_zero_iff (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : T.genusContribution i = 0 ↔ T.IsMinusTwoIndex i

With more than one component, the contribution of a component to the signed genus is zero exactly when it is a (-2)-index (Stacks, Tag 0C7D).

theorem TauCeti.NumericalType.genusContribution_nonneg_iff (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : 0 ≤ T.genusContribution i ↔ ¬T.IsMinusOneIndex i

With more than one component, the contribution of a component to the signed genus is nonnegative exactly when it is not a (-1)-index.

theorem TauCeti.NumericalType.one_half_le_genusContribution (T : NumericalType) (h : 1 < Fintype.card T.Component) {i : T.Component} (h₁ : ¬T.IsMinusOneIndex i) (h₂ : ¬T.IsMinusTwoIndex i) : 1 / 2 ≤ T.genusContribution i

With more than one component, a component that is neither a (-1)-index nor a (-2)-index contributes at least 1 / 2 to the signed genus.

Minimal numerical types

theorem TauCeti.NumericalType.IsMinimal.genusContribution_nonneg {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) (i : T.Component) : 0 ≤ T.genusContribution i

In a minimal numerical type with more than one component, every contribution to the signed genus is nonnegative.

theorem TauCeti.NumericalType.IsMinimal.genusContribution_le {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) (i : T.Component) : T.genusContribution i ≤ ↑T.arithmeticGenus - 1

In a minimal numerical type with more than one component, every contribution to the signed genus is at most g - 1.

theorem TauCeti.NumericalType.IsMinimal.one_le_arithmeticGenus {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) : 1 ≤ T.arithmeticGenus

A minimal numerical type with more than one component has signed genus at least one (Stacks, Tag 0C7B).

theorem TauCeti.NumericalType.IsMinimal.card_filter_not_isMinusTwoIndex_le {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) : ↑{i : T.Component | ¬T.IsMinusTwoIndex i}.card ≤ 2 * T.arithmeticGenus - 2

A minimal numerical type of genus g with more than one component has at most 2g - 2 components that are not (-2)-indices.

theorem TauCeti.NumericalType.IsMinimal.genus_lt_arithmeticGenus {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) (i : T.Component) : ↑(T.genus i) < T.arithmeticGenus

In a minimal numerical type with more than one component, every component genus is smaller than the signed genus.

theorem TauCeti.NumericalType.IsMinimal.multiplicity_mul_abs_intersection_self_le {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) {j : T.Component} (hj : ¬T.IsMinusTwoIndex j) : ↑↑(T.multiplicity j) * |T.intersection j j| ≤ 6 * T.arithmeticGenus - 6

In a minimal numerical type of genus g with more than one component, the weighted self-intersection mⱼ|aⱼⱼ| of a component that is not a (-2)-index is at most 6g - 6.

theorem TauCeti.NumericalType.IsMinimal.multiplicity_mul_intersection_le {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) {j : T.Component} (hj : ¬T.IsMinusTwoIndex j) (i : T.Component) : ↑↑(T.multiplicity i) * T.intersection i j ≤ 6 * T.arithmeticGenus - 6

In a minimal numerical type of genus g with more than one component, every multiplicity-weighted intersection number mᵢaᵢⱼ with a component j that is not a (-2)-index is at most 6g - 6.