The point target and intersections on stable-curve moduli

For a point target the state space is the coefficient ring, the primary class is the unit class, and ancestors are exactly psi-class intersection numbers on Mbar(g,S). The final definition states the all-genus DVV recursion as the additional tautological relation that a geometric stable-curve model must prove; it is not derivable from the primitive psi pullback rules alone.

noncomputable def AxiomaticGW.PointTarget.primaryClass {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (g : ℕ) (S : Type) [Fintype S] (_h : StableArity g S) : MultilinearMap R (fun (x : S) => R) (C.H g S).carrier

The point-target primary class. Its scalar value is the product of all state-space inputs, embedded as a degree-zero stable-curve class.

Equations

• AxiomaticGW.PointTarget.primaryClass g S _h = (Algebra.linearMap R (C.H g S).carrier).compMultilinearMap ((AxiomaticGW.CommFrobeniusAlgebra.baseRing R).correlator g S)

@[simp]

theorem AxiomaticGW.PointTarget.primaryClass_apply {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (a : S → R) : (primaryClass g S h) a = (algebraMap R (C.H g S).carrier) (∏ s : S, a s)

noncomputable def AxiomaticGW.PointTarget.intersectionNumber {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (k : S → ℕ) : R

A stable point-target psi-class intersection number.

Equations

• AxiomaticGW.PointTarget.intersectionNumber P I g S k = if h : AxiomaticGW.StableArity g S then (I.integrate g S h) (P.monomial g S h k) else 0

@[simp]

theorem AxiomaticGW.PointTarget.intersectionNumber_of_stable {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) : intersectionNumber P I g S k = (I.integrate g S h) (P.monomial g S h k)

@[simp]

theorem AxiomaticGW.PointTarget.intersectionNumber_of_unstable {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : ¬StableArity g S) (k : S → ℕ) : intersectionNumber P I g S k = 0

noncomputable def AxiomaticGW.PointTarget.ancestor {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) : MultilinearMap R (fun (x : S) => R) R

Point-target ancestors: primary inputs multiply the psi-class intersection number.

Equations

• AxiomaticGW.PointTarget.ancestor P I g S h k = (I.integrate g S h).compMultilinearMap ((AxiomaticGW.CohFT.multiplyPsi P g S h k).compMultilinearMap (AxiomaticGW.PointTarget.primaryClass g S h))

@[simp]

theorem AxiomaticGW.PointTarget.ancestor_apply {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) (a : S → R) : (ancestor P I g S h k) a = (∏ s : S, a s) * intersectionNumber P I g S k

theorem AxiomaticGW.PointTarget.intersectionNumber_relabel {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S T : Type) [Fintype S] [Fintype T] (hS : StableArity g S) (hT : StableArity g T) (e : S ≃ T) (k : S → ℕ) : (intersectionNumber P I g T fun (t : T) => k (e.symm t)) = intersectionNumber P I g S k

Relabelling the marked points does not change a point intersection number.

theorem AxiomaticGW.PointTarget.intersectionNumber_eq_zero_of_degree_ne {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) (hne : ∑ s : S, k s ≠ StableArity.dimension g S) : intersectionNumber P I g S k = 0

A point-target psi-class intersection number vanishes unless the psi codimension equals the dimension of Mbar(g,S).

theorem AxiomaticGW.PointTarget.intersectionNumber_zero_three {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (hI : (I.integrate 0 (Fin 3) StableArity.zero_fin_three) 1 = 1) : (intersectionNumber P I 0 (Fin 3) fun (x : Fin 3) => 0) = 1

The normalized zero-dimensional point intersection is <tau_0 tau_0 tau_0>_0 = 1.

theorem AxiomaticGW.PointTarget.genusOne_one_stable : StableArity 1 (Fin 1)

One marked point in genus one is stable.

theorem AxiomaticGW.PointTarget.intersectionNumber_one_one {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) (hI : (I.integrate 1 (Fin 1) genusOne_one_stable) (P.psi 1 (Fin 1) genusOne_one_stable 0) = (algebraMap ℚ R) (1 / 24)) : (intersectionNumber P I 1 (Fin 1) fun (x : Fin 1) => 1) = (algebraMap ℚ R) (1 / 24)

The exceptional initial value needed alongside DVV is <tau_1>_1 = 1/24. The hypothesis isolates the corresponding geometric intersection calculation.

theorem AxiomaticGW.PointTarget.unitClass_wdvv {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (G : GenusZeroGeometry C) : (C.separating 0 0 (Fin 2) (Fin 2) StableArity.zero_option_fin_two StableArity.zero_option_fin_two) ((C.rename 0 (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) ⋯ ⋯ wdvvPermutation) 1) = (C.separating 0 0 (Fin 2) (Fin 2) StableArity.zero_option_fin_two StableArity.zero_option_fin_two) 1

The point primary class passes the Mbar(0,4) WDVV boundary test: both boundary restrictions of the unit class agree.

def AxiomaticGW.PointTarget.oddDoubleFactorial (n : ℕ) : ℕ

The odd double factorial (2n+1)!!.

Equations

• AxiomaticGW.PointTarget.oddDoubleFactorial n = ∏ j ∈ Finset.range (n + 1), (2 * j + 1)

def AxiomaticGW.PointTarget.dvvMergeWeight (k d : ℕ) : ℚ

Coefficient for merging tau_(k+1) with tau_d in the DVV recursion.

Equations

• AxiomaticGW.PointTarget.dvvMergeWeight k d = ↑(AxiomaticGW.PointTarget.oddDoubleFactorial (k + d)) / ↑(if d = 0 then 1 else AxiomaticGW.PointTarget.oddDoubleFactorial (d - 1))

def AxiomaticGW.PointTarget.DVVRecursion {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (I : StableCurveIntegration C) : Prop

The all-genus DVV recursion for point-target psi-class intersections.

The intersection-number definition supplies the unstable value 0; the formula therefore includes stable and unstable splittings uniformly. A geometric model of stable curves should prove this proposition from the DVV tautological relation.

Equations

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