Hom spaces of the skein category

The morphism spaces of the skein category of a graph parameter: the free complex module on the t-fragments, quotiented by the kernel of the full-closure pairing. The edge-rank hypothesis bounds their rank through the first isomorphism theorem: the quotient by the kernel is equivalent to the range of the pairing map.

noncomputable def RS.HomSpace (f : ClosedFragment → ℂ) (t : ℕ) : Type 1

The Hom space of the skein category at arity t: the free module on t-fragments modulo the kernel of the connection pairing.

Equations

• RS.HomSpace f t = ((RS.Fragment (Fin t) →₀ ℂ) ⧸ (RS.connectionMap f t).ker)

@[instance_reducible]

noncomputable instance RS.instAddCommGroupHomSpace (f : ClosedFragment → ℂ) (t : ℕ) : AddCommGroup (HomSpace f t)

Hom spaces are abelian groups, being quotients of free modules.

Equations

• RS.instAddCommGroupHomSpace f t = Submodule.Quotient.addCommGroup (RS.connectionMap f t).ker

@[instance_reducible]

noncomputable instance RS.instModuleComplexHomSpace (f : ClosedFragment → ℂ) (t : ℕ) : Module ℂ (HomSpace f t)

And ℂ-modules.

Equations

• RS.instModuleComplexHomSpace f t = Submodule.Quotient.module (RS.connectionMap f t).ker

noncomputable def RS.HomSpace.ofFragment (f : ClosedFragment → ℂ) {t : ℕ} (F : Fragment (Fin t)) : HomSpace f t

The class of a single fragment in the Hom space.

Equations

• RS.HomSpace.ofFragment f F = Submodule.Quotient.mk (Finsupp.single F 1)

noncomputable def RS.HomSpace.equivRange (f : ClosedFragment → ℂ) (t : ℕ) : HomSpace f t ≃ₗ[ℂ] ↥(connectionMap f t).range

The Hom space embeds in the range of the connection pairing.

Equations

• RS.HomSpace.equivRange f t = (RS.connectionMap f t).quotKerEquivRange

theorem RS.HomSpace.rank_le {R : ℕ} (f : EdgeRankParameter R) (t : ℕ) : Module.rank ℂ (HomSpace f.val t) ≤ ↑R ^ t

The Hom-space dimension bound: the edge-rank hypothesis caps the rank of every Hom space at R ^ t.