Proposition 5.4 in its general form

mesh-deformations.tex (prop:filtered-normal-form): "Let C = kQ/(r_1, …, r_t) be a finite-dimensional graded algebra over any field, with Q finite and each r_i homogeneous quadratic. For q ≥ 3, let D_{q-1} send a family (f_a)_a, where f_a ∈ C_{q-1} is parallel to the arrow a, to the family whose ith entry is the sum, over the arrow occurrences in r_i, of the terms obtained by replacing that occurrence of a by f_a; these entries lie in C_q. Assume that D_{q-1} is surjective for every q ≥ 3. Let E be a finite filtered algebra, or a finite filtered category with the vertices of Q as objects, with a specified graded identification gr E = C. Then E is isomorphic to C by a map inducing that identification."

Here C is the relation category of the quadratic relations r_i (Rel), E a k-linear category with objects O x (x a vertex), a finite multiplicative filtration F of its Hom spaces and symbols σ_d : F^d → C_d realizing gr E = C (FilteredId). The proof is the source's: lift the arrows (Lifts); the relation errors lie in F³; a degree-q error is D_{q-1} of a family, and subtracting its lifts cancels it, the terms with two corrections having degree 2q - 2 > q (exists_correction); the filtration is finite, so the errors vanish; the resulting functor C → E is bijective on Hom spaces by graded injectivity and surjectivity (normalForm). The case E = ind(mod A), C = k(Γ_A) is IndSkeleton.filteredNormalForm.

Realizing paths

def MultiplicativeBasisDeformations.GeneralNormalForm.pathMap {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x y : V} : Quiver.Path x y → (O x ⟶ O y)

The realization of a path.

@[simp]

theorem MultiplicativeBasisDeformations.GeneralNormalForm.pathMap_nil {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x : V} : pathMap (fun {x y : V} => L) Quiver.Path.nil = CategoryTheory.CategoryStruct.id (O x)

@[simp]

theorem MultiplicativeBasisDeformations.GeneralNormalForm.pathMap_cons {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x y z : V} (p : Quiver.Path x y) (a : y ⟶ z) : pathMap (fun {x y : V} => L) (p.cons a) = CategoryTheory.CategoryStruct.comp (pathMap (fun {x y : V} => L) p) (L a)

theorem MultiplicativeBasisDeformations.GeneralNormalForm.pathMap_comp {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) : pathMap (fun {x y : V} => L) (p.comp q) = CategoryTheory.CategoryStruct.comp (pathMap (fun {x y : V} => L) p) (pathMap (fun {x y : V} => L) q)

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.realize {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) (x y : V) : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] O x ⟶ O y

The realization of a morphism of kQ.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.realize_path {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x y : V} (p : Quiver.Path x y) : (realize (fun {x y : V} => L) x y) (LinearPaths.path p) = pathMap (fun {x y : V} => L) p

theorem MultiplicativeBasisDeformations.GeneralNormalForm.realize_comp {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) {x y z : V} (f : LinearPaths.obj x ⟶ LinearPaths.obj y) (g : LinearPaths.obj y ⟶ LinearPaths.obj z) : (realize (fun {x y : V} => L) x z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((realize (fun {x y : V} => L) x y) f) ((realize (fun {x y : V} => L) y z) g)

theorem MultiplicativeBasisDeformations.GeneralNormalForm.realize_id {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) (x : V) : (realize (fun {x y : V} => L) x x) (CategoryTheory.CategoryStruct.id (LinearPaths.obj x)) = CategoryTheory.CategoryStruct.id (O x)

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.pathFunctor {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} (L : {x y : V} → (x ⟶ y) → (O x ⟶ O y)) : CategoryTheory.Functor (LinearPaths k V) 𝓔

The functor kQ → E sending each arrow to its lift.

Quadratic relations

def MultiplicativeBasisDeformations.GeneralNormalForm.Rel {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (X Y : LinearPaths k V) : Set (X ⟶ Y)

The relations r_i as a family of morphisms of kQ.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.GeneralNormalForm.cl {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) : CategoryTheory.Functor (LinearPaths k V) (RelationCategory k (Rel s t r))

The quotient kQ → C = kQ/(r).

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.Cdeg {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (d : ℕ) (x y : V) : Submodule k ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))

The image in C of the degree-d part.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.cl_mem_Cdeg {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) {d : ℕ} {x y : V} {P : LinearPaths.obj x ⟶ LinearPaths.obj y} (hP : P ∈ LinearPaths.degreePart d x y) : (cl s t r).map P ∈ Cdeg s t r d x y

The filtered category

structure MultiplicativeBasisDeformations.GeneralNormalForm.FilteredId {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] (O : V → 𝓔) {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) : Type (max (max (max u v) w) w')

A finite filtered category E with objects O x and gr E = C: a finite multiplicative filtration F of the Hom spaces and symbols σ_d : F^d → C_d, onto, with kernel F^{d+1}, multiplicative.

• F : ℕ → (x y : V) → Submodule k (O x ⟶ O y)
• F_zero (x y : V) : self.F 0 x y = ⊤
• F_succ_le (d : ℕ) (x y : V) : self.F (d + 1) x y ≤ self.F d x y
• F_comp (d e : ℕ) {x y z : V} {f : O x ⟶ O y} {g : O y ⟶ O z} : f ∈ self.F d x y → g ∈ self.F e y z → CategoryTheory.CategoryStruct.comp f g ∈ self.F (d + e) x z
• N : ℕ
• F_N (x y : V) : self.F self.N x y = ⊥
• σ : ℕ → (x y : V) → (O x ⟶ O y) →ₗ[k] (cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y)
• σ_mem (d : ℕ) (x y : V) (f : O x ⟶ O y) : f ∈ self.F d x y → (self.σ d x y) f ∈ Cdeg s t r d x y
• σ_ker (d : ℕ) (x y : V) (f : O x ⟶ O y) : f ∈ self.F d x y → ((self.σ d x y) f = 0 ↔ f ∈ self.F (d + 1) x y)
• σ_surj (d : ℕ) (x y : V) (c : (cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y)) : c ∈ Cdeg s t r d x y → ∃ f ∈ self.F d x y, (self.σ d x y) f = c
• σ_comp (d e : ℕ) {x y z : V} (f : O x ⟶ O y) (g : O y ⟶ O z) : f ∈ self.F d x y → g ∈ self.F e y z → (self.σ (d + e) x z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.σ d x y) f) ((self.σ e y z) g)
• σ_id (x : V) : (self.σ 0 x x) (CategoryTheory.CategoryStruct.id (O x)) = CategoryTheory.CategoryStruct.id ((cl s t r).obj (LinearPaths.obj x))

theorem MultiplicativeBasisDeformations.GeneralNormalForm.FilteredId.F_anti {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (E : FilteredId O s t r) {d d' : ℕ} (h : d ≤ d') (x y : V) : E.F d' x y ≤ E.F d x y

theorem MultiplicativeBasisDeformations.GeneralNormalForm.FilteredId.σ_eq_zero {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (E : FilteredId O s t r) {d : ℕ} {x y : V} {f : O x ⟶ O y} (hf : f ∈ E.F (d + 1) x y) : (E.σ d x y) f = 0

structure MultiplicativeBasisDeformations.GeneralNormalForm.Lifts {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (E : FilteredId O s t r) : Type (max (max v w) w')

Lifts of the arrows: in F¹ with symbol the arrow.

• L {x y : V} : (x ⟶ y) → (O x ⟶ O y)
• mem {x y : V} (a : x ⟶ y) : self.L a ∈ E.F 1 x y
• sym {x y : V} (a : x ⟶ y) : (E.σ 1 x y) (self.L a) = (cl s t r).map (LinearPaths.arrow a)

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.exists_lifts {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} : Nonempty (Lifts E)

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.pathMap_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) {x y : V} (p : Quiver.Path x y) : pathMap (fun {x y : V} => L.L) p ∈ E.F p.length x y ∧ (E.σ p.length x y) (pathMap (fun {x y : V} => L.L) p) = (cl s t r).map (LinearPaths.path p)

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.realize_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) {d : ℕ} {x y : V} {P : LinearPaths.obj x ⟶ LinearPaths.obj y} (hP : P ∈ LinearPaths.degreePart d x y) : (realize (fun {x y : V} => L.L) x y) P ∈ E.F d x y ∧ (E.σ d x y) ((realize (fun {x y : V} => L.L) x y) P) = (cl s t r).map P

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.error {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) (i : ι) : O (s i) ⟶ O (t i)

The relation error of the lifts.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.r_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (i : ι) : r i ∈ (CategoricalIdeal.HomIdeal.linearSpan k (Rel s t r)).hom (LinearPaths.obj (s i)) (LinearPaths.obj (t i))

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.cl_r {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (i : ι) : (cl s t r).map (r i) = 0

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.error_mem_three {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) (hr : ∀ (i : ι), r i ∈ LinearPaths.degreePart 2 (s i) (t i)) (i : ι) : L.error i ∈ E.F 3 (s i) (t i)

The relation errors lie in F³.

The derivative D_{q-1}

def MultiplicativeBasisDeformations.GeneralNormalForm.pathDer {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))) {x y : V} : Quiver.Path x y → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))

Replacing one arrow occurrence of a path by f_a, summed over the occurrences.

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.derL {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))) (x y : V) : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] (cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y)

Its linear extension to kQ.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.derL_path {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))) {x y : V} (p : Quiver.Path x y) : (derL (fun {x y : V} => f) x y) (LinearPaths.path p) = pathDer (fun {x y : V} => f) p

noncomputable def MultiplicativeBasisDeformations.GeneralNormalForm.Dmap {k : Type u} [Field k] {V : Type v} [Quiver V] {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))) (i : ι) : (cl s t r).obj (LinearPaths.obj (s i)) ⟶ (cl s t r).obj (LinearPaths.obj (t i))

The derivative D_{q-1}(f)_i.

The correction step

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.exists_correction {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) {q' : ℕ} (hq : 2 ≤ q') (hL : ∀ (i : ι), L.error i ∈ E.F (q' + 1) (s i) (t i)) (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))) (hf : ∀ {x y : V} (a : x ⟶ y), f a ∈ Cdeg s t r q' x y) (hD : ∀ (i : ι), Dmap (fun {x y : V} => f) i = (E.σ (q' + 1) (s i) (t i)) (L.error i)) (hr : ∀ (i : ι), r i ∈ LinearPaths.degreePart 2 (s i) (t i)) : ∃ (L' : Lifts E), ∀ (i : ι), L'.error i ∈ E.F (q' + 2) (s i) (t i)

Cancelling the degree-q errors (q = q' + 1 ≥ 3): if the errors lie in F^q and D_{q-1}(f) = σ_q(errors), subtracting lifts of f from the arrows pushes the errors into F^{q+1}; a term with two corrections has degree 2q - 2 > q.

The isomorphism

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.realize_eq_zero_of_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) (hL : ∀ (i : ι), L.error i = 0) {x y : V} {G : LinearPaths.obj x ⟶ LinearPaths.obj y} (hG : G ∈ (CategoricalIdeal.HomIdeal.linearSpan k (Rel s t r)).hom (LinearPaths.obj x) (LinearPaths.obj y)) : (realize (fun {x y : V} => L.L) x y) G = 0

Lifts satisfying the relations kill the relation ideal.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.mem_of_realize_eq_zero {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) (hL : ∀ (i : ι), L.error i = 0) {x y : V} {G : LinearPaths.obj x ⟶ LinearPaths.obj y} (hG : (realize (fun {x y : V} => L.L) x y) G = 0) : G ∈ (CategoricalIdeal.HomIdeal.linearSpan k (Rel s t r)).hom (LinearPaths.obj x) (LinearPaths.obj y)

Faithfulness: a morphism of kQ realized to zero lies in the relation ideal.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.Lifts.exists_realize_eq {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {E : FilteredId O s t r} (L : Lifts E) {x y : V} (f : O x ⟶ O y) : ∃ (G : LinearPaths.obj x ⟶ LinearPaths.obj y), (realize (fun {x y : V} => L.L) x y) G = f

Fullness: every morphism of E is realized.

theorem MultiplicativeBasisDeformations.GeneralNormalForm.normalForm {k : Type u} [Field k] {V : Type v} [Quiver V] {𝓔 : Type u'} [CategoryTheory.Category.{w', u'} 𝓔] [CategoryTheory.Preadditive 𝓔] [CategoryTheory.Linear k 𝓔] {O : V → 𝓔} {ι : Type} {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (E : FilteredId O s t r) (hr : ∀ (i : ι), r i ∈ LinearPaths.degreePart 2 (s i) (t i)) (hDsurj : ∀ (q' : ℕ), 2 ≤ q' → ∀ (g : (i : ι) → (cl s t r).obj (LinearPaths.obj (s i)) ⟶ (cl s t r).obj (LinearPaths.obj (t i))), (∀ (i : ι), g i ∈ Cdeg s t r (q' + 1) (s i) (t i)) → ∃ (f : {x y : V} → (x ⟶ y) → ((cl s t r).obj (LinearPaths.obj x) ⟶ (cl s t r).obj (LinearPaths.obj y))), (∀ {x y : V} (a : x ⟶ y), f a ∈ Cdeg s t r q' x y) ∧ ∀ (i : ι), Dmap (fun {x y : V} => f) i = g i) : ∃ (L : Lifts E), (∀ (i : ι), L.error i = 0) ∧ ∃ (Φ : CategoryTheory.Functor (RelationCategory k (Rel s t r)) 𝓔), ((cl s t r).comp Φ = pathFunctor fun {x y : V} => L.L) ∧ Φ.Full ∧ Φ.Faithful ∧ ∀ (d : ℕ) {x y : V}, ∀ P ∈ LinearPaths.degreePart d x y, (realize (fun {x y : V} => L.L) x y) P ∈ E.F d x y ∧ (E.σ d x y) ((realize (fun {x y : V} => L.L) x y) P) = (cl s t r).map P

Proposition 5.4 (prop:filtered-normal-form), general form: for quadratic relations r_i with every D_{q-1} (q ≥ 3) surjective, and a finite filtered category E with objects the vertices and gr E = C = kQ/(r), there are lifts of the arrows satisfying the relations, and the induced functor C → E is full and faithful (an isomorphism of categories on the vertices) and induces the given identification gr E = C.