Corollary 12.1: all modules over a positive deformation #
deformation-refinements.tex: every positive filtered deformation B of A₀ is
representation-finite, and the lifted normalized modules M_x^B exhaust its indecomposables.
Formalization. The lifted modules carry mesh data (meshB, LiftedMeshData.lean) with the
injective labels of A₀ (injB, the dimensions agree with C by finrank_FB), and their corner
algebra at the projective labels is B (cornerEquiv, LiftedCorner.lean). Proposition 2.10
applied to this mesh data gives representation-finiteness, and every indecomposable is an
evaluated module; the evaluation of M_x^B at the regular projectives φ(e_p) B ≅ M_p^B is
M_x^B itself (evIso).
Evaluation at the regular projectives #
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_u
{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)), (θ Ls S hleft Vx p) m = Ep S p
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.uB
{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)
The generator u_p ∈ M_p^B corresponding to E_p ∈ E_p B.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.θ_uB
{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)
:
theorem
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)}
[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)
(n : CatAlg.Rep D.F0 (meshFam Q c ↑p))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.uB_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)
(n : CatAlg.Rep D.F0 (meshFam Q c ↑p))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.uB_act_θ_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}
{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}
(h : p ≠ q)
(n : CatAlg.Rep D.F0 (meshFam Q c ↑p))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.sum_ξ_uB
{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)
(q : D.PV)
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.evB
{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)
(x : V)
:
CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)
The evaluation ⊕_p Hom(M_p^B, M_x^B) → M_x^B, f ↦ Σ_p f_p(u_p).
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.evB_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}
{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)
(x : V)
(f : CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x))
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.evBInv
{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)
(x : V)
(m : CatAlg.Rep D.F0 (meshFam Q c x))
:
CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x)
The inverse: m ↦ (n ↦ m · θ_p(n))_p.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.evB_evBInv
{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)
(x : V)
(m : CatAlg.Rep D.F0 (meshFam Q c x))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.evBInv_evB
{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)
(x : V)
(f : CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.evB_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)
(x : V)
(b : B)
(f : CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x))
:
Every indecomposable is a lifted module #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.eOpB
{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ᵐᵒᵖ ≃+* CatAlg.Alg fun (p : D.PV) => FB Ls ↑p
Bᵐᵒᵖ ≅ Alg F₀ from the corner.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.eOpB_symm_algebraMap
{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)
(t : k)
:
(eOpB Ls S hleft Vx J h1).symm ((algebraMap k (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)) t) = (algebraMap k Bᵐᵒᵖ) t
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.evLin
{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)
(x : V)
(J : D.InjData)
(h1 : DegOne D)
:
↑((ModuleCat.restrictScalars (eOpB Ls S hleft Vx J h1).toRingHom).obj
(ModuleCat.of (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p)
(CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x)))) ≃ₗ[Bᵐᵒᵖ] ↑(FB Ls x)
The evaluation of M_x^B, as a B-linear isomorphism.
Instances For
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.evIso
{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)
(x : V)
(J : D.InjData)
(h1 : DegOne D)
:
(ModuleCat.restrictScalars (eOpB Ls S hleft Vx J h1).toRingHom).obj
(ModuleCat.of (CatAlg.Alg fun (p : D.PV) => FB Ls ↑p) (CatAlg.Rep (fun (p : D.PV) => FB Ls ↑p) (FB Ls x))) ≅ FB Ls x
The evaluation of M_x^B is M_x^B.
Instances For
def
MultiplicativeBasisDeformations.MeshWalk.injB
{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)
(Vx : (lenA0 D hfin).Vertices)
(J : D.InjData)
(h1 : DegOne D)
(hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y)
:
The injective labels of the lifted mesh data are those of A₀.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.finiteDimensional_B
{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)
:
FiniteDimensional k B
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_iso_FB
{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)
(hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y)
(M : RightModuleCat B)
(hM : IsFiniteIndecomposable k B M)
:
∃ (x : V), Nonempty (M ≅ FB Ls x)
The lifted modules exhaust the indecomposable B-modules.
The skeleton of ind(mod B) #
def
MultiplicativeBasisDeformations.MeshWalk.fbK
{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}
(x : V)
:
CatAlg.Rep D.F0 (meshFam Q c x) →ₗ[k] ↑(FB Ls x)
The identity of M_x^B from the native k-structure.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.isFiniteIndecomposable_FB
{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)
(Vx : (lenA0 D hfin).Vertices)
(x : V)
:
IsFiniteIndecomposable k B (FB Ls x)
theorem
MultiplicativeBasisDeformations.MeshWalk.eq_of_iso_FB
{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)
(Vx : (lenA0 D hfin).Vertices)
{x y : V}
(e : FB Ls x ≅ FB Ls y)
:
x = y
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.skelB
{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)
(hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y)
:
IndSkeleton k B
The lifted modules as a skeleton of ind(mod B).
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.skelB_obj
{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)
(hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y)
(x : V)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.isRepresentationFinite_B
{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)
(hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y)
: