Zero negligibles: nondegeneracy of the trace pairing

The accompanying paper's Lemma 3.6: the trace closure of x against a test fragment differs from the defining connection pairing only by the fixed transpose relabeling of the open ends — a bijection on fragments — so the two test families coincide, and an element all of whose traces vanish lies in the pairing kernel.

theorem RS.fragTrace_compose_eq_pairing (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {t u : ℕ} (F : Fragment (Fin (t + u))) (G : Fragment (Fin (u + t))) : fragTrace f (F.compose G) = connectionPairing f (t + u) F (G.relabel (transposeEquiv u t))

The trace of a composition is the connection pairing against the transposed test fragment: the trace closure is the defining pairing up to a relabeling.

theorem RS.connectionMap_eq_trace_row (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {t u : ℕ} (x : Fragment (Fin (t + u)) →₀ ℂ) (H : Fragment (Fin (t + u))) : (connectionMap f (t + u)) x H = (traceFunctional f t) (((composeFinsupp t u t) x) (Finsupp.single (H.relabel (transposeEquiv u t).symm) 1))

Every connection row is a family of traces: the row of x at the test fragment H is the trace of x composed with the un-transposed H.

theorem RS.mem_ker_of_traces_vanish (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {t u : ℕ} (x : Fragment (Fin (t + u)) →₀ ℂ) (hx : ∀ (G : Fragment (Fin (u + t))), (traceFunctional f t) (((composeFinsupp t u t) x) (Finsupp.single G 1)) = 0) : x ∈ (connectionMap f (t + u)).ker

Zero negligibles (accompanying paper, Lemma 3.6): an element all of whose composition traces vanish lies in the pairing kernel.