Connection ranks as skein dimensions

The first isomorphism theorem identifies the connection-map range with the skein Hom space. At even arity this is the endomorphism algebra used by the commutant estimate.

theorem RS.connectionRank_eq_homSpace_finrank (f : ClosedFragment → ℂ) (t : ℕ) : connectionRank f t = Module.finrank ℂ (HomSpace f t)

The connection rank is the dimension of the corresponding skein Hom space.

theorem RS.connectionRank_eq_skeinEnd_finrank {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : connectionRank f.val (2 * n) = Module.finrank ℂ (skeinEnd f n)

At even arity, connection rank is the dimension of the endomorphism algebra on half as many strands.

theorem RS.connectionRank_cast_eq_rank {R : ℕ} (f : EdgeRankParameter R) (t : ℕ) : ↑(connectionRank f.val t) = Module.rank ℂ ↥(connectionMap f.val t).range

Under the edge-rank hypothesis, natural connection rank agrees with the actual module rank of the connection-map range.

theorem RS.connectionRank_le_pow {f : ClosedFragment → ℂ} {B : ℕ} (h : EdgeRankBounded f B) (t : ℕ) : connectionRank f t ≤ B ^ t

The natural connection ranks satisfy every edge-rank bound of the parameter, independently of its original packaged base.