Two-dimensional topological field theories

TwoDimensionalTFT is the finite-labelled correlator presentation of a closed oriented two-dimensional topological field theory. It records scalar correlators, their unit, and their one-edge sewing laws. The equivalent symmetric-monoidal-functor presentation is not constructed here.

Correlators are provided for all genera and all finite label types, including unstable arities. This makes the counit, metric, and multiplication visible as low-arity operations and permits a later restriction to stable CohFT arities.

structure AxiomaticGW.TwoDimensionalTFT (R : Type u_1) (V : Type u_2) [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] : Type (max (max 1 u_1) u_2)

A closed oriented two-dimensional TFT in its finite-labelled correlator presentation.

• pairing : SymmetricPerfectPairing R V

  The metric used to contract the two half-edges of a node.

• unit : V

  The distinguished unit state.

• correlator (g : ℕ) (S : Type) [Fintype S] : MultilinearMap R (fun (x : S) => V) R

  The connected genus-g correlator with label type S.

• relabel (g : ℕ) (S T : Type) [Fintype S] [Fintype T] (e : S ≃ T) : MultilinearMap.domDomCongr e (self.correlator g S) = self.correlator g T

  Correlators are natural under equivalences of finite label types.

• unit_insert (g : ℕ) (S : Type) [Fintype S] (a : S → V) : ((self.correlator g (Option S)) fun (x : Option S) => match x with | none => self.unit | some s => a s) = (self.correlator g S) a

  Inserting the distinguished unit at a new marking changes no correlator.

• nonseparating (g : ℕ) (S : Type) [Fintype S] : self.pairing.selfContract (self.correlator g (S ⊕ Fin 2)) = self.correlator (g + 1) S

  Contracting two markings on one connected component adds a handle.

• separating (g₁ g₂ : ℕ) (S T : Type) [Fintype S] [Fintype T] : self.pairing.pairContract (self.correlator g₁ (Option S)) (self.correlator g₂ (Option T)) = self.correlator (g₁ + g₂) (S ⊕ T)

  Contracting one marking on each of two components joins them.

• normalization (a : Fin 2 → V) : (self.correlator 0 (Fin 2)) a = (self.pairing.form (a 0)) (a 1)

  The genus-zero two-point correlator is the metric.

def AxiomaticGW.TwoDimensionalTFT.counit {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (T : TwoDimensionalTFT R V) : V →ₗ[R] R

The genus-zero one-point correlator of a theory, used below as its candidate Frobenius counit.

Equations

• T.counit = ↑(MultilinearMap.ofSubsingletonₗ R R V R 0).symm (T.correlator 0 (Fin 1))

@[simp]

theorem AxiomaticGW.TwoDimensionalTFT.counit_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (T : TwoDimensionalTFT R V) (x : V) : T.counit x = (T.correlator 0 (Fin 1)) fun (x_1 : Fin 1) => x

Evaluation of the counit extracted from the one-point correlator.