Documentation

LeanPool.RegtsSevenster.RS.Novel.Skein.SkeinCatInstance

The skein category, packaged #

The accompanying paper's connection category ๐’ž_f as a CategoryTheory.Category instance: objects are arities, morphisms are Hom-space classes, identities are strand bundle classes, composition is the descended bilinear composition. All axioms were proven in SkeinCategory.lean; this file only packages them.

source
structure RS.SkeinObj {R : โ„•} (f : EdgeRankParameter R) :
Type

An object of the skein category of a parameter: an arity.

  • arity : โ„•

    The arity: the number of open ends.

Instances For
    source
    @[instance_reducible]
    noncomputable instance RS.skeinCategory {R : โ„•} (f : EdgeRankParameter R) :
    CategoryTheory.Category.{1, 0} (SkeinObj f)

    The skein category: the accompanying paper's connection category ๐’ž_f (ยง3.2).

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