Indecomposable classes in the Grothendieck group of finitely generated projectives

Let R be an Artinian ring. Every finitely generated R-module has finite length, so the Krull-Schmidt theorem applies to it: it decomposes into indecomposable summands, uniquely up to a matching. The multiplicity of a fixed module among those summands is additive on direct sums, and the exact structure of the finitely generated projectives is the split one, so that multiplicity descends to an integer-valued coordinate on K₀(proj R).

These coordinates show that the classes of any pairwise nonisomorphic family of indecomposable finitely generated projective modules are linearly independent. If the family contains a representative of every indecomposable finitely generated projective, an induction on the length of a module also shows that the classes span, giving a canonical ℤ-basis of K₀(proj R) indexed by that family. The basis is the projective side of the projective/simple coordinates that express the Cartan map TauCeti.cartanMap as a matrix; the simple side is TauCeti.simpleClassBasis, in TauCeti/RepresentationTheory/GrothendieckGroup/SimpleBasis.lean.

Main definitions

• TauCeti.indecomposableCoordinate: the homomorphism from K₀(proj R) which reads the Krull-Schmidt multiplicity of a fixed module.
• TauCeti.IsExhaustiveIndecomposableProjectiveFamily: a family of finitely generated projective modules meeting every indecomposable one.
• TauCeti.indecomposableProjectiveClassBasis: the basis of K₀(proj R) given by an exhaustive family of pairwise nonisomorphic indecomposable finitely generated projective modules.

Main results

• TauCeti.indecomposableCoordinate_of: the coordinate of an object class is its Krull-Schmidt multiplicity.
• TauCeti.linearIndependent_exactK0_of: pairwise nonisomorphic indecomposable projective classes are linearly independent.
• TauCeti.span_range_exactK0_of_eq_top: an exhaustive family of indecomposable projective classes spans.
• TauCeti.isExhaustiveIndecomposableProjectiveFamily_of_isLocalRing: over a commutative local ring the ring itself is, up to isomorphism, the only indecomposable finitely generated projective module.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Sections 5 and 7.
• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter I, Section 4, and Chapter III, Section 3.
• The construction and proof architecture are adapted from TauCeti/RepresentationTheory/GrothendieckGroup/SimpleBasis.lean.

The multiplicity coordinates

noncomputable def TauCeti.indecomposableCoordinate (R : Type u) [Ring R] [IsArtinianRing R] (N : Type w) [AddCommGroup N] [Module R N] : ExactK0 (finiteProjectiveModulesExactStructure R) →+ ℤ

The Krull-Schmidt coordinate of a fixed module N on K₀(proj R). On the class of a finitely generated projective module M it is the number of summands of M isomorphic to N in a decomposition of M into indecomposables. It is useful as a coordinate when N is indecomposable, but the construction is valid for arbitrary N (and is identically zero when N is not indecomposable, by TauCeti.isIndecomposableModule_of_indecomposableMultiplicity_ne_zero).

Equations

• TauCeti.indecomposableCoordinate R N = TauCeti.ExactK0.lift (TauCeti.indecomposableInvariant✝ R N)

@[simp]

theorem TauCeti.indecomposableCoordinate_of (R : Type u) [Ring R] [IsArtinianRing R] (N : Type w) [AddCommGroup N] [Module R N] (X : (finiteProjectiveModules R).FullSubcategory) : (indecomposableCoordinate R N) (ExactK0.of X) = ↑(indecomposableMultiplicity R (↑X.obj) N)

The coordinate of an object class is its Krull-Schmidt multiplicity.

theorem TauCeti.indecomposableCoordinate_congr (R : Type u) [Ring R] [IsArtinianRing R] (N : Type w) [AddCommGroup N] [Module R N] {N' : Type w'} [AddCommGroup N'] [Module R N'] (e : N ≃ₗ[R] N') : indecomposableCoordinate R N = indecomposableCoordinate R N'

Linearly equivalent modules define the same Krull-Schmidt coordinate.

@[simp]

theorem TauCeti.indecomposableCoordinate_self {R : Type u} [Ring R] [IsArtinianRing R] (X : (finiteProjectiveModules R).FullSubcategory) (hX : IsIndecomposableModule R ↑X.obj) : (indecomposableCoordinate R ↑X.obj) (ExactK0.of X) = 1

An indecomposable module has coordinate one on its own class.

@[simp]

theorem TauCeti.indecomposableCoordinate_eq_zero_of_isEmpty_linearEquiv {R : Type u} [Ring R] [IsArtinianRing R] (X Y : (finiteProjectiveModules R).FullSubcategory) (hY : IsIndecomposableModule R ↑Y.obj) (h : IsEmpty (↑Y.obj ≃ₗ[R] ↑X.obj)) : (indecomposableCoordinate R ↑X.obj) (ExactK0.of Y) = 0

Two nonisomorphic indecomposable modules have zero mutual coordinate.

Linear independence and spanning

theorem TauCeti.linearIndependent_exactK0_of {R : Type u} [Ring R] [IsArtinianRing R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) : LinearIndependent ℤ fun (i : I) => ExactK0.of (P i)

Pairwise nonisomorphic indecomposable projective classes are linearly independent in K₀(proj R).

def TauCeti.IsExhaustiveIndecomposableProjectiveFamily {R : Type u} [Ring R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) : Prop

A family of finitely generated projective modules is exhaustive if every indecomposable finitely generated projective module is isomorphic to one of its members.

Equations

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

theorem TauCeti.isExhaustiveIndecomposableProjectiveFamily_iff {R : Type u} [Ring R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) : IsExhaustiveIndecomposableProjectiveFamily P ↔ ∀ (X : (finiteProjectiveModules R).FullSubcategory), IsIndecomposableModule R ↑X.obj → ∃ (i : I), Nonempty (↑X.obj ≃ₗ[R] ↑(P i).obj)

Characterization of TauCeti.IsExhaustiveIndecomposableProjectiveFamily: the family is exhaustive exactly when every indecomposable finitely generated projective module is isomorphic to one of its members. Importing modules build and use the predicate through this lemma, since the body of the definition above is not exposed to them.

theorem TauCeti.span_range_exactK0_of_eq_top {R : Type u} [Ring R] [IsArtinianRing R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) (hexh : IsExhaustiveIndecomposableProjectiveFamily P) : Submodule.span ℤ (Set.range fun (i : I) => ExactK0.of (P i)) = ⊤

An exhaustive family of indecomposable projective classes spans K₀(proj R). Every finitely generated module over an Artinian ring has finite length, and splitting off one indecomposable summand at a time expresses the class of a finitely generated projective module as a sum of indecomposable projective classes.

noncomputable def TauCeti.indecomposableProjectiveClassBasis {R : Type u} [Ring R] [IsArtinianRing R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hexh : IsExhaustiveIndecomposableProjectiveFamily P) : Module.Basis I ℤ (ExactK0 (finiteProjectiveModulesExactStructure R))

The indecomposable-projective basis of K₀(proj R). Its basis vector at i is the class [P i]. The hypotheses say precisely that the chosen modules are indecomposable, pairwise nonisomorphic, and exhaust all indecomposable finitely generated projective modules.

Equations

• TauCeti.indecomposableProjectiveClassBasis P hind hnoniso hexh = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.indecomposableProjectiveClassBasis_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hexh : IsExhaustiveIndecomposableProjectiveFamily P) (i : I) : (indecomposableProjectiveClassBasis P hind hnoniso hexh) i = ExactK0.of (P i)

The basis vector indexed by i is the Grothendieck class [P i].

@[simp]

theorem TauCeti.indecomposableProjectiveClassBasis_repr_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type u_1} (P : I → (finiteProjectiveModules R).FullSubcategory) (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hexh : IsExhaustiveIndecomposableProjectiveFamily P) (x : ExactK0 (finiteProjectiveModulesExactStructure R)) (i : I) : ((indecomposableProjectiveClassBasis P hind hnoniso hexh).repr x) i = (indecomposableCoordinate R ↑(P i).obj) x

The ith coefficient in the indecomposable-projective basis is the Krull-Schmidt multiplicity coordinate attached to P i.

Commutative local rings

theorem TauCeti.isExhaustiveIndecomposableProjectiveFamily_of_isLocalRing {A : Type u} [CommRing A] [IsLocalRing A] (X : (finiteProjectiveModules A).FullSubcategory) (e : ↑X.obj ≃ₗ[A] A) : IsExhaustiveIndecomposableProjectiveFamily fun (x : Unit) => X

Over a commutative local ring, one projective module isomorphic to the ring is an exhaustive family: a finitely generated projective module over such a ring is free, and an indecomposable free module is isomorphic to the ring.