Proposition 5.4 for a filtered algebra #
prop:filtered-normal-form: "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."
The category case is GeneralNormalForm.normalForm. For an algebra E with a finite
multiplicative filtration and symbols σ_d : F^d → C_d into the algebra C = ⊕_{x,y} C(x, y)
(CatAlg.Alg of the relation category; FilteredAlg), the vertex idempotents of C lift to
orthogonal idempotents f_x of E through the nilpotent ideal F¹; the corners f_x E f_y
form a k-linear category (CornerCat) with the induced filtration and symbols
(FilteredAlg.toFilteredId); the category case gives a full and faithful functor from C, and
summing over the corners gives an algebra isomorphism C ≅ E inducing the identification
(normalForm_algebra). The same assembly applied to normalFormRetained gives Proposition 12.2
for an algebra: E ≅ kQ/(𝔪^{N+1}, r_v − Σ_j λ_j (p_j)_v) inducing the identification
(normalFormRetained_algebra).
The category of corners of an algebra #
def
MultiplicativeBasisDeformations.GeneralNormalForm.corner
(k : Type u)
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
(f : V → E)
(x y : V)
:
Submodule k E
The corner f_x E f_y.
Instances For
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.mul_mem_corner
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
{x y z : V}
{a b : E}
(ha : a ∈ corner k f x y)
(hb : b ∈ corner k f y z)
:
a * b ∈ corner k f x z
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.corner_mul_corner_ne
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
{x y y' z : V}
(h : y ≠ y')
{a b : E}
(ha : a ∈ corner k f x y)
(hb : b ∈ corner k f y' z)
:
a * b = 0
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.eq_sum_corner
{E : Type u}
[Ring E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
(a : E)
:
a = ∑ x : V, ∑ y : V, f x * a * f y
@[instance_reducible]
instance
MultiplicativeBasisDeformations.GeneralNormalForm.instCategoryCornerCat
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
:
CategoryTheory.Category.{u, 0} (CornerCat k hf)
@[simp]
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.cc_comp_val
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
{x y z : CornerCat k hf}
(a : x ⟶ y)
(b : y ⟶ z)
:
↑(CategoryTheory.CategoryStruct.comp a b) = ↑a * ↑b
@[instance_reducible]
instance
MultiplicativeBasisDeformations.GeneralNormalForm.instPreadditiveCornerCat
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
:
CategoryTheory.Preadditive (CornerCat k hf)
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.idem_mul_corner_mul_idem
{k : Type u}
[Field k]
{E : Type u}
[Ring E]
[Algebra k E]
{V : Type}
[Fintype V]
[DecidableEq V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
(x y : V)
{x' y' : V}
{a : E}
(ha : a ∈ corner k f x' y')
:
f x * a * f y = if x = x' then if y = y' then a else 0 else 0
def
MultiplicativeBasisDeformations.GeneralNormalForm.cobj
{k E : Type u}
[Ring E]
{V : Type}
[Fintype V]
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
(x : V)
:
CornerCat k hf
The objects of the category of corners.
Instances For
Matrix units of a category algebra #
def
MultiplicativeBasisDeformations.GeneralNormalForm.sgl
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[DecidableEq ι]
{G : ι → 𝒞}
(x y : ι)
(c : G x ⟶ G y)
:
The matrix unit with entry c at (x, y).
Instances For
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.sgl_self
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(x y : ι)
(c : G x ⟶ G y)
:
sgl x y c x y = c
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.sgl_zero
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(x y : ι)
:
sgl x y 0 = 0
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.sum_sgl
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(m : CatAlg.Alg G)
:
∑ x : ι, ∑ y : ι, sgl x y (m x y) = m
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.sgl_mem
{k : Type u}
[Field k]
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
{S : (x y : ι) → Submodule k (G x ⟶ G y)}
{x y : ι}
{c : G x ⟶ G y}
(hc : c ∈ S x y)
(a b : ι)
:
sgl x y c a b ∈ S a b
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.idem_mul_apply
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(x : ι)
(m : CatAlg.Alg G)
(a c : ι)
:
(CatAlg.idem x * m) a c = CategoryTheory.CategoryStruct.comp (CatAlg.idTo a x) (m x c)
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.mul_idem_apply
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(y : ι)
(m : CatAlg.Alg G)
(a b : ι)
:
(m * CatAlg.idem y) a b = CategoryTheory.CategoryStruct.comp (m a y) (CatAlg.idTo y b)
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.idem_mul_mul_idem
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(x y : ι)
(m : CatAlg.Alg G)
:
CatAlg.idem x * m * CatAlg.idem y = sgl x y (m x y)
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.idem_eq_sgl
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{G : ι → 𝒞}
(x : ι)
:
CatAlg.idem x = sgl x x (CategoryTheory.CategoryStruct.id (G x))
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.idem_complete
{𝒞 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(G : ι → 𝒞)
:
CompleteOrthogonalIdempotents fun (x : ι) => CatAlg.idem x
Filtered algebras #
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.GeneralNormalForm.clObj
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{ι : Type}
(s t : ι → V)
(r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i))
(x : V)
:
RelationCategory k (Rel s t r)
The objects of C.
Instances For
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.id_mem_Cdeg
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
(s t : ι → V)
(r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i))
(x : V)
:
structure
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
(s t : ι → V)
(r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i))
(E : Type u)
[Ring E]
[Algebra k E]
:
Type u
A finite filtered algebra E with gr E = C: a finite multiplicative filtration F of
E and symbols σ_d : F^d → C_d into the category algebra of C, onto, with kernel F^{d+1},
multiplicative and unital.
- F : ℕ → Submodule k E
- F_zero : self.F 0 = ⊤
- N : ℕ
- σ : ℕ → E →ₗ[k] CatAlg.Alg (clObj s t r)
- σ_surj (d : ℕ) (c : CatAlg.Alg (clObj s t r)) : (∀ (x y : V), c x y ∈ Cdeg s t r d x y) → ∃ a ∈ self.F d, (self.σ d) a = c
- σ_one : (self.σ 0) 1 = 1
Instances For
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.mem_F_zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
(a : E)
:
a ∈ A.F 0
noncomputable def
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.σ₀
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
:
E →+* CatAlg.Alg (clObj s t r)
The degree-zero symbol, a ring map with nilpotent kernel F¹.
Instances For
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.pow_mem
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{a : E}
(ha : a ∈ A.F 1)
(n : ℕ)
:
a ^ n ∈ A.F n
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.isNilpotent_of_ker
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{a : E}
(ha : a ∈ RingHom.ker A.σ₀)
:
IsNilpotent a
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.exists_idem
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
:
∃ (f : V → E), CompleteOrthogonalIdempotents f ∧ ∀ (x : V), (A.σ 0) (f x) = CatAlg.idem x
The vertex idempotents lift through the nilpotent ideal F¹.
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.σ_corner
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{f : V → E}
(hσf : ∀ (x : V), (A.σ 0) (f x) = CatAlg.idem x)
{d : ℕ}
{g : E}
(hg : g ∈ A.F d)
(x y : V)
:
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.corner_mem_F
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{f : V → E}
{d : ℕ}
{g : E}
(hg : g ∈ A.F d)
(x y : V)
:
f x * g * f y ∈ A.F d
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.σ_conc
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{f : V → E}
(hσf : ∀ (x : V), (A.σ 0) (f x) = CatAlg.idem x)
{d : ℕ}
{x y : V}
{a : E}
(ha : a ∈ corner k f x y)
(had : a ∈ A.F d)
:
noncomputable def
MultiplicativeBasisDeformations.GeneralNormalForm.FilteredAlg.toFilteredId
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{f : V → E}
(hf : CompleteOrthogonalIdempotents f)
(hσf : ∀ (x : V), (A.σ 0) (f x) = CatAlg.idem x)
:
FilteredId (cobj hf) s t r
The filtered category of corners f_x E f_y, with the induced filtration and symbols.
Instances For
From corner maps to an algebra isomorphism #
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.exists_algEquiv
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{E' : Type u}
[Ring E']
[Algebra k E']
{f : V → E'}
(hf : CompleteOrthogonalIdempotents f)
{𝒟 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒟]
[CategoryTheory.Preadditive 𝒟]
[CategoryTheory.Linear k 𝒟]
{G : V → 𝒟}
(φ : (x y : V) → (G x ⟶ G y) →ₗ[k] E')
(hmem : ∀ (x y : V) (c : G x ⟶ G y), (φ x y) c ∈ corner k f x y)
(hcomp :
∀ (x y z : V) (c : G x ⟶ G y) (c' : G y ⟶ G z),
(φ x z) (CategoryTheory.CategoryStruct.comp c c') = (φ x y) c * (φ y z) c')
(hid : ∀ (x : V), (φ x x) (CategoryTheory.CategoryStruct.id (G x)) = f x)
(hinj : ∀ (x y : V) (c : G x ⟶ G y), (φ x y) c = 0 → c = 0)
(hsurj : ∀ (x y : V), ∀ a ∈ corner k f x y, ∃ (c : G x ⟶ G y), (φ x y) c = a)
:
∃ (Ψ : CatAlg.Alg G ≃ₐ[k] E'), ∀ (m : CatAlg.Alg G), Ψ m = ∑ x : V, ∑ y : V, (φ x y) (m x y)
Assembly: maps φ_{xy} : 𝒟(G x, G y) → f_x E f_y, bijective onto the corners and
compatible with composition and identities, sum to an algebra isomorphism Alg G ≅ E.
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.exists_cornerMaps
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{E' : Type u}
[Ring E']
[Algebra k E']
{f : V → E'}
(hf : CompleteOrthogonalIdempotents f)
{R : (X Y : LinearPaths k V) → Set (X ⟶ Y)}
(L : {x y : V} → (x ⟶ y) → (cobj hf x ⟶ cobj hf y))
(Φ : CategoryTheory.Functor (RelationCategory k R) (CornerCat k hf))
(hΦ : (RelationCategory.functor k R).comp Φ = pathFunctor fun {x y : V} => L)
(hfull : Φ.Full)
(hfaith : Φ.Faithful)
:
∃ (φ :
(x y : V) →
((RelationCategory.functor k R).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj y)) →ₗ[k] E'),
(∀ (x y : V) (P : LinearPaths.obj x ⟶ LinearPaths.obj y),
(φ x y) ((RelationCategory.functor k R).map P) = ↑((realize (fun {x y : V} => L) x y) P)) ∧ (∀ (x y : V)
(c :
(RelationCategory.functor k R).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj y)),
(φ x y) c ∈ corner k f x y) ∧ (∀ (x y z : V)
(c :
(RelationCategory.functor k R).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj y))
(c' :
(RelationCategory.functor k R).obj (LinearPaths.obj y) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj z)),
(φ x z) (CategoryTheory.CategoryStruct.comp c c') = (φ x y) c * (φ y z) c') ∧ (∀ (x : V),
(φ x x) (CategoryTheory.CategoryStruct.id ((RelationCategory.functor k R).obj (LinearPaths.obj x))) = f x) ∧ (∀ (x y : V)
(c :
(RelationCategory.functor k R).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj y)),
(φ x y) c = 0 → c = 0) ∧ ∀ (x y : V),
∀ a ∈ corner k f x y,
∃ (c :
(RelationCategory.functor k R).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k R).obj (LinearPaths.obj y)),
(φ x y) c = a
Corner maps from a full and faithful functor kQ/R → (corners of E) lifting the
realization of paths.
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.normalForm_algebra
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
(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)
:
∃ (Ψ : CatAlg.Alg (clObj s t r) ≃ₐ[k] E),
∀ (d : ℕ) (c : CatAlg.Alg (clObj s t r)), (∀ (x y : V), c x y ∈ Cdeg s t r d x y) → Ψ c ∈ A.F d ∧ (A.σ d) (Ψ c) = c
Proposition 5.4 (prop:filtered-normal-form) for a filtered algebra: under the
hypotheses of the general form (quadratic relations, surjective D_{q-1} for q ≥ 3), a finite
filtered algebra E with a graded identification gr E = C is isomorphic to the category
algebra of C by a map inducing that identification: it sends C_d into F^d E with symbol
the identity.
theorem
MultiplicativeBasisDeformations.GeneralNormalForm.normalFormRetained_algebra
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{ι : Type}
{s t : ι → V}
{r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
{E : Type u}
[Ring E]
[Algebra k E]
(A : FilteredAlg s t r E)
{J : Type}
[Fintype J]
{deg : J → ℕ}
{p : J → (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)}
(hdeg : ∀ (j : J), 3 ≤ deg j)
(hp : ∀ (j : J) (i : ι), p j i ∈ LinearPaths.degreePart (deg j) (s i) (t i))
(hr : ∀ (i : ι), r i ∈ LinearPaths.degreePart 2 (s i) (t i))
(hspan :
∀ (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))) (c :
J → k),
(∀ {x y : V} (a : x ⟶ y), f a ∈ Cdeg s t r q' x y) ∧ (∀ (j : J), deg j ≠ q' + 1 → c j = 0) ∧ ∀ (i : ι), g i = Dmap (fun {x y : V} => f) i + ∑ j : J, c j • (cl s t r).map (p j i))
:
∃ (lam : J → k) (Ψ :
(CatAlg.Alg fun (x : V) => (RelationCategory.functor k (RelRet r p lam A.N)).obj (LinearPaths.obj x)) ≃ₐ[k] E),
∀ (d : ℕ) (P : (x y : V) → LinearPaths.obj x ⟶ LinearPaths.obj y),
(∀ (x y : V), P x y ∈ LinearPaths.degreePart d x y) →
(Ψ fun (x y : V) => (RelationCategory.functor k (RelRet r p lam A.N)).map (P x y)) ∈ A.F d ∧ (A.σ d) (Ψ fun (x y : V) => (RelationCategory.functor k (RelRet r p lam A.N)).map (P x y)) = fun (x y : V) =>
(cl s t r).map (P x y)
Proposition 12.2 (prop:characteristic-two-normal-form) for a filtered algebra:
under the hypotheses of normalFormRetained (quadratic relations, retained tuples p_j of degrees
≥ 3 whose classes together with im D_{q-1} span), every finite filtered algebra E with a
graded identification gr E = C has a presentation E ≅ kQ/(𝔪^{N+1}, r_v − Σ_j λ_j (p_j)_v)
(the category algebra of the relation category RelRet r p λ N, with F^N E = 0) for some
scalars λ, and the isomorphism induces the identification: it sends the class of a family of
degree-d path combinations into F^d E, with symbol its class in C.