Ancestor correlators

Ancestor correlators multiply a CohFT class by powers of stable-curve psi classes and integrate the resulting class.

def AxiomaticGW.CohFT.multiplyPsi {R : Type u} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (P : PsiClasses C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) : (C.H g S).carrier →ₗ[R] (C.H g S).carrier

Multiplication by a fixed stable-curve psi monomial.

Equations

• AxiomaticGW.CohFT.multiplyPsi P g S h k = { toFun := fun (x : (C.H g S).carrier) => x * P.monomial g S h k, map_add' := ⋯, map_smul' := ⋯ }

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

Numerical ancestor correlator with cotangent powers k.

Equations

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

@[simp]

theorem AxiomaticGW.CohFT.ancestor_apply {R V : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {C : StableCurveCohomology R} (Ω : CohFT R V C) (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (k : S → ℕ) (a : S → V) : (Ω.ancestor P I g S h k) a = (I.integrate g S h) ((Ω.omega g S h) a * P.monomial g S h k)

theorem AxiomaticGW.CohFT.ancestor_zero_apply {R V : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {C : StableCurveCohomology R} (Ω : CohFT R V C) (P : PsiClasses C) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (a : S → V) : (Ω.ancestor P I g S h fun (x : S) => 0) a = (I.integrate g S h) ((Ω.omega g S h) a)

theorem AxiomaticGW.CohFT.ancestor_domDomCongr {R V : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {C : StableCurveCohomology R} (Ω : CohFT R V C) (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 → ℕ) : MultilinearMap.domDomCongr e (Ω.ancestor P I g S hS k) = Ω.ancestor P I g T hT fun (t : T) => k (e.symm t)

Ancestor correlators are invariant under simultaneous relabelling of markings, insertion powers, and state-space inputs.

def AxiomaticGW.constantStableCurveCohomology.psiClasses (R : Type u) [CommRing R] [Algebra ℚ R] : PsiClasses (constantStableCurveCohomology R)

The constant target has zero cotangent-line classes.

Equations

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

def AxiomaticGW.constantStableCurveCohomology.integrate (R : Type u) [CommRing R] (g : ℕ) (S : Type) [Fintype S] : R →ₗ[R] R

Integration in the constant target is the identity exactly in complex dimension zero and is zero otherwise.

Equations

• AxiomaticGW.constantStableCurveCohomology.integrate R g S = if AxiomaticGW.StableArity.dimension g S = 0 then LinearMap.id else 0

@[simp]

theorem AxiomaticGW.constantStableCurveCohomology.integrate_zero_fin_three (R : Type u) [CommRing R] : integrate R 0 (Fin 3) = LinearMap.id

def AxiomaticGW.constantStableCurveCohomology.integration (R : Type u) [CommRing R] [Algebra ℚ R] : StableCurveIntegration (constantStableCurveCohomology R)

Top-degree integration for the constant stable-curve target.

Equations

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

def AxiomaticGW.constantStableCurveCohomology.forgetfulPushforward (R : Type u) [CommRing R] [Algebra ℚ R] : ForgetfulPushforward (constantStableCurveCohomology R) (integration R)

Forgetful pushforward in the constant model is zero: its source has one more complex dimension while the model has no positive-degree classes.

Equations

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

def AxiomaticGW.constantStableCurveCohomology.psiForgetFormula (R : Type u) [CommRing R] [Algebra ℚ R] : PsiForgetFormula (psiClasses R)

The constant model has no rational-tail divisor and satisfies the forgetful psi formula trivially.

Equations

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

@[simp]

theorem AxiomaticGW.constantStableCurveCohomology.kappa_eq_zero (R : Type u) [CommRing R] [Algebra ℚ R] (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (m : ℕ) : (psiClasses R).kappa (forgetfulPushforward R) g S h m = 0

theorem AxiomaticGW.TopologicalCohFT.toConstantCohFT_ancestor_zero_three {R V : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (T : TopologicalCohFT R V) (a : Fin 3 → V) : (T.toConstantCohFT.ancestor (constantStableCurveCohomology.psiClasses R) (constantStableCurveCohomology.integration R) 0 (Fin 3) StableArity.zero_fin_three fun (x : Fin 3) => 0) a = (T.omega 0 (Fin 3) StableArity.zero_fin_three) a

In the constant model, the zero-power genus-zero three-point ancestor is the original topological correlator.