The snake identities on Hom classes

The two snake composites of the skein category are the identity class. Both composites are concrete fragments built from strands by tensor and composition, and the entire gluing stack reduces definitionally on concrete data, so the fragment equivalences are established by decide over the two surviving flags, with the inverse flag map given canonically by the boundary-flag function.

noncomputable def RS.snakeFragL : Fragment (Fin (1 + 1))

The left snake fragment (coev ⊗ id) ∘ (id ⊗ ev).

Equations

• RS.snakeFragL = (RS.tensorFragment RS.coevFrag (RS.strandBundle 1)).compose (RS.tensorFragment (RS.strandBundle 1) RS.evFrag)

noncomputable def RS.snakeFragR : Fragment (Fin (1 + 1))

The right snake fragment (id ⊗ coev) ∘ (ev ⊗ id).

Equations

• RS.snakeFragR = (RS.tensorFragment (RS.strandBundle 1) RS.coevFrag).compose (RS.tensorFragment RS.evFrag (RS.strandBundle 1))

noncomputable def RS.snakeFragLEquiv : (strandBundle 1).Equiv snakeFragL

The left snake fragment is the identity strand.

Equations

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

noncomputable def RS.snakeFragREquiv : (strandBundle 1).Equiv snakeFragR

The right snake fragment is the identity strand.

Equations

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

noncomputable def RS.idClass {R : ℕ} (f : EdgeRankParameter R) : HomSpace f.val (1 + 1)

The identity class on one strand.

Equations

• RS.idClass f = RS.HomSpace.ofFragment f.val (RS.strandBundle 1)

theorem RS.snake_left {R : ℕ} (f : EdgeRankParameter R) : ((HomSpace.comp f 1 3 1) (((HomSpace.tensor f 0 2 1 1) (coevClass f)) (idClass f))) (((HomSpace.tensor f 1 1 2 0) (idClass f)) (evClass f)) = idClass f

The left snake identity on Hom classes.

theorem RS.snake_right {R : ℕ} (f : EdgeRankParameter R) : ((HomSpace.comp f 1 3 1) (((HomSpace.tensor f 1 1 0 2) (idClass f)) (coevClass f))) (((HomSpace.tensor f 2 0 1 1) (evClass f)) (idClass f)) = idClass f

The right snake identity on Hom classes.