Initial forms identify ray products (Proposition 8.3(2), Theorem 11.8(1))

local-ray-geometry.tex (prop:dimension-induction(2)): "The initial-form bijection of Lemma 3.7 identifies the products in ray A and ray A₀." Theorem 11.8(1) uses the same identification.

For the categorical filtration J of A (posFiltA), Lemma 3.7 (rayDegree_J) gives the initial-form bijection between the rays of a corner and the nonzero pieces A₀(x,y)_d. Here: for nonzero f ∈ A(x,y), g ∈ A(y,z) of degrees d, e, the ray product [f][g] is nonzero (fg ∉ M(f,g)) iff the product of the initial forms σ_d f · σ_e g is nonzero, and then σ_{d+e}(fg) = σ_d f · σ_e g (IndSkeleton.initialForm_products).

One direction holds for every positive filtered deformation whose radical lies in degree one (mul_not_mem_of_σ: M(f,g) ⊆ F^{d+e+1}). For the converse we count: the initial forms of the rays of a presentation of A by the table P of A₀ (rayA_eq_rayA0) give a bijection θ of the rays of P (thetaR) under which every nonzero product of P comes from a nonzero product of A; both tables have the same number of nonzero products, so the two sets of pairs coincide.

theorem MultiplicativeBasisDeformations.PosFiltration.σ_mul3 {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) [IsAlgClosed k] [FiniteDimensional k B] {d : ℕ} (a f c : B) (hf : f ∈ P.F d) : (P.σ d) (a * f * c) = (P.σ 0) a * (P.σ d) f * (P.σ 0) c

theorem MultiplicativeBasisDeformations.PosFiltration.σ_cornerUnit {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (hP : P.RadOne) {x : Fin F.m} {u : B} (hu : F.IsCornerUnit x u) : ∃ (c : k), c ≠ 0 ∧ (P.σ 0) u = c • (P.σ 0) (F.e x)

The initial form of a corner unit is a nonzero multiple of the idempotent.

theorem MultiplicativeBasisDeformations.PosFiltration.insertionSpan_le_F {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (hP : P.RadOne) {x y z : Fin F.m} {f h : B} {d e : ℕ} (hf : f ∈ P.F d) (hh : h ∈ P.F e) : F.insertionSpan x y z f h ≤ P.F (d + e + 1)

M(f, h) ⊆ F^{d+e+1}.

theorem MultiplicativeBasisDeformations.PosFiltration.mul_not_mem_of_σ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (hP : P.RadOne) {x y z : Fin F.m} {f h : B} {d e : ℕ} (hf : f ∈ P.F d) (hh : h ∈ P.F e) (hσ : (P.σ d) f * (P.σ e) h ≠ 0) : f * h ∉ F.insertionSpan x y z f h ∧ f * h ∈ P.F (d + e) ∧ f * h ∉ P.F (d + e + 1) ∧ (P.σ (d + e)) (f * h) = (P.σ d) f * (P.σ e) h

If the initial forms multiply to a nonzero element, the ray product is nonzero with that initial form.

theorem MultiplicativeBasisDeformations.PosFiltration.σ_of_mem_ray {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (hP : P.RadOne) {x y : Fin F.m} {f f' : B} (hfc : f ∈ F.corner x y) (hf' : f' ∈ F.ray x y f) {d : ℕ} (hf : f ∈ P.F d) : f' ∈ P.F d ∧ ∃ (c : k), c ≠ 0 ∧ (P.σ d) f' = c • (P.σ d) f

Elements of a ray have proportional initial forms.

The initial forms of the idempotents of A are vertex idempotents of A₀

theorem MultiplicativeBasisDeformations.MeshWalk.isHom_of_isDiag {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {z : (CatAlg.Alg D.F0)ᵐᵒᵖ} {t : D.PV → k} (hz : IsDiag D z t) : (lenA0 D hfin).IsHom 0 z

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_one {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : IsDiag D 1 fun (x : D.PV) => 1

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_eP {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (p : D.PV) : IsDiag D (eP D p) (Pi.single p 1)

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {z w : (CatAlg.Alg D.F0)ᵐᵒᵖ} {t s : D.PV → k} (hz : IsDiag D z t) (hw : IsDiag D w s) : IsDiag D (z + w) (t + s)

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {ι : Type u_1} (S : Finset ι) {z : ι → (CatAlg.Alg D.F0)ᵐᵒᵖ} {t : ι → D.PV → k} (hz : ∀ (i : ι), IsDiag D (z i) (t i)) : IsDiag D (∑ i ∈ S, z i) (∑ i ∈ S, t i)

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_coeff {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {z : (CatAlg.Alg D.F0)ᵐᵒᵖ} {t s : D.PV → k} (hz : IsDiag D z t) (hs : IsDiag D z s) : t = s

theorem MultiplicativeBasisDeformations.MeshWalk.eq_of_isDiag {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {z w : (CatAlg.Alg D.F0)ᵐᵒᵖ} {t : D.PV → k} (hz : IsDiag D z t) (hw : IsDiag D w t) : z = w

theorem MultiplicativeBasisDeformations.MeshWalk.σ_zero_one {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) : (P.σ 0) 1 = 1

theorem MultiplicativeBasisDeformations.MeshWalk.σ_e_ne_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (x : Fin F.m) : (P.σ 0) (F.e x) ≠ 0

theorem MultiplicativeBasisDeformations.MeshWalk.isDiag_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] : IsDiag D 0 0

theorem MultiplicativeBasisDeformations.MeshWalk.exists_vertexMatch {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) (hcard : Fintype.card D.PV = F.m) : ∃ (π : Fin F.m ≃ D.PV), ∀ (x : Fin F.m), (P.σ 0) (F.e x) = eP D (π x)

Vertex matching: the initial forms of the idempotents e_x are the vertex idempotents of A₀, for a bijection of the vertices.

Homogeneous elements of a corner of A₀

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.dA {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (r : RayA0 D v₀) : ℕ

The length degree of a ray of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_isHom' {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (r : RayA0 D v₀) : (lenA0 D ⋯).IsHom (dA D v₀ r) ((basisR D v₀ hF) r)

theorem MultiplicativeBasisDeformations.MeshWalk.eq_smul_basisR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {a b : Fin (FpA0 D v₀ hF).m} {d : ℕ} {z : (CatAlg.Alg D.F0)ᵐᵒᵖ} (hz : z ∈ (FpA0 D v₀ hF).corner a b) (hd : (lenA0 D ⋯).IsHom d z) (hz0 : z ≠ 0) : ∃ (r : RayA0 D v₀), (idxA0 D v₀ hF) (srcR D v₀ r) = a ∧ (idxA0 D v₀ hF) (tgtR D v₀ r) = b ∧ dA D v₀ r = d ∧ ∃ (t : k), t ≠ 0 ∧ z = t • (basisR D v₀ hF) r

A nonzero homogeneous element of a corner of A₀ is a multiple of one ray vector.

Counting nonzero products

theorem MultiplicativeBasisDeformations.MeshWalk.eP_eq_unitM {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : eP D p = MulOpposite.op (CatAlg.unitM p p (CategoryTheory.CategoryStruct.id (D.F0 p)))

noncomputable def MultiplicativeBasisDeformations.MeshWalk.degβ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : ℕ

The degree of a ray vector of the presentation.

theorem MultiplicativeBasisDeformations.MeshWalk.degβ_spec {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : β r ∈ Pf.F (degβ D F v₀ hF Pf hβ r) ∧ β r ∉ Pf.F (degβ D F v₀ hF Pf hβ r + 1)

theorem MultiplicativeBasisDeformations.MeshWalk.card_PV {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) : Fintype.card D.PV = F.m

noncomputable def MultiplicativeBasisDeformations.MeshWalk.πV {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) : Fin F.m ≃ D.PV

The vertex matching of the initial forms.

theorem MultiplicativeBasisDeformations.MeshWalk.σ_e_eq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (x : Fin F.m) : (Pf.σ 0) (F.e x) = (FpA0 D v₀ hF).e ((idxA0 D v₀ hF) ((πV D F v₀ hF Pf hβ) x))

theorem MultiplicativeBasisDeformations.MeshWalk.exists_thetaR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : ∃ (r' : RayA0 D v₀), (idxA0 D v₀ hF) (srcR D v₀ r') = (idxA0 D v₀ hF) ((πV D F v₀ hF Pf hβ) (ι (srcR D v₀ r))) ∧ (idxA0 D v₀ hF) (tgtR D v₀ r') = (idxA0 D v₀ hF) ((πV D F v₀ hF Pf hβ) (ι (tgtR D v₀ r))) ∧ dA D v₀ r' = degβ D F v₀ hF Pf hβ r ∧ ∃ (t : k), t ≠ 0 ∧ (Pf.σ (degβ D F v₀ hF Pf hβ r)) (β r) = t • (basisR D v₀ hF) r'

noncomputable def MultiplicativeBasisDeformations.MeshWalk.thetaR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : RayA0 D v₀

The initial-form map on the rays of P.

theorem MultiplicativeBasisDeformations.MeshWalk.thetaR_spec {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : srcR D v₀ (thetaR D F v₀ hF Pf hβ r) = (πV D F v₀ hF Pf hβ) (ι (srcR D v₀ r)) ∧ tgtR D v₀ (thetaR D F v₀ hF Pf hβ r) = (πV D F v₀ hF Pf hβ) (ι (tgtR D v₀ r)) ∧ ∃ (t : k), t ≠ 0 ∧ (Pf.σ (degβ D F v₀ hF Pf hβ r)) (β r) = t • (basisR D v₀ hF) (thetaR D F v₀ hF Pf hβ r)

theorem MultiplicativeBasisDeformations.MeshWalk.thetaR_dA {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) (r : RayA0 D v₀) : dA D v₀ (thetaR D F v₀ hF Pf hβ r) = degβ D F v₀ hF Pf hβ r

theorem MultiplicativeBasisDeformations.MeshWalk.thetaR_injective {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) (hP : Pf.RadOne) (hA : IsRepresentationFinite k B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) : Function.Injective (thetaR D F v₀ hF Pf hβ)

theorem MultiplicativeBasisDeformations.MeshWalk.mul_some_of_thetaR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) (hP : Pf.RadOne) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) {r s t : RayA0 D v₀} (h : (A0Mult D v₀ hF).mul (thetaR D F v₀ hF Pf hβ r) (thetaR D F v₀ hF Pf hβ s) = some t) : ((A0Mult D v₀ hF).mul r s).isSome = true

A nonzero product of P at the initial forms is a nonzero product of the presentation.

theorem MultiplicativeBasisDeformations.MeshWalk.σ_mul_ne_zero_of_mul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) (hP : Pf.RadOne) (hA : IsRepresentationFinite k B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) {r s : RayA0 D v₀} (h : ((A0Mult D v₀ hF).mul r s).isSome = true) : (Pf.σ (degβ D F v₀ hF Pf hβ r)) (β r) * (Pf.σ (degβ D F v₀ hF Pf hβ s)) (β s) ≠ 0

Every nonzero product of the presentation has nonzero initial forms (counting).

theorem MultiplicativeBasisDeformations.MeshWalk.initialForm_products {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (Pf : PosFiltration (lenA0 D ⋯) B) (hP : Pf.RadOne) (hA : IsRepresentationFinite k B) {ι : D.PV ≃ Fin F.m} {β : RayA0 D v₀ → B} (hβ : F.IsRayPres (A0Mult D v₀ hF) ι β) {x y z : Fin F.m} {f g : B} {d e : ℕ} (hf : f ∈ F.corner x y) (hg : g ∈ F.corner y z) : f ∈ Pf.F d → ∀ (hfd' : f ∉ Pf.F (d + 1)) (hge : g ∈ Pf.F e) (hge' : g ∉ Pf.F (e + 1)), (f * g ∉ F.insertionSpan x y z f g ↔ (Pf.σ d) f * (Pf.σ e) g ≠ 0) ∧ ((Pf.σ d) f * (Pf.σ e) g ≠ 0 → f * g ∈ Pf.F (d + e) ∧ f * g ∉ Pf.F (d + e + 1) ∧ (Pf.σ (d + e)) (f * g) = (Pf.σ d) f * (Pf.σ e) g)

Initial forms identify ray products (Proposition 8.3(2)): for nonzero f ∈ A(x,y), g ∈ A(y,z) of degrees d, e, the ray product [f][g] is nonzero iff σ_d f · σ_e g ≠ 0, and then fg has degree d + e with initial form σ_d f · σ_e g.

Theorem 11.8(1): initial forms identify ray A with ray A₀

theorem MultiplicativeBasisDeformations.rayA_initialForms (k : Type u) [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (hn : Nontrivial A) (S : IndSkeleton k A) : ∃ (b : S.ArrowBases) (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (F : PrimitiveIdempotents A) (ι : (S.arMeshData b).PV ≃ Fin F.m) (β : S.rayA0AR b v₀ → A), F.IsRayPres (S.A0MultAR b v₀ hF) ι β ∧ ∀ {n : ℕ} {e : Fin n → A} (he : CompleteOrthogonalIdempotents e) (hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i)) (hbas : ∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j) {x y z : Fin F.m} {f g : A} {d d' : ℕ}, f ∈ F.corner x y → g ∈ F.corner y z → f ∈ (S.posFiltA b he hprim hbas).F d → f ∉ (S.posFiltA b he hprim hbas).F (d + 1) → g ∈ (S.posFiltA b he hprim hbas).F d' → g ∉ (S.posFiltA b he hprim hbas).F (d' + 1) → (f * g ∉ F.insertionSpan x y z f g ↔ ((S.posFiltA b he hprim hbas).σ d) f * ((S.posFiltA b he hprim hbas).σ d') g ≠ 0) ∧ (((S.posFiltA b he hprim hbas).σ d) f * ((S.posFiltA b he hprim hbas).σ d') g ≠ 0 → f * g ∈ (S.posFiltA b he hprim hbas).F (d + d') ∧ f * g ∉ (S.posFiltA b he hprim hbas).F (d + d' + 1) ∧ ((S.posFiltA b he hprim hbas).σ (d + d')) (f * g) = ((S.posFiltA b he hprim hbas).σ d) f * ((S.posFiltA b he hprim hbas).σ d') g)

Initial forms identify ray A with ray A₀ (Proposition 8.3(2), Theorem 11.8(1)): the rays of A are presented by the ray table of A₀ (rayA_eq_rayA0), and for the categorical filtration J (posFiltA, for any complete set e of primitive idempotents) a ray product [f][g] is nonzero iff the product of the initial forms is nonzero, in which case fg has the sum of the degrees and initial form σ_d f · σ_e g. With Lemma 3.7 (rayDegree_J: the initial-form bijection), this is the identification of the products.