Graded vertex simples of a path algebra and their first-arrow resolution #
Let kQ carry its path-length grading, extended by zero to ℤ, let the quiver have finitely
many vertices, and let i be a vertex with finitely many arrows out of it. The graded vertex
simple Sᵢ is the head kQ eᵢ / A₊eᵢ of the graded vertex projective kQ eᵢ, free of rank one
over k and concentrated in degree zero. When k is a field it is a simple graded module. A path
of positive length starting at i is uniquely an arrow a : i ⟶ j followed by a path out of j,
so A₊eᵢ is the direct sum of the left ideals kQ a ≅ (kQ eⱼ){1}. The shift records that a has
degree one. This gives the short exact sequence of graded modules
0 ⟶ ⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ ⟶ Sᵢ ⟶ 0,
the graded form of the first-arrow resolution of a vertex simple. No acyclicity is needed for it,
and it shows that Sᵢ has projective dimension at most one. It is the resolution through which
graded Hom and Ext computations on the vertex projectives pass to the graded simples.
For a finite acyclic quiver the graded vertex simples are, up to shift, all the simple finite
graded modules, and their classes form a basis of G₀^gr(mod kQ) over ℤ[q,q⁻¹] whose
coordinates are the idempotent graded dimensions.
Main definitions #
TauCeti.PathAlgebra.gradedVertexSimple: the graded vertex simpleSᵢ.TauCeti.PathAlgebra.gradedVertexProjectiveToSimple: the quotient mapkQ eᵢ ⟶ Sᵢ.TauCeti.PathAlgebra.gradedVertexProjectiveArrowHom: the map(kQ eⱼ){1} ⟶ kQ eᵢ,x ↦ x a, of an arrowa : i ⟶ j.TauCeti.PathAlgebra.gradedArrowSum: the graded module⨁_{a : i ⟶ j} (kQ eⱼ){1}.TauCeti.PathAlgebra.gradedVertexSimpleResolution: the first-arrow short complex.TauCeti.PathAlgebra.gradedVertexSimpleClassBasis: the basis[Sᵢ]ofG₀^gr(mod kQ).
Main results #
TauCeti.PathAlgebra.gradedPositiveMulIdeal_vertexIdempotent_eq_span_range_ofArrow:A₊eᵢis the left ideal generated by the arrows out ofi.TauCeti.PathAlgebra.shortExact_gradedVertexSimpleResolution: the graded first-arrow sequence is short exact.TauCeti.PathAlgebra.hasProjectiveDimensionLT_two_gradedVertexSimple:Sᵢhas projective dimension at most one.TauCeti.PathAlgebra.simple_gradedVertexSimpleandTauCeti.PathAlgebra.isExhaustiveGradedSimpleFamily_gradedVertexSimple: theSᵢare simple, and for a finite acyclic quiver every simple finite graded module is a shift of one of them.
References #
- I. Assem, D. Simson and A. Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Sections 2--3, for the projective resolution of a vertex simple.
- C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded projective modules and grading shifts.
- Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for graded
Grothendieck groups over
ℤ[q,q⁻¹].
The resolution follows the ungraded first-arrow resolution of
TauCeti/RepresentationTheory/Quiver/Representation/Projective/Simple/Resolution.lean, and the
instantiation of the graded-head simplicity, exhaustiveness and class-basis results follows the
zigzag graded simples of TauCeti/RepresentationTheory/Quiver/Zigzag/Projective/CartanMap.lean.
The positive part of a vertex projective is generated by the arrows out of the vertex. For
the path-length grading, the left ideal A₊eᵢ generated by the products x eᵢ with x of positive
degree is the left ideal generated by the arrows a : i ⟶ j: a path of positive length starting at
i is its first arrow followed by a path.
The graded vertex simple Sᵢ of the path algebra with its path-length grading: the
quotient of the graded vertex projective kQ eᵢ by the span of the paths of positive length
starting at i.
Instances For
The graded vertex simple is the generic quotient A eᵢ / A₊ eᵢ of
TauCeti.gradedPositiveMulQuotient.
An element of kQ eᵢ maps to zero in Sᵢ exactly when it lies in the left ideal generated by
the arrows out of i.
The morphism of an arrow: for a : i ⟶ j, the graded map (kQ eⱼ){1} ⟶ kQ eᵢ,
x ↦ x a, which composes a path out of j after the arrow a. The shift accounts for the
arrow raising path length by one.
Instances For
The morphism of an arrow a is right multiplication by a.
The graded module ⨁_{a : i ⟶ j} (kQ eⱼ){1}, one shifted vertex projective for each arrow out
of i, graded degreewise.
Instances For
The direct sum of the shifted vertex projectives indexed by arrows out of a vertex is finitely generated as a graded module.
The kernel of kQ eᵢ ↠ Sᵢ as a direct sum: the graded map
⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ whose component at a is the morphism
TauCeti.PathAlgebra.gradedVertexProjectiveArrowHom of the arrow a.
Instances For
On elements, ⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ sends a family (x_a) to ∑_a x_a a.
The composite ⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ ⟶ Sᵢ vanishes: every ∑_a x_a a lies in
the left ideal generated by the arrows out of i.
The composite ⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ ⟶ Sᵢ vanishes: every ∑_a x_a a lies in
the left ideal generated by the arrows out of i.
The first-arrow sequence of a graded vertex simple:
0 ⟶ ⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ ⟶ Sᵢ ⟶ 0, the left map prefixing the arrows out of i
and the right map the quotient onto the graded head. Use gradedVertexSimpleResolution_def to
read off its objects and maps.
Instances For
The first-arrow sequence is the short complex built from
gradedArrowSumToVertexProjective and gradedVertexProjectiveToSimple.
⨁_{a : i ⟶ j} (kQ eⱼ){1} ⟶ kQ eᵢ is a monomorphism: by the uniqueness of the
first-arrow decomposition, ∑_a x_a a = 0 with x_a ∈ kQ eⱼ forces every x_a to vanish.
A graded vertex simple has projective dimension at most one: its first-arrow sequence is a projective resolution of length one.
Simplicity and the simple-class basis #
A graded vertex simple is a finite graded module.
Every simple finite graded kQ-module is a shift Sᵢ{d} of a graded vertex simple, for a
finite acyclic quiver.
The simple-class basis of G₀^gr(mod kQ) over ℤ[q,q⁻¹], for a finite acyclic quiver:
its vector at i is the class [Sᵢ] of the graded vertex simple.
Instances For
The basis vector of TauCeti.PathAlgebra.gradedVertexSimpleClassBasis at i is the class
[Sᵢ].
The coordinates in the basis [Sᵢ] are the idempotent coordinates of the vertex idempotents:
the ith coordinate of [M] is ∑ₚ dim_k(eᵢ • Mₚ) qᵖ.