Exhausting graded projectives with homogeneous idempotents

For a finite-dimensional graded algebra, a complete family of homogeneous degree-zero idempotents whose associated graded ideals are indecomposable meets every finite graded indecomposable projective up to shift. Consequently their classes span the actual Laurent Grothendieck group of graded projectives.

A finite graded free cover splits over a projective. Resolving each of its regular summands using the complete idempotents expresses the identity of the projective as a finite sum of maps through shifted idempotent ideals. Its local endomorphism ring makes one summand invertible, and indecomposability of that ideal turns the resulting retract into an isomorphism. This argument needs no positivity assumption on the grading.

If the eᵢ are moreover primitive idempotents of A whose ungraded left ideals A eᵢ are pairwise nonisomorphic, then the classes [A eᵢ] form a basis of K₀^gr(proj A) over ℤ[q,q⁻¹]. A graded endomorphism or isomorphism is in particular an A-linear one, so indecomposability of the ungraded module A eᵢ makes the graded module A eᵢ indecomposable, and nonisomorphic ungraded modules A eᵢ, A eⱼ are not isomorphic up to any internal shift. These hypotheses involve no grading positivity and no splitting: the degree-zero corners eᵢ A eᵢ ∩ 𝒜 0 need not be the lines k eᵢ, so the field need not split the simple modules.

If A is nonnegatively graded and its degree-zero piece is spanned by the nonzero idempotents eᵢ, both hypotheses hold. The degree-zero part of the corner eᵢ A eᵢ is k eᵢ, and an idempotent of A without degree-zero component vanishes (TauCeti.GradedAlgebra.eq_zero_of_isIdempotentElem_of_decompose_zero), so each eᵢ is primitive. An isomorphism A eᵢ ≃ A eⱼ with i ≠ j would write eᵢ = x y with x ∈ eᵢ A eⱼ, while off-diagonal corners live in positive degrees, so the degree-zero component of x y vanishes. This is the projective counterpart of the basis of graded heads.

Main definitions

• TauCeti.gradedIdempotentProjectiveBasisOfPrimitive: the basis [A eᵢ] of K₀^gr(proj A) for primitive idempotents with pairwise nonisomorphic left ideals.
• TauCeti.gradedIdempotentProjectiveBasis: the same basis when the degree-zero piece of a nonnegatively graded algebra is spanned by the eᵢ.

Main results

• TauCeti.isExhaustiveGradedIndecomposableProjectiveFamily_of_completeOrthogonalIdempotents: indecomposable idempotent ideals A eᵢ exhaust the finite graded indecomposable projectives.
• TauCeti.indecomposable_ofIdeal_span_singleton: the graded projective A f of a primitive idempotent f is indecomposable.
• TauCeti.cornerSubmodule_inf_zero_eq_span_singleton and TauCeti.pos_of_mem_cornerSubmodule_inf: if the degree-zero piece of a nonnegatively graded algebra is spanned by orthogonal idempotents, its diagonal corners are k eᵢ in degree zero and its off-diagonal corners live in positive degrees.
• TauCeti.coe_decompose_mem_cornerSubmodule: the homogeneous components of an element of a corner aAb cut out by elements of degree zero lie in that corner.
• TauCeti.isPrimitiveIdempotent_of_gradeZero_le_span: each eᵢ is a primitive idempotent of A.
• TauCeti.isEmpty_linearEquiv_span_singleton_of_gradeZero_le_span: the ungraded modules A eᵢ are pairwise nonisomorphic.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.
• H. Krause, "Krull–Schmidt categories and projective covers", Expositiones Mathematicae 33 (2015), 535–549.

Homogeneous components in corners

theorem TauCeti.coe_decompose_mem_cornerSubmodule {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {a b x : A} (ha₀ : a ∈ 𝒜 0) (hb₀ : b ∈ 𝒜 0) (hx : x ∈ cornerSubmodule k a b) (p : ℤ) : ↑(((DirectSum.decompose 𝒜) x) p) ∈ cornerSubmodule k a b

The homogeneous components of an element of the corner aAb cut out by two elements of degree zero lie in the same corner.

Degree-zero corners

theorem TauCeti.cornerSubmodule_inf_zero_eq_span_singleton {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (ho : OrthogonalIdempotents e) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (i : I) : cornerSubmodule k (e i) (e i) ⊓ 𝒜 0 = k ∙ e i

The degree-zero part of a diagonal corner is the line through the idempotent: if the degree-zero piece of A is spanned by the orthogonal idempotents eᵢ, then eᵢ A eᵢ ∩ 𝒜 0 = k eᵢ.

theorem TauCeti.pos_of_mem_cornerSubmodule_inf {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} (ho : OrthogonalIdempotents e) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) {i j : I} (hij : i ≠ j) {p : ℤ} {x : A} (hx : x ∈ cornerSubmodule k (e i) (e j) ⊓ 𝒜 p) (hx₀ : x ≠ 0) : 0 < p

Off-diagonal corners live in positive degrees: in a nonnegatively graded algebra whose degree-zero piece is spanned by the orthogonal idempotents eᵢ, a nonzero homogeneous element of eᵢ A eⱼ with i ≠ j has positive degree.

theorem TauCeti.isPrimitiveIdempotent_of_gradeZero_le_span {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} {e : I → A} (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (ho : OrthogonalIdempotents e) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (i : I) (hne : e i ≠ 0) : IsPrimitiveIdempotent (e i)

Each eᵢ is a primitive idempotent of A when A is nonnegatively graded and its degree-zero piece is spanned by the orthogonal idempotents eᵢ.

theorem TauCeti.isEmpty_linearEquiv_span_singleton_of_gradeZero_le_span {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} {e : I → A} (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (ho : OrthogonalIdempotents e) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) {i j : I} (hij : i ≠ j) (hi : e i ≠ 0) : IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))

The ungraded modules A eᵢ are pairwise nonisomorphic when A is nonnegatively graded and its degree-zero piece is spanned by the orthogonal idempotents eᵢ.

theorem TauCeti.isExhaustiveGradedIndecomposableProjectiveFamily_of_completeOrthogonalIdempotents {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A] (hind : ∀ (i : I), CategoryTheory.Indecomposable { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ }) : IsExhaustiveGradedIndecomposableProjectiveFamily fun (i : I) => { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ }

A complete family of orthogonal idempotents whose left ideals are homogeneous and indecomposable exhausts all finite graded indecomposable projectives up to internal shift.

The idempotent projective basis

theorem TauCeti.indecomposable_ofIdeal_span_singleton {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {f : A} (hf : IsPrimitiveIdempotent f) (hfI : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) : CategoryTheory.Indecomposable { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {f}) hfI, property := ⋯ }

The graded projective A f of a primitive idempotent f is indecomposable. A graded endomorphism of A f is in particular an A-linear endomorphism, and A f is an indecomposable module (TauCeti.IsPrimitiveIdempotent.isIndecomposableModule), so its only idempotent graded endomorphisms are 0 and the identity. No hypothesis on the grading is needed.

noncomputable def TauCeti.gradedIdempotentProjectiveBasisOfPrimitive {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A] (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))

The graded projectives A eᵢ of primitive idempotents form a basis of K₀^gr(proj A) over ℤ[q,q⁻¹], for a finite-dimensional graded algebra with a complete family of orthogonal primitive idempotents eᵢ whose left ideals A eᵢ are homogeneous (so the eᵢ have degree zero) and, as ungraded modules, pairwise nonisomorphic. Its basis vector at i is the class [A eᵢ]. The degree-zero corners eᵢ A eᵢ ∩ 𝒜 0 need not be the lines k eᵢ, so the field need not split the simple modules. This is the graded counterpart of TauCeti.idempotentProjectiveBasis.

@[simp]

theorem TauCeti.gradedIdempotentProjectiveBasisOfPrimitive_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A] (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) (i : I) : (gradedIdempotentProjectiveBasisOfPrimitive he hI hprim hnoniso) i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ }

The basis vector of TauCeti.gradedIdempotentProjectiveBasisOfPrimitive at i is the class [A eᵢ].

noncomputable def TauCeti.gradedIdempotentProjectiveBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A] (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))

The graded projectives A eᵢ form a basis of K₀^gr(proj A) over ℤ[q,q⁻¹], for a nonnegatively graded finite-dimensional algebra whose degree-zero piece is spanned by a complete family of orthogonal nonzero idempotents eᵢ. Its basis vector at i is the class [A eᵢ]. This is the projective counterpart of the head basis TauCeti.gradedIdempotentHeadBasis, and the case of TauCeti.gradedIdempotentProjectiveBasisOfPrimitive where each eᵢ is primitive by TauCeti.isPrimitiveIdempotent_of_gradeZero_le_span and the A eᵢ are pairwise nonisomorphic by TauCeti.isEmpty_linearEquiv_span_singleton_of_gradeZero_le_span.

@[simp]

theorem TauCeti.gradedIdempotentProjectiveBasis_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A] (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) (i : I) : (gradedIdempotentProjectiveBasis he hI hneg hspan hne) i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ }

The basis vector of TauCeti.gradedIdempotentProjectiveBasis at i is the class [A eᵢ].