Spanning the graded projective Grothendieck group

Over a finite-dimensional algebra, every finite graded projective is a finite direct sum of indecomposable graded projectives. If a family meets all such indecomposables up to internal shift, its classes span K₀^gr(proj A) over ℤ[q,q⁻¹]: shifting a summand by d multiplies its class by qᵈ.

No uniqueness of decomposition or splitting-field hypothesis is needed. This result supplies the spanning half of a projective-class basis, whose coordinates can then express the graded Cartan map. Indecomposability is taken in the full category of finite graded projectives.

Main results

• TauCeti.span_range_laurentK0_projective_of_eq_top: a family exhaustive among indecomposable graded projectives up to shift spans the Laurent Grothendieck group.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.
• C. A. Weibel, The K-book, Chapter II, Sections 5 and 7.
• TauCeti.RepresentationTheory.GrothendieckGroup.ProjectiveBasis: this result is the graded analogue of its ungraded projective-class spanning theorem and exhaustiveness API.
• TauCeti.Algebra.Category.GradedModuleCat.CartanMap.SimpleBasis: the graded simple-class basis.

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

A family of finite graded projectives is exhaustive up to shift if every indecomposable object of their full subcategory is isomorphic to an internal shift of a member of the family.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.isExhaustiveGradedIndecomposableProjectiveFamily_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (P : I → (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : IsExhaustiveGradedIndecomposableProjectiveFamily P ↔ ∀ (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory), CategoryTheory.Indecomposable M → ∃ (i : I) (d : ℤ), Nonempty (M ≅ { obj := (P i).obj.shiftObj d, property := ⋯ })

Characterization of exhaustiveness up to shift without unfolding the definition.

theorem TauCeti.span_range_laurentK0_projective_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} (P : I → (gradedFiniteProjectiveModules 𝒜).FullSubcategory) (hP : IsExhaustiveGradedIndecomposableProjectiveFamily P) : Submodule.span (LaurentPolynomial ℤ) (Set.range fun (i : I) => LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) (P i)) = ⊤

The classes of a family exhaustive among indecomposable graded projectives up to shift span K₀^gr(proj A) over ℤ[q,q⁻¹]. Every finite graded projective splits into finitely many indecomposable summands, and the class of a shifted summand is a Laurent monomial times the class of a member of the family. No independence or uniqueness of decomposition is assumed.