Free circles as scalars

A fragment with extra free circles is the tensor with a circles-only closed fragment; on Hom classes the circles split off as the power of the circle value. This is the accompanying paper's "free circles are carried by multiplicativity" discipline, at class level.

noncomputable def RS.circleVal {R : ℕ} (f : EdgeRankParameter R) : ℂ

The circle value of a parameter.

Equations

• RS.circleVal f = f.val (RS.circlesClosed 1)

def RS.addCircles {α : Type} (X : Fragment α) (c : ℕ) : Fragment α

Adding free circles to a fragment.

Equations

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

noncomputable def RS.addCirclesTensor {s t : ℕ} (X : Fragment (Fin (s + t))) (c : ℕ) : (tensorFragment X (circlesClosed c)).Equiv ((addCircles X c).relabel (finCongr ⋯))

Adding circles is tensoring with a circles-only fragment.

Equations

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

noncomputable def RS.circlesClosedUnion (a b : ℕ) : Fragment.Equiv ((circlesClosed a).union (circlesClosed b)) (circlesClosed (a + b))

The union of circle fragments adds the counts.

Equations

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

theorem RS.circlesClosed_val {R : ℕ} (f : EdgeRankParameter R) (c : ℕ) : f.val (circlesClosed c) = circleVal f ^ c

The circle value of c circles is the c-th power.

theorem RS.ofFragment_relabel_unitcast {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (Y : Fragment (Fin (s + t))) : HomSpace.ofFragment f.val (Y.relabel (finCongr ⋯)) = HomSpace.ofFragment f.val Y

Relabelling by the unit-padding cast fixes the class.

theorem RS.ofFragment_tensor_circles {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (X : Fragment (Fin (s + t))) (c : ℕ) : HomSpace.ofFragment f.val (tensorFragment X (circlesClosed c)) = circleVal f ^ c • HomSpace.ofFragment f.val (X.relabel (finCongr ⋯))

The class-level circle split, at the padded arity: the tensor with a circles-only fragment is the circle power times the padded class.