The simple unit

Lemma 3.4 of the accompanying paper: the arity-zero Hom space of an edge-rank-bounded parameter is spanned by the class of the empty fragment, which is nonzero — End(𝟙) = ℂ·[∅]. The rank bound at arity zero caps the dimension at one, and the empty class is nonzero because its closure row at the empty fragment is f(∅) = 1.

noncomputable def RS.emptyClass (f : ClosedFragment → ℂ) : HomSpace f 0

The class of the empty fragment in the arity-zero Hom space.

Equations

• RS.emptyClass f = RS.HomSpace.ofFragment f RS.emptyClosedFragment

theorem RS.connectionPairing_zero {R : ℕ} (f : EdgeRankParameter R) (F G : ClosedFragment) : connectionPairing f.val 0 F G = f.val (F.union G)

The arity-zero connection pairing is the parameter of the union.

theorem RS.emptyClass_ne_zero {R : ℕ} (f : EdgeRankParameter R) : emptyClass f.val ≠ 0

The empty class is nonzero.

theorem RS.homSpace_zero_spanned {R : ℕ} (f : EdgeRankParameter R) (u : HomSpace f.val 0) : ∃ (c : ℂ), u = c • emptyClass f.val

The simple unit (accompanying paper, Lemma 3.4): the arity-zero Hom space is spanned by the class of the empty fragment.