Lemma 8.8 for bound quiver algebras

lem:dimension-infinity (local-ray-geometry.tex): "Let kQ/(ρ_1, …, ρ_t) be a finite-dimensional bound quiver algebra, with each relation between radical paths with specified endpoints. For a nonzero dimension vector d, put D = Σ_v d_v², N = Σ_{a : v → w} d_v d_w, F = Σ_i d_{source(ρ_i)} d_{target(ρ_i)}. If N − F ≥ D, the algebra is representation-infinite."

The algebra kQ/(ρ) is the category algebra of the relation category kQ/(ρ) (path-order product). A point x of the representation space (matrices on the arrows) gives the arrow maps of a representation; the relations evaluate to the matrices relMat x i, whose entries are F polynomials in the coordinates (relP), vanishing at 0 (the relations have no length-zero part) and stable under ∏ GL_{d v} (relMat_act). A point of their zero set gives a functor kQ/(ρ) → Mod k (Φ), hence a right module of dimension Σ d_v (repObj), and isomorphic modules come from conjugate points (conj_of_iso). Finite representation type would give finitely many orbits, contradicting OrbitDim.orbits_not_finite (not_isRepresentationFinite_bound).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.Arr (V : Type) [Quiver V] : Type

The arrows.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.src {V : Type} [Quiver V] (a : Arr V) : V

The source of an arrow.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.tgt {V : Type} [Quiver V] (a : Arr V) : V

The target of an arrow.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.Pt (k : Type u) {V : Type} [Quiver V] (d : V → ℕ) : Type u

The points of the representation space.

Path matrices

@[irreducible]

def MultiplicativeBasisDeformations.BoundQuiver.pathMat {k : Type u} [Field k] {V : Type} [Quiver V] (d : V → ℕ) (x : Pt k d) {u v : V} : Quiver.Path u v → Matrix (Fin (d v)) (Fin (d u)) k

The matrix of a path at a point (path order: M_{p a} = M_a M_p).

theorem MultiplicativeBasisDeformations.BoundQuiver.pathMat_nil {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (x : Pt k d) (u : V) : pathMat d x Quiver.Path.nil = 1

theorem MultiplicativeBasisDeformations.BoundQuiver.pathMat_cons {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (x : Pt k d) {u v w : V} (p : Quiver.Path u v) (e : v ⟶ w) : pathMat d x (p.cons e) = OrbitDim.mat x ⟨v, ⟨w, e⟩⟩ * pathMat d x p

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.matP (k : Type u) [Field k] {V : Type} [Quiver V] (d : V → ℕ) (a : Arr V) : Matrix (Fin (d (tgt a))) (Fin (d (src a))) (MvPolynomial (OrbitDim.Coord d src tgt) k)

The generic matrix of an arrow.

@[irreducible]

def MultiplicativeBasisDeformations.BoundQuiver.pathMatP (k : Type u) [Field k] {V : Type} [Quiver V] (d : V → ℕ) {u v : V} : Quiver.Path u v → Matrix (Fin (d v)) (Fin (d u)) (MvPolynomial (OrbitDim.Coord d src tgt) k)

The polynomial matrix of a path.

theorem MultiplicativeBasisDeformations.BoundQuiver.map_pathMatP {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (x : Pt k d) {u v : V} (p : Quiver.Path u v) : (pathMatP k d p).map ⇑(MvPolynomial.eval x) = pathMat d x p

theorem MultiplicativeBasisDeformations.BoundQuiver.pathMat_act {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (g : (v : V) → GL (Fin (d v)) k) (x : Pt k d) {u v : V} (p : Quiver.Path u v) : pathMat d (OrbitDim.act g x) p = ↑(g v) * pathMat d x p * ↑(g u)⁻¹

theorem MultiplicativeBasisDeformations.BoundQuiver.pathMat_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {u v : V} (p : Quiver.Path u v) (hp : p.length ≠ 0) : pathMat d 0 p = 0

The relations

def MultiplicativeBasisDeformations.BoundQuiver.relMat {k : Type u} [Field k] {V : Type} [Quiver V] (d : V → ℕ) {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (x : Pt k d) (i : ι) : Matrix (Fin (d (t i))) (Fin (d (s i))) k

The matrix of a relation at a point.

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.relP {k : Type u} [Field k] {V : Type} [Quiver V] (d : V → ℕ) {ι : Type} (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (i : ι) : Matrix (Fin (d (t i))) (Fin (d (s i))) (MvPolynomial (OrbitDim.Coord d src tgt) k)

The polynomial matrix of a relation.

theorem MultiplicativeBasisDeformations.BoundQuiver.eval_relP {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (x : Pt k d) (i : ι) (a : Fin (d (t i))) (b : Fin (d (s i))) : (MvPolynomial.eval x) (relP d s t r i a b) = relMat d s t r x i a b

theorem MultiplicativeBasisDeformations.BoundQuiver.relMat_act {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (g : (v : V) → GL (Fin (d v)) k) (x : Pt k d) (i : ι) : relMat d s t r (OrbitDim.act g x) i = ↑(g (t i)) * relMat d s t r x i * ↑(g (s i))⁻¹

theorem MultiplicativeBasisDeformations.BoundQuiver.relMat_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) (hrad : ∀ (i : ι), (LinearPaths.proj 0 (s i) (t i)) (r i) = 0) (i : ι) : relMat d s t r 0 i = 0

Realization in Mod k

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.Sp (k : Type u) [Field k] {V : Type} (d : V → ℕ) (v : V) : ModuleCat k

The space k^{d v}.

def MultiplicativeBasisDeformations.BoundQuiver.Lx {k : Type u} [Field k] {V : Type} [Quiver V] (d : V → ℕ) (x : Pt k d) {u v : V} (e : u ⟶ v) : Sp k d u ⟶ Sp k d v

The arrow maps of a point.

theorem MultiplicativeBasisDeformations.BoundQuiver.pathMap_Lx {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (x : Pt k d) {u v : V} (p : Quiver.Path u v) : GeneralNormalForm.pathMap (fun {x_1 y : V} => Lx d x) p = ModuleCat.ofHom (Matrix.toLin' (pathMat d x p))

theorem MultiplicativeBasisDeformations.BoundQuiver.realize_Lx {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) (x : Pt k d) {u v : V} (P : LinearPaths.obj u ⟶ LinearPaths.obj v) : (GeneralNormalForm.realize (fun {x_1 y : V} => Lx d x) u v) P = ModuleCat.ofHom (Matrix.toLin' ((LinearPaths.toFinsupp P).sum fun (p : Quiver.Path u v) (c : k) => c • pathMat d x p))

The functor and the module of a point

theorem MultiplicativeBasisDeformations.BoundQuiver.realize_eq_zero_of_mem {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} {G : LinearPaths.obj u ⟶ LinearPaths.obj v} (hG : G ∈ (CategoricalIdeal.HomIdeal.linearSpan k (GeneralNormalForm.Rel s t r)).hom (LinearPaths.obj u) (LinearPaths.obj v)) : (GeneralNormalForm.realize (fun {x_1 y : V} => Lx d x) u v) G = 0

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.Φ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : CategoryTheory.Functor (RelationCategory k (GeneralNormalForm.Rel s t r)) (ModuleCat k)

The functor kQ/(ρ) → Mod k of a point of the zero set.

theorem MultiplicativeBasisDeformations.BoundQuiver.Φ_map_cl {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (P : LinearPaths.obj u ⟶ LinearPaths.obj v) : (Φ d x hx).map ((GeneralNormalForm.cl s t r).map P) = (GeneralNormalForm.realize (fun {x_1 y : V} => Lx d x) u v) P

theorem MultiplicativeBasisDeformations.BoundQuiver.Φ_map_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (c c' : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) : (Φ d x hx).map (c + c') = (Φ d x hx).map c + (Φ d x hx).map c'

theorem MultiplicativeBasisDeformations.BoundQuiver.Φ_map_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (a : k) (c : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) : (Φ d x hx).map (a • c) = a • (Φ d x hx).map c

theorem MultiplicativeBasisDeformations.BoundQuiver.Φ_map_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} : (Φ d x hx).map 0 = 0

theorem MultiplicativeBasisDeformations.BoundQuiver.Φ_map_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} {κ : Type u_1} (F : Finset κ) (c : κ → (GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v)) : (Φ d x hx).map (∑ j ∈ F, c j) = ∑ j ∈ F, (Φ d x hx).map (c j)

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.Φl {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (c : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) : (Fin (d u) → k) →ₗ[k] Fin (d v) → k

The linear map of a morphism of kQ/(ρ).

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (c c' : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) : Φl d x hx (c + c') = Φl d x hx c + Φl d x hx c'

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (a : k) (c : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) : Φl d x hx (a • c) = a • Φl d x hx c

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} : Φl d x hx 0 = 0

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} {κ : Type u_1} (F : Finset κ) (c : κ → (GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v)) : Φl d x hx (∑ j ∈ F, c j) = ∑ j ∈ F, Φl d x hx (c j)

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v w : V} (c : GeneralNormalForm.clObj s t r u ⟶ GeneralNormalForm.clObj s t r v) (c' : GeneralNormalForm.clObj s t r v ⟶ GeneralNormalForm.clObj s t r w) : Φl d x hx (CategoryTheory.CategoryStruct.comp c c') = Φl d x hx c' ∘ₗ Φl d x hx c

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_id {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (u : V) : Φl d x hx (CategoryTheory.CategoryStruct.id (GeneralNormalForm.clObj s t r u)) = LinearMap.id

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_idTo_ne {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {u v : V} (h : u ≠ v) : Φl d x hx (CatAlg.idTo u v) = 0

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.act {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k) (v : V) : Fin (d v) → k

The action of the bound quiver algebra on ⊕_v k^{d v}.

theorem MultiplicativeBasisDeformations.BoundQuiver.act_mul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (a b : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k) : act d x hx (b * a) w = act d x hx a (act d x hx b w)

theorem MultiplicativeBasisDeformations.BoundQuiver.act_one {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (w : (v : V) → Fin (d v) → k) : act d x hx 1 w = w

theorem MultiplicativeBasisDeformations.BoundQuiver.act_algebraMap {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (c : k) (w : (v : V) → Fin (d v) → k) : act d x hx ((algebraMap k (CatAlg.Alg (GeneralNormalForm.clObj s t r))) c) w = c • w

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.BoundQuiver.Car {k : Type u} {V : Type} [Quiver V] (d : V → ℕ) (_x : Pt k d) : Type u

The carrier.

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.repModule {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : Module (CatAlg.Alg (GeneralNormalForm.clObj s t r))ᵐᵒᵖ (Car d x)

The right module structure.

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.repObj {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : RightModuleCat (CatAlg.Alg (GeneralNormalForm.clObj s t r))

The module of a point.

def MultiplicativeBasisDeformations.BoundQuiver.toPi {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : ↑(repObj d x hx) →ₗ[k] (v : V) → Fin (d v) → k

The identification with ∏ k^{d v} is k-linear.

theorem MultiplicativeBasisDeformations.BoundQuiver.repObj_finite {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : Module.Finite k ↑(repObj d x hx)

theorem MultiplicativeBasisDeformations.BoundQuiver.finrank_repObj_le {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) : Module.finrank k ↑(repObj d x hx) ≤ ∑ v : V, d v

Isomorphisms are conjugations

theorem MultiplicativeBasisDeformations.BoundQuiver.act_sgl {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (p q : V) (c : GeneralNormalForm.clObj s t r p ⟶ GeneralNormalForm.clObj s t r q) (w : (v : V) → Fin (d v) → k) : act d x hx (GeneralNormalForm.sgl p q c) w = Pi.single q ((Φl d x hx c) (w p))

theorem MultiplicativeBasisDeformations.BoundQuiver.Φl_arrow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) {p q : V} (e : p ⟶ q) : Φl d x hx ((GeneralNormalForm.cl s t r).map (LinearPaths.arrow e)) = Matrix.toLin' (OrbitDim.mat x ⟨p, ⟨q, e⟩⟩)

def MultiplicativeBasisDeformations.BoundQuiver.comp {k : Type u} [Field k] {V : Type} [DecidableEq V] (d : V → ℕ) (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (v : V) (w : Fin (d v) → k) : Fin (d v) → k

The component maps of an isomorphism.

theorem MultiplicativeBasisDeformations.BoundQuiver.f_single {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {x y : Pt k d} {hx : ∀ (i : ι), relMat d s t r x i = 0} {hy : ∀ (i : ι), relMat d s t r y i = 0} (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hf : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), f (act d x hx a w) = act d y hy a (f w)) (v : V) (w : Fin (d v) → k) : f (Pi.single v w) = Pi.single v (comp d f v w)

theorem MultiplicativeBasisDeformations.BoundQuiver.f_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {x y : Pt k d} {hx : ∀ (i : ι), relMat d s t r x i = 0} {hy : ∀ (i : ι), relMat d s t r y i = 0} (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hf : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), f (act d x hx a w) = act d y hy a (f w)) (c : k) (w : (v : V) → Fin (d v) → k) : f (c • w) = c • f w

def MultiplicativeBasisDeformations.BoundQuiver.compL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {x y : Pt k d} {hx : ∀ (i : ι), relMat d s t r x i = 0} {hy : ∀ (i : ι), relMat d s t r y i = 0} (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hf : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), f (act d x hx a w) = act d y hy a (f w)) (hfa : ∀ (w w' : (v : V) → Fin (d v) → k), f (w + w') = f w + f w') (v : V) : (Fin (d v) → k) →ₗ[k] Fin (d v) → k

The component maps as linear maps.

theorem MultiplicativeBasisDeformations.BoundQuiver.comp_arrow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {x y : Pt k d} {hx : ∀ (i : ι), relMat d s t r x i = 0} {hy : ∀ (i : ι), relMat d s t r y i = 0} (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hf : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), f (act d x hx a w) = act d y hy a (f w)) (hfa : ∀ (w w' : (v : V) → Fin (d v) → k), f (w + w') = f w + f w') {p q : V} (e : p ⟶ q) (u : Fin (d p) → k) : (compL d f hf hfa q) ((Matrix.toLin' (OrbitDim.mat x ⟨p, ⟨q, e⟩⟩)) u) = (Matrix.toLin' (OrbitDim.mat y ⟨p, ⟨q, e⟩⟩)) ((compL d f hf hfa p) u)

The arrow relation g_q M_e = M'_e g_p.

theorem MultiplicativeBasisDeformations.BoundQuiver.comp_left_inv {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} {x y : Pt k d} {hx : ∀ (i : ι), relMat d s t r x i = 0} {hy : ∀ (i : ι), relMat d s t r y i = 0} (f : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hf : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), f (act d x hx a w) = act d y hy a (f w)) (hfa : ∀ (w w' : (v : V) → Fin (d v) → k), f (w + w') = f w + f w') (g : ((v : V) → Fin (d v) → k) → (v : V) → Fin (d v) → k) (hg : ∀ (a : CatAlg.Alg (GeneralNormalForm.clObj s t r)) (w : (v : V) → Fin (d v) → k), g (act d y hy a w) = act d x hx a (g w)) (hga : ∀ (w w' : (v : V) → Fin (d v) → k), g (w + w') = g w + g w') (hgf : ∀ (w : (v : V) → Fin (d v) → k), g (f w) = w) (v : V) (u : Fin (d v) → k) : (compL d g hg hga v) ((compL d f hf hfa v) u) = u

theorem MultiplicativeBasisDeformations.BoundQuiver.conj_of_iso {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] {s t : ι → V} {r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)} (x y : Pt k d) (hx : ∀ (i : ι), relMat d s t r x i = 0) (hy : ∀ (i : ι), relMat d s t r y i = 0) (L : ↑(repObj d x hx) ≃ₗ[(CatAlg.Alg (GeneralNormalForm.clObj s t r))ᵐᵒᵖ] ↑(repObj d y hy)) : ∃ (g : (v : V) → GL (Fin (d v)) k), y = OrbitDim.act g x

Isomorphic modules are conjugate points.

Lemma 8.8

noncomputable def MultiplicativeBasisDeformations.BoundQuiver.Obj {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)) {N : ℕ} (X : Fin N → RightModuleCat (CatAlg.Alg (GeneralNormalForm.clObj s t r))) (B : ℕ) (τ : (m : Fin (B + 1)) × (Fin ↑m → Fin N)) : RightModuleCat (CatAlg.Alg (GeneralNormalForm.clObj s t r))

The labelled biproducts.

theorem MultiplicativeBasisDeformations.BoundQuiver.not_isRepresentationFinite_bound {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] (d : V → ℕ) {ι : Type} [Fintype ι] (s t : ι → V) (r : (i : ι) → LinearPaths.obj (s i) ⟶ LinearPaths.obj (t i)) [IsAlgClosed k] [FiniteDimensional k (CatAlg.Alg (GeneralNormalForm.clObj s t r))] (hrad : ∀ (i : ι), (LinearPaths.proj 0 (s i) (t i)) (r i) = 0) (hd : ∃ (v : V), 0 < d v) (hNF : ∑ v : V, d v ^ 2 + ∑ i : ι, d (s i) * d (t i) ≤ ∑ a : Arr V, d (src a) * d (tgt a)) : ¬IsRepresentationFinite k (CatAlg.Alg (GeneralNormalForm.clObj s t r))

Lemma 8.8 (lem:dimension-infinity): let kQ/(ρ₁, …, ρ_t) be a finite-dimensional bound quiver algebra (the category algebra of the relation category, path-order product), each relation ρ_i : s_i → t_i a combination of paths of positive length. For a nonzero dimension vector d with N − F ≥ D, i.e. Σ_v d_v² + Σ_i d_{s_i} d_{t_i} ≤ Σ_{a : v → w} d_v d_w, the algebra is representation-infinite.