Documentation

TauCeti.AlgebraicGeometry.Curves.StableReduction.NumericalType.Genus.Zero

Minimal numerical types of genus zero #

This file classifies minimal numerical types of arithmetic genus zero. There is only one, up to equivalence: it has one component, of multiplicity one, weight one, and component genus zero. Its intersection matrix is necessarily zero.

The one-component genus formula is

g(T) = 1 + mᵢwᵢ(gᵢ - 1).

Thus genus zero forces gᵢ = 0 and mᵢwᵢ = 1, hence mᵢ = wᵢ = 1. Conversely these data have genus zero. A minimal numerical type with more than one component has arithmetic genus at least one, so the one-component calculation gives the full classification.

Main definitions #

Main results #

References #

The classification is Stacks, Lemma 55.6.1 in the chapter Semistable Reduction.

source
def TauCeti.NumericalType.genusZeroType :
NumericalType

The canonical minimal numerical type of arithmetic genus zero: one component, with multiplicity and weight one, component genus zero, and zero intersection matrix.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.NumericalType.card_genusZeroType_component :
    Fintype.card genusZeroType.Component = 1

    The canonical genus-zero type has one component.

    source
    @[simp]
    theorem TauCeti.NumericalType.genusZeroType_multiplicity (i : genusZeroType.Component) :
    genusZeroType.multiplicity i = 1

    The multiplicity of the component of the canonical genus-zero type is one.

    source
    @[simp]
    theorem TauCeti.NumericalType.genusZeroType_weight (i : genusZeroType.Component) :
    genusZeroType.weight i = 1

    The weight of the component of the canonical genus-zero type is one.

    source
    @[simp]
    theorem TauCeti.NumericalType.genusZeroType_intersection (i j : genusZeroType.Component) :
    genusZeroType.intersection i j = 0

    Every intersection number of the canonical genus-zero type is zero.

    source
    @[simp]
    theorem TauCeti.NumericalType.genusZeroType_genus (i : genusZeroType.Component) :
    genusZeroType.genus i = 0

    The component of the canonical genus-zero type has genus zero.

    source
    theorem TauCeti.NumericalType.arithmeticGenus_eq_zero_iff_of_card_eq_one {T : NumericalType} (h : Fintype.card T.Component = 1) (i : T.Component) :
    T.arithmeticGenus = 0 ↔ T.multiplicity i = 1 ∧ T.weight i = 1 ∧ T.genus i = 0

    A numerical type with a single component i has arithmetic genus zero exactly when i has multiplicity one, weight one, and component genus zero.

    source
    theorem TauCeti.NumericalType.isMinimal_and_arithmeticGenus_eq_zero_iff {T : NumericalType} :
    T.IsMinimal ∧ T.arithmeticGenus = 0 ↔ Fintype.card T.Component = 1 ∧ ∀ (i : T.Component), T.multiplicity i = 1 ∧ T.weight i = 1 ∧ T.genus i = 0

    Classification of minimal numerical types of genus zero. A numerical type is minimal and has arithmetic genus zero exactly when it has one component, whose multiplicity and weight are one and whose component genus is zero.

    source
    @[simp]
    theorem TauCeti.NumericalType.isMinimal_genusZeroType :
    genusZeroType.IsMinimal

    The canonical genus-zero numerical type is minimal.

    source
    @[simp]
    theorem TauCeti.NumericalType.genusZeroType_arithmeticGenus :
    genusZeroType.arithmeticGenus = 0

    The canonical genus-zero numerical type has arithmetic genus zero.

    source
    theorem TauCeti.NumericalType.nonempty_equiv_genusZeroType_iff {T : NumericalType} :
    Nonempty (T.Equiv genusZeroType) ↔ T.IsMinimal ∧ T.arithmeticGenus = 0

    A numerical type is equivalent to the canonical genus-zero type exactly when it is minimal and has arithmetic genus zero. This is the uniqueness-up-to-equivalence form of the genus-zero classification.