The composition ideal

Bilinear composition on the free modules of fragments, and the first half of the ideal lemma (accompanying paper, Lemma 3.3(a)): composing a kernel element with any fragment on the right stays in the kernel, because every closure row of the composite is a closure row of the original — the rotation of closures moves the composed factor into the test fragment.

noncomputable def RS.composeFinsupp (m n p : ℕ) : (Fragment (Fin (m + n)) →₀ ℂ) →ₗ[ℂ] (Fragment (Fin (n + p)) →₀ ℂ) →ₗ[ℂ] Fragment (Fin (m + p)) →₀ ℂ

Bilinear composition on the free modules of fragments.

Equations

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

theorem RS.composeFinsupp_single (m n p : ℕ) (F : Fragment (Fin (m + n))) (c : ℂ) (G : Fragment (Fin (n + p))) (d : ℂ) : ((composeFinsupp m n p) (Finsupp.single F c)) (Finsupp.single G d) = Finsupp.single (F.compose G) (c * d)

Composition of weighted single fragments.

theorem RS.connectionMap_single (f : ClosedFragment → ℂ) (t : ℕ) (X : Fragment (Fin t)) (c : ℂ) (G : Fragment (Fin t)) : (connectionMap f t) (Finsupp.single X c) G = c * connectionPairing f t X G

The connection row of a weighted single fragment.

theorem RS.connectionPairing_compose_right (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {m n p : ℕ} (F : Fragment (Fin (m + n))) (H : Fragment (Fin (n + p))) (K : Fragment (Fin (m + p))) : connectionPairing f (m + p) (F.compose H) K = connectionPairing f (m + n) F (K.compose (H.relabel (transposeEquiv n p)))

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

theorem RS.connectionMap_compose_single (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {m n p : ℕ} (x : Fragment (Fin (m + n)) →₀ ℂ) (H : Fragment (Fin (n + p))) (K : Fragment (Fin (m + p))) : (connectionMap f (m + p)) (((composeFinsupp m n p) x) (Finsupp.single H 1)) K = (connectionMap f (m + n)) x (K.compose (H.relabel (transposeEquiv n p)))

The closure row of a right-composite, linearized: each row of x ∘ H is a row of x at a rotated test fragment.

theorem RS.composeFinsupp_single_ker (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {m n p : ℕ} {x : Fragment (Fin (m + n)) →₀ ℂ} (hx : x ∈ (connectionMap f (m + n)).ker) (H : Fragment (Fin (n + p))) : ((composeFinsupp m n p) x) (Finsupp.single H 1) ∈ (connectionMap f (m + p)).ker

The right ideal property (accompanying paper, Lemma 3.3(a), right): a kernel element composed with any single fragment on the right stays in the kernel.

theorem RS.composeFinsupp_ker_left (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {m n p : ℕ} {x : Fragment (Fin (m + n)) →₀ ℂ} (hx : x ∈ (connectionMap f (m + n)).ker) (y : Fragment (Fin (n + p)) →₀ ℂ) : ((composeFinsupp m n p) x) y ∈ (connectionMap f (m + p)).ker

The right ideal property, bilinear form: a kernel element composed with anything on the right stays in the kernel.