The projective corner of the lifted modules is B (toward Corollary 12.1)

deformation-refinements.tex: "At projective labels choose the regular B-projectives." The vertex idempotents e_p of A₀ give vertices of the length grading (vxIdem), and a splitting of B respecting them (Lemma 6.4). The lift M_p^B at a projective label is the regular module φ(e_p) B (Proposition 6.5(3)), by uniqueness of lifts; the corner algebra of the lifted modules at the projective labels is therefore B (cornerEquiv).

The vertex idempotents of A₀

theorem MultiplicativeBasisDeformations.MeshWalk.idem_apply' {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) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x y z : D.PV) : CatAlg.idem x y z = CategoryTheory.CategoryStruct.comp (CatAlg.idTo y x) (CatAlg.idTo x z)

theorem MultiplicativeBasisDeformations.MeshWalk.idem_mul_idem_ne {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) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {p q : D.PV} (h : p ≠ q) : CatAlg.idem p * CatAlg.idem q = 0

theorem MultiplicativeBasisDeformations.MeshWalk.sum_idem' {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) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : ∑ x : D.PV, CatAlg.idem x = 1

theorem MultiplicativeBasisDeformations.MeshWalk.idem_mem {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) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p y z : D.PV) : CatAlg.idem p y z ∈ ScalarMeshCategory.degreePart c 0 ↑y ↑z

noncomputable def MultiplicativeBasisDeformations.MeshWalk.vxIdem {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : (lenA0 D hfin).Vertices

The vertex idempotents of A₀ as vertices of its length grading.

theorem MultiplicativeBasisDeformations.MeshWalk.vxIdem_e {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : (vxIdem D hfin).e ((Fintype.equivFin D.PV) p) = MulOpposite.op (CatAlg.idem p)

The lifts at projective labels are regular

theorem MultiplicativeBasisDeformations.MeshWalk.idem_isHom0 {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : (lenA0 D hfin).IsHom 0 (MulOpposite.op (CatAlg.idem p))

theorem MultiplicativeBasisDeformations.MeshWalk.idem_idem {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : IsIdempotentElem (MulOpposite.op (CatAlg.idem p))

theorem MultiplicativeBasisDeformations.MeshWalk.colAlg_mul_idem {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : CatAlg.colAlg p m * CatAlg.idem p = CatAlg.colAlg p m

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ψR {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : CatAlg.Rep D.F0 (meshFam Q c ↑p) →ₗ[k] ↥(GExt.RI k (MulOpposite.op (CatAlg.idem p)))

The cyclic projective ψ : M_p → e_p A₀, m ↦ (m, as a column).

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_apply {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : ↑((ψR p) m) = MulOpposite.op (CatAlg.colAlg p m)

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_act {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ↑((ψR p) (MulOpposite.unop a • m)) = ↑((ψR p) m) * a

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : Function.Injective ⇑(ψR p)

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_surjective {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) : Function.Surjective ⇑(ψR p)

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (p : D.PV) (q : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (hm : (gmodEv D hfin ↑p).gr.IsHom q m) : (GExt.rightIdeal ⋯ ⋯ ⋯).gr.IsHom (q + 0) ((ψR p) m)

theorem MultiplicativeBasisDeformations.MeshWalk.hleft_p {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (p : D.PV) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : S.φ (MulOpposite.op (CatAlg.idem p) * a) = S.φ (MulOpposite.op (CatAlg.idem p)) * S.φ a

noncomputable def MultiplicativeBasisDeformations.MeshWalk.regT {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (p : D.PV) : P.FLift ⋯ (gmodEv D hfin ↑p)

The regular lift transported to M_p.

theorem MultiplicativeBasisDeformations.MeshWalk.ψR_regT {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (x : B) : S.φ ↑((ψR p) (((regT S hleft p).act m) x)) = S.φ ↑((ψR p) m) * x

theorem MultiplicativeBasisDeformations.MeshWalk.exists_regIso {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p : D.PV) : ∃ (Φ : CatAlg.Rep D.F0 (meshFam Q c ↑p) ≃ₗ[k] CatAlg.Rep D.F0 (meshFam Q c ↑p)), ∀ (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (x : B), Φ (((Ls.L ↑p).act m) x) = ((regT S hleft p).act (Φ m)) x

noncomputable def MultiplicativeBasisDeformations.MeshWalk.θ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p : D.PV) : CatAlg.Rep D.F0 (meshFam Q c ↑p) →ₗ[k] B

M_p^B ≅ φ(e_p)B: the embedding θ_p : M_p^B → B.

theorem MultiplicativeBasisDeformations.MeshWalk.θ_act {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (x : B) : (θ Ls S hleft Vx p) (((Ls.L ↑p).act m) x) = (θ Ls S hleft Vx p) m * x

theorem MultiplicativeBasisDeformations.MeshWalk.θ_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p : D.PV) : Function.Injective ⇑(θ Ls S hleft Vx p)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.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} {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} (S : P.Split) (p : D.PV) : B

The lifted vertex idempotent E_p = φ(e_p).

theorem MultiplicativeBasisDeformations.MeshWalk.mem_range_θ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p : D.PV) (b : B) : b ∈ (θ Ls S hleft Vx p).range ↔ Ep S p * b = b

The corner algebra

theorem MultiplicativeBasisDeformations.MeshWalk.Ep_mul_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (p q : D.PV) : Ep S p * Ep S q = if p = q then Ep S p else 0

theorem MultiplicativeBasisDeformations.MeshWalk.sum_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) : ∑ p : D.PV, Ep S p = 1

theorem MultiplicativeBasisDeformations.MeshWalk.Ep_idem {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (p : D.PV) : Ep S p * Ep S p = Ep S p

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ξ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b : B) (p q : D.PV) : CatAlg.Rep D.F0 (meshFam Q c ↑p) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c ↑q)

The components m ↦ θ_q⁻¹(E_q b θ_p m) of left multiplication by b.

theorem MultiplicativeBasisDeformations.MeshWalk.θ_ξ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b : B) (p q : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : (θ Ls S hleft Vx q) ((ξ Ls S hleft Vx b p q) m) = Ep S q * b * (θ Ls S hleft Vx p) m

theorem MultiplicativeBasisDeformations.MeshWalk.ξ_act {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b : B) (p q : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (x : B) : (ξ Ls S hleft Vx b p q) (((Ls.L ↑p).act m) x) = ((Ls.L ↑q).act ((ξ Ls S hleft Vx b p q) m)) x

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Ξ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b : B) : (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)ᵐᵒᵖ

Left multiplication, as an element of the corner algebra.

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_Ξ {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b : B) (p q : D.PV) : toLin (MulOpposite.unop (Ξ Ls S hleft Vx b) p q) = ξ Ls S hleft Vx b p q

theorem MultiplicativeBasisDeformations.MeshWalk.θ_toLin_idTo {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (p q : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : (θ Ls S hleft Vx q) ((toLin (CatAlg.idTo p q)) m) = Ep S q * (θ Ls S hleft Vx p) m

theorem MultiplicativeBasisDeformations.MeshWalk.Ξ_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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) : Ξ Ls S hleft Vx 1 = 1

theorem MultiplicativeBasisDeformations.MeshWalk.Ξ_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b b' : B) : Ξ Ls S hleft Vx (b * b') = Ξ Ls S hleft Vx b * Ξ Ls S hleft Vx b'

theorem MultiplicativeBasisDeformations.MeshWalk.Ξ_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (b b' : B) : Ξ Ls S hleft Vx (b + b') = Ξ Ls S hleft Vx b + Ξ Ls S hleft Vx b'

theorem MultiplicativeBasisDeformations.MeshWalk.Ξ_smul {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (t : k) (b : B) : Ξ Ls S hleft Vx (t • b) = t • Ξ Ls S hleft Vx b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ΞAlg {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) : B →ₐ[k] (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)ᵐᵒᵖ

Left multiplication as an algebra map B → (End ⊕_p M_p^B)ᵒᵖ.

theorem MultiplicativeBasisDeformations.MeshWalk.ΞAlg_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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) : Function.Injective ⇑(ΞAlg Ls S hleft Vx)

Bijectivity by dimensions

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_Alg {k : Type u} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : ι → 𝒞} [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] : Module.finrank k (CatAlg.Alg F) = ∑ x : ι, ∑ y : ι, Module.finrank k (F x ⟶ F y)

instance MultiplicativeBasisDeformations.MeshWalk.finiteDimensional_Alg {k : Type u} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : ι → 𝒞} [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] : FiniteDimensional k (CatAlg.Alg F)

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_corner {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) : Module.finrank k (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)ᵐᵒᵖ = Module.finrank k B

theorem MultiplicativeBasisDeformations.MeshWalk.ΞAlg_bijective {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) : Function.Bijective ⇑(ΞAlg Ls S hleft Vx)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cornerEquiv {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (S : P.Split) (hleft : ∀ (i : Fin (vxIdem D hfin).n) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), S.φ ((vxIdem D hfin).e i * a) = S.φ ((vxIdem D hfin).e i) * S.φ a) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) : B ≃ₐ[k] (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)ᵐᵒᵖ

The corner algebra of the lifted modules at the projective labels is B.