Multiplicativity from the rank bound at arity zero

An edge-rank-bounded parameter is automatically multiplicative over disjoint unions: the arity-zero connection pairing has rank at most one, its row at the empty graph is nonzero (the parameter is normalized there), so every row is a scalar multiple of it, and evaluating at the empty graph identifies the scalar.

noncomputable def RS.ClosedFragment.union (W₁ W₂ : ClosedFragment) : ClosedFragment

Disjoint union of closed fragments.

Equations

• W₁.union W₂ = (RS.Fragment.disjUnion W₁ W₂).relabel (Equiv.equivOfIsEmpty (Fin 0 ⊕ Fin 0) (Fin 0))

noncomputable def RS.connectionRow (f : ClosedFragment → ℂ) (F : Fragment (Fin (0 + 0))) : Fragment (Fin (0 + 0)) → ℂ

The row of the arity-zero connection pairing at a fragment.

Equations

• RS.connectionRow f F = (RS.connectionMap f 0) (Finsupp.single F 1)

theorem RS.connectionRow_apply (f : ClosedFragment → ℂ) (F G : Fragment (Fin (0 + 0))) : connectionRow f F G = f (pairClose F G)

The row at F evaluates to the pairing values.

noncomputable def RS.relabelZeroEquiv (W : Fragment (Fin 0)) (e : Fin 0 ≃ Fin 0) : (W.relabel e).Equiv W

Relabelling a closed fragment along any equivalence of empty label types is trivial.

Equations

• RS.relabelZeroEquiv W e = { flagEquiv := Equiv.refl (W.relabel e).Flag, vertexEquiv := Equiv.refl (W.relabel e).Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.composeZeroEquiv (F G : ClosedFragment) : (Fragment.compose F G).Equiv (F.union G)

Composition at arity zero is the disjoint union, up to equivalence: with no interface labels, no gluing happens, and any two relabellings into the empty label type coincide.

Equations

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

noncomputable def RS.unionEmptyLeftEquiv (G : ClosedFragment) : Fragment.Equiv (emptyClosedFragment.union G) G

Union with the empty fragment on the left.

Equations

• RS.unionEmptyLeftEquiv G = { flagEquiv := Equiv.emptySum Empty G.Flag, vertexEquiv := Equiv.emptySum Empty G.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.unionEmptyRightEquiv (W : ClosedFragment) : Fragment.Equiv (W.union emptyClosedFragment) W

Union with the empty fragment on the right.

Equations

• RS.unionEmptyRightEquiv W = { flagEquiv := Equiv.sumEmpty W.Flag Empty, vertexEquiv := Equiv.sumEmpty W.Vertex Empty, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

theorem RS.EdgeRankParameter.val_union {R : ℕ} (f : EdgeRankParameter R) (W₁ W₂ : ClosedFragment) : f.val (W₁.union W₂) = f.val W₁ * f.val W₂

Multiplicativity from the rank bound (Lemma 3.2): an edge-rank-bounded parameter is multiplicative over disjoint unions of closed fragments.