The composition ideal, left half

The mirror of SkeinIdeal.lean: composing a kernel element with any fragment on the left stays in the kernel, because every closure row of w ∘ x is a closure row of x — the mirror rotation moves the left factor into the test fragment. Together with composeFinsupp_ker_left this makes the pairing kernel a two-sided ideal (accompanying paper, Lemma 3.3(a)), so composition descends to the Hom spaces.

theorem RS.connectionPairing_compose_left (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u : ℕ} (W : Fragment (Fin (s + t))) (F : Fragment (Fin (t + u))) (K : Fragment (Fin (s + u))) : connectionPairing f (s + u) (W.compose F) K = connectionPairing f (t + u) F ((W.relabel (transposeEquiv s t)).compose K)

Rotation of connection rows, left (accompanying paper, Lemma 3.3(a), left): for an isomorphism-invariant parameter, the closure row of a left-composite is a closure row of the original.

theorem RS.connectionMap_compose_left_single (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u : ℕ} (W : Fragment (Fin (s + t))) (y : Fragment (Fin (t + u)) →₀ ℂ) (K : Fragment (Fin (s + u))) : (connectionMap f (s + u)) (((composeFinsupp s t u) (Finsupp.single W 1)) y) K = (connectionMap f (t + u)) y ((W.relabel (transposeEquiv s t)).compose K)

The closure row of a left-composite, linearized: each row of W ∘ y is a row of y at a rotated test fragment.

theorem RS.composeFinsupp_single_ker_left (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u : ℕ} (W : Fragment (Fin (s + t))) {y : Fragment (Fin (t + u)) →₀ ℂ} (hy : y ∈ (connectionMap f (t + u)).ker) : ((composeFinsupp s t u) (Finsupp.single W 1)) y ∈ (connectionMap f (s + u)).ker

A kernel element composed with a single fragment on the left stays in the kernel.

theorem RS.composeFinsupp_ker_right (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u : ℕ} (x : Fragment (Fin (s + t)) →₀ ℂ) {y : Fragment (Fin (t + u)) →₀ ℂ} (hy : y ∈ (connectionMap f (t + u)).ker) : ((composeFinsupp s t u) x) y ∈ (connectionMap f (s + u)).ker

The left ideal property (accompanying paper, Lemma 3.3(a), left): anything composed with a kernel element on the left stays in the kernel.