Simple classes in the graded Grothendieck group of finite graded modules

Let A be a finite-dimensional algebra over a field k, with homogeneous pieces 𝒜 : ℤ → Submodule k A. A finite graded A-module is finite-dimensional over k, so it has a filtration by graded submodules whose successive quotients are simple objects of the graded module category. If every simple finite graded module is an internal shift Sᵢ{d} of a member of a family S, the relation [M{d}] = qᵈ [M] turns such a filtration into an expression of [M] as a ℤ[q,q⁻¹]-linear combination of the classes [Sᵢ]. Thus these classes span the graded Grothendieck group G₀^gr(mod A) over the Laurent ring.

This is the spanning half of the simple-class basis of G₀^gr(mod A). Linear independence is read off from the idempotent coordinates TauCeti.gradedIdempotentCoordinate: if degree-zero idempotents eᵢ satisfy gdim(eᵢ • Sⱼ) = δᵢⱼ, as for the vertex idempotents and vertex simples of a basic algebra whose simple modules are one-dimensional, the classes [Sᵢ] form a ℤ[q,q⁻¹]-basis whose coordinates are the idempotent coordinates. This basis is the module-side basis of the graded Cartan matrix TauCeti.gradedCartanMatrix.

Main definitions

• TauCeti.IsExhaustiveGradedSimpleFamily: every simple finite graded module is isomorphic to an internal shift of a member of the family.
• TauCeti.gradedSimpleClassBasis: the ℤ[q,q⁻¹]-basis of G₀^gr(mod A) given by an exhaustive family with Kronecker-delta idempotent coordinates.

Main results

• TauCeti.span_range_laurentK0_of_eq_top: the classes of an exhaustive family span G₀^gr(mod A) over ℤ[q,q⁻¹].
• TauCeti.gradedSimpleClassBasis_repr_apply: the coordinates in the simple-class basis are the idempotent coordinates.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded modules and their degree shifts.
• Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for the graded Grothendieck group as a ℤ[q,q⁻¹]-module.

The argument adapts the ungraded simple-class basis of TauCeti.RepresentationTheory.GrothendieckGroup.SimpleBasis (TauCeti.simpleClassBasis) to graded modules and the Laurent-linear Grothendieck group.

Exhaustive families of graded simples

def TauCeti.IsExhaustiveGradedSimpleFamily {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) : Prop

A family of finite graded modules is an exhaustive family of graded simples up to shift if every finite graded module which is a simple object of the graded module category is isomorphic to an internal shift (S i){d} of a member of the family.

Equations

• TauCeti.IsExhaustiveGradedSimpleFamily S = ∀ (M : (TauCeti.gradedFiniteModules 𝒜).FullSubcategory), CategoryTheory.Simple M.obj → ∃ (i : I) (d : ℤ), Nonempty (M.obj ≅ (S i).obj.shiftObj d)

theorem TauCeti.isExhaustiveGradedSimpleFamily_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) : IsExhaustiveGradedSimpleFamily S ↔ ∀ (M : (gradedFiniteModules 𝒜).FullSubcategory), CategoryTheory.Simple M.obj → ∃ (i : I) (d : ℤ), Nonempty (M.obj ≅ (S i).obj.shiftObj d)

Characterization of IsExhaustiveGradedSimpleFamily, for importing modules, to which the body of the definition is not exposed.

Spanning

theorem TauCeti.span_range_laurentK0_of_eq_top {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) (hS : IsExhaustiveGradedSimpleFamily S) : Submodule.span (LaurentPolynomial ℤ) (Set.range fun (i : I) => LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) (S i)) = ⊤

The classes of an exhaustive family of graded simples span G₀^gr(mod A) over ℤ[q,q⁻¹]. A finite graded module has a filtration by graded submodules with simple subquotients, each of which is a shift Sᵢ{d} of a member of the family, with class qᵈ [Sᵢ].

The simple-class basis

noncomputable def TauCeti.gradedSimpleClassBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))

The simple-class basis of G₀^gr(mod A) over ℤ[q,q⁻¹]. Its basis vector at i is the class [Sᵢ]. The hypotheses say that the degree-zero idempotents eᵢ have graded dimensions gdim(eᵢ • Sⱼ) = δᵢⱼ, and that every simple finite graded module is a shift of some Sᵢ.

Equations

• TauCeti.gradedSimpleClassBasis S he he₀ hne hself hS = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.gradedSimpleClassBasis_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (i : I) : (gradedSimpleClassBasis S he he₀ hne hself hS) i = LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) (S i)

The basis vector indexed by i is the class [Sᵢ].

@[simp]

theorem TauCeti.gradedSimpleClassBasis_repr_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (x : LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) (i : I) : ((gradedSimpleClassBasis S he he₀ hne hself hS).repr x) i = (gradedIdempotentCoordinate ⋯ ⋯) x

The ith coordinate in the simple-class basis is the idempotent coordinate of eᵢ, the graded dimension of eᵢ • M on the class of M.