Lemma 6.4 as stated

lem:split-positive-deformation (positive-deformations.tex): "S lifts to a unital subalgebra of B, and the filtration of B splits as S-bimodules. The resulting identification of B with Λ as filtered vector spaces induces the prescribed identification gr B = Λ, and the multiplication of B becomes μ₀ + Σ_{q>0} μ_q, where μ₀ is the multiplication of Λ and each μ_q raises internal degree by q, is S-relative, and vanishes when an input belongs to S."

For S = Λ₀ with its vertex idempotents (Vertices): the splitting of exists_split is S-bilinear on both sides, so the transported product is S-relative (star_s_*) and each μ_q, q > 0, is a normalized S-relative cochain (μ_isRelS), and the statement is assembled in splitPositiveDeformation.

theorem MultiplicativeBasisDeformations.PosFiltration.proj_hom_mul' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {m : ℕ} {e : Λ} (he : G.IsHom m e) (a : Λ) (d : ℕ) : (G.proj (m + d)) (e * a) = e * (G.proj d) a

theorem MultiplicativeBasisDeformations.PosFiltration.proj_mul_hom' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {m : ℕ} {e : Λ} (he : G.IsHom m e) (a : Λ) (d : ℕ) : (G.proj (d + m)) (a * e) = (G.proj d) a * e

def MultiplicativeBasisDeformations.PosFiltration.IsRelS {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Prop

S-relative and normalized, for S = Λ₀: μ(sa, b) = sμ(a, b), μ(as, b) = μ(a, sb), μ(a, bs) = μ(a, b)s, and μ vanishes when an input belongs to S.

theorem MultiplicativeBasisDeformations.PosFiltration.IsRelS.isRel₂ {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (h : IsRelS G μ) : LenGrading.IsRel₂ V μ

theorem MultiplicativeBasisDeformations.PosFiltration.Split.star_s_left {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hl : ∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) {s : Λ} (hs : G.IsHom 0 s) (a b : Λ) : (S.star (s * a)) b = s * (S.star a) b

theorem MultiplicativeBasisDeformations.PosFiltration.Split.star_s_mid {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hl : ∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) (hr : ∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) {s : Λ} (hs : G.IsHom 0 s) (a b : Λ) : (S.star (a * s)) b = (S.star a) (s * b)

theorem MultiplicativeBasisDeformations.PosFiltration.Split.star_s_right {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hr : ∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) {s : Λ} (hs : G.IsHom 0 s) (a b : Λ) : (S.star a) (b * s) = (S.star a) b * s

theorem MultiplicativeBasisDeformations.PosFiltration.Split.star_s_unit_left {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hl : ∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) {s : Λ} (hs : G.IsHom 0 s) (b : Λ) : (S.star s) b = s * b

theorem MultiplicativeBasisDeformations.PosFiltration.Split.star_s_unit_right {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hr : ∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) {s : Λ} (hs : G.IsHom 0 s) (a : Λ) : (S.star a) s = a * s

theorem MultiplicativeBasisDeformations.PosFiltration.Split.bilin_eq {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {f g : Λ →ₗ[k] Λ →ₗ[k] Λ} (h : ∀ (d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → (f a) b = (g a) b) : f = g

Bilinear maps agreeing on homogeneous pairs agree.

theorem MultiplicativeBasisDeformations.PosFiltration.Split.lin_eq {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {f g : Λ →ₗ[k] Λ} (h : ∀ (d : ℕ) (a : Λ), G.IsHom d a → f a = g a) : f = g

Linear maps agreeing on homogeneous elements agree.

theorem MultiplicativeBasisDeformations.PosFiltration.Split.μ_isRelS {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (S : P.Split) (hl : ∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) (hr : ∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) {q : ℕ} (hq : 0 < q) : IsRelS G (S.μ q)

Each μ_q, q > 0, is a normalized S-relative cochain, for S = Λ₀, when the splitting is S-bilinear.

theorem MultiplicativeBasisDeformations.PosFiltration.splitPositiveDeformation {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (V : G.Vertices) : ∃ (S : P.Split), (CompleteOrthogonalIdempotents fun (i : Fin V.n) => S.φ (V.e i)) ∧ (∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) ∧ (∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) ∧ (∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (S.φ a) = a) ∧ (∀ (d : ℕ), Submodule.map (↑S.φ) (G.geSub d) = P.F d) ∧ (∀ (a b : Λ), S.φ a * S.φ b = S.φ (∑ q ∈ Finset.range G.N, ((S.μ q) a) b)) ∧ (∀ (a b : Λ), ((S.μ 0) a) b = a * b) ∧ (∀ (q d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.IsHom (d + e + q) (((S.μ q) a) b)) ∧ ∀ (q : ℕ), 0 < q → LenGrading.IsRel₂ V (S.μ q)

Lemma 6.4 (lem:split-positive-deformation): a positive filtered deformation B of Λ splits: there is a filtered linear isomorphism φ : Λ ≅ B inducing the identification gr B = Λ, restricting on S = Λ₀ to a unital algebra map (the vertex idempotents go to a complete set of orthogonal idempotents) and S-bilinear on both sides; the transported multiplication is μ₀ + Σ_{q>0} μ_q with μ₀ the multiplication of Λ, each μ_q raising the degree by q, S-relative and vanishing when an input belongs to S.