The skein category: the axioms on Hom spaces

The skein category — the accompanying paper's connection category 𝒞_f (§3.2): identities are strand bundle classes and composition is the descended bilinear composition. Every axiom reduces to a kernel membership of a difference of free-module elements, proven by linear induction with the per-single case supplied by a fragment equivalence (identity laws, associativity) through isomorphism invariance.

theorem RS.mem_ker_single_sub_of_equiv {R : ℕ} (f : EdgeRankParameter R) {t : ℕ} {F G : Fragment (Fin t)} (h : F.Equiv G) : Finsupp.single F 1 - Finsupp.single G 1 ∈ (connectionMap f.val t).ker

The single difference of equivalent fragments lies in the pairing kernel.

theorem RS.HomSpace.ofFragment_congr {R : ℕ} (f : EdgeRankParameter R) {t : ℕ} {F G : Fragment (Fin t)} (h : F.Equiv G) : ofFragment f.val F = ofFragment f.val G

Equivalent fragments have equal classes.

theorem RS.mem_ker_single_sub_of_equiv_smul {R : ℕ} (f : EdgeRankParameter R) {t : ℕ} {F G : Fragment (Fin t)} (h : F.Equiv G) (c : ℂ) : Finsupp.single F c - Finsupp.single G c ∈ (connectionMap f.val t).ker

The single difference of a weighted pair of equivalent fragments lies in the kernel.

theorem RS.mem_ker_id_left {R : ℕ} (f : EdgeRankParameter R) (s u : ℕ) (y : Fragment (Fin (s + u)) →₀ ℂ) : ((composeFinsupp s s u) (Finsupp.single (strandBundle s) 1)) y - y ∈ (connectionMap f.val (s + u)).ker

The left unit difference lies in the kernel.

theorem RS.mem_ker_id_right {R : ℕ} (f : EdgeRankParameter R) (s u : ℕ) (y : Fragment (Fin (s + u)) →₀ ℂ) : ((composeFinsupp s u u) y) (Finsupp.single (strandBundle u) 1) - y ∈ (connectionMap f.val (s + u)).ker

The right unit difference lies in the kernel.

theorem RS.mem_ker_assoc {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (x : Fragment (Fin (s + t)) →₀ ℂ) (y : Fragment (Fin (t + u)) →₀ ℂ) (z : Fragment (Fin (u + v)) →₀ ℂ) : ((composeFinsupp s u v) (((composeFinsupp s t u) x) y)) z - ((composeFinsupp s t v) x) (((composeFinsupp t u v) y) z) ∈ (connectionMap f.val (s + v)).ker

The associativity difference lies in the kernel.

The axioms on quotient classes

theorem RS.HomSpace.comp_id_left {R : ℕ} (f : EdgeRankParameter R) (s u : ℕ) (q : HomSpace f.val (s + u)) : ((comp f s s u) (ofFragment f.val (strandBundle s))) q = q

Left unit law on classes.

theorem RS.HomSpace.comp_id_right {R : ℕ} (f : EdgeRankParameter R) (s u : ℕ) (q : HomSpace f.val (s + u)) : ((comp f s u u) q) (ofFragment f.val (strandBundle u)) = q

Right unit law on classes.

theorem RS.HomSpace.comp_assoc {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (p : HomSpace f.val (s + t)) (q : HomSpace f.val (t + u)) (r : HomSpace f.val (u + v)) : ((comp f s u v) (((comp f s t u) p) q)) r = ((comp f s t v) p) (((comp f t u v) q) r)

Associativity on classes.