Simple classes in the Grothendieck group of finite-length modules

Let R be an Artinian ring. Every finitely generated left R-module has finite length, and its Jordan--Hölder multiplicities are additive in short exact sequences. Consequently, multiplicity of a fixed simple module descends to an integer-valued coordinate on the exact Grothendieck group G₀(mod R).

These coordinates show that the classes of any pairwise nonisomorphic family of simple modules are linearly independent. If the family contains a representative of every simple finitely generated module, finite-length induction also shows that the classes span, giving a canonical \mathbb Z-basis of G₀(mod R) indexed by that family. The basis is the simple-module side of the projective/simple coordinates used to express the Cartan map as a matrix.

Main definitions

• TauCeti.jordanHolderCoordinate: the homomorphism from G₀(mod R) which reads the Jordan--Hölder multiplicity of a fixed simple module.
• TauCeti.simpleClassBasis: the basis of G₀(mod R) given by an exhaustive family of pairwise nonisomorphic simple modules.

Main results

• TauCeti.jordanHolderCoordinate_of: the coordinate of an object class is its Jordan--Hölder multiplicity.
• TauCeti.linearIndependent_exactK0OfFamily: pairwise nonisomorphic simple classes are linearly independent.
• TauCeti.span_range_exactK0OfFamily_eq_top: an exhaustive family of simple classes spans.
• TauCeti.free_exactK0_of_isExhaustiveSimpleFamily, TauCeti.finite_exactK0_of_isExhaustiveSimpleFamily and TauCeti.finrank_exactK0_eq_card_of_isExhaustiveSimpleFamily: G₀(mod R) is a free ℤ-module, finite of rank the number of simple classes.
• TauCeti.IsSimpleModule.nonempty_linearEquiv_quot_maximalIdeal: a simple module over a commutative local ring is isomorphic to its residue field.
• TauCeti.isExhaustiveSimpleFamily_of_isLocalRing: over a commutative local ring a single simple module is an exhaustive family.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6.
• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3.

Jordan--Hölder coordinates

noncomputable def TauCeti.jordanHolderCoordinate (R : Type u) [Ring R] [IsArtinianRing R] (S : Type w) [AddCommGroup S] [Module R S] : ExactK0 (finiteModulesExactStructure R) →+ ℤ

The Jordan--Hölder coordinate of a fixed module S on G₀(mod R). On the class of M it is the multiplicity [M : S]. It is useful as a simple coordinate when S is simple, but the construction is valid for arbitrary S (and is then identically zero if S is not simple).

Equations

• TauCeti.jordanHolderCoordinate R S = TauCeti.ExactK0.lift (TauCeti.jordanHolderInvariant✝ R S)

@[simp]

theorem TauCeti.jordanHolderCoordinate_of (R : Type u) [Ring R] [IsArtinianRing R] (S : Type w) [AddCommGroup S] [Module R S] (M : FGModuleCat R) : (jordanHolderCoordinate R S) (ExactK0.of M) = ↑(jordanHolderMultiplicity R (↑M) S)

The Jordan--Hölder coordinate of an object class is its multiplicity in that module.

theorem TauCeti.jordanHolderCoordinate_congr (R : Type u) [Ring R] [IsArtinianRing R] (S : Type w) [AddCommGroup S] [Module R S] {T : Type w'} [AddCommGroup T] [Module R T] (e : S ≃ₗ[R] T) : jordanHolderCoordinate R S = jordanHolderCoordinate R T

Isomorphic modules define the same Jordan--Hölder coordinate.

@[simp]

theorem TauCeti.jordanHolderCoordinate_self (R : Type u) [Ring R] [IsArtinianRing R] (S : Type u) [AddCommGroup S] [Module R S] [IsSimpleModule R S] [Module.Finite R S] : (jordanHolderCoordinate R S) (ExactK0.of ↧S) = 1

A simple module has coordinate one on its own class.

@[simp]

theorem TauCeti.jordanHolderCoordinate_eq_zero_of_isEmpty_linearEquiv (R : Type u) [Ring R] [IsArtinianRing R] (S : Type w) [AddCommGroup S] [Module R S] {T : Type u} [AddCommGroup T] [Module R T] [Module.Finite R T] [IsSimpleModule R T] (h : IsEmpty (T ≃ₗ[R] S)) : (jordanHolderCoordinate R S) (ExactK0.of ↧T) = 0

Two nonisomorphic simple modules have zero mutual Jordan--Hölder coordinate.

Linear independence and spanning

noncomputable def TauCeti.exactK0OfFamily {R : Type u} [Ring R] {I : Type v} (S : I → FGModuleCat R) (i : I) : ExactK0 (finiteModulesExactStructure R)

The classes in G₀(mod R) of an indexed family of finitely generated modules.

Equations

• TauCeti.exactK0OfFamily S i = TauCeti.ExactK0.of (S i)

theorem TauCeti.exactK0OfFamily_apply {R : Type u} [Ring R] {I : Type v} (S : I → FGModuleCat R) (i : I) : exactK0OfFamily S i = ExactK0.of (S i)

The characteristic equation of exactK0OfFamily: the member at i is the class [S i] in the exact Grothendieck group. Intended for explicit rewriting; the specialized Jordan--Hölder coordinate lemmas below are the simp normal forms.

@[simp]

theorem TauCeti.jordanHolderCoordinate_exactK0OfFamily_self {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (i : I) : (jordanHolderCoordinate R ↑(S i)) (exactK0OfFamily S i) = 1

A member of a simple family has Jordan--Hölder coordinate one on its own class.

@[simp]

theorem TauCeti.jordanHolderCoordinate_exactK0OfFamily_eq_zero {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] {i j : I} (hij : IsEmpty (↑(S j) ≃ₗ[R] ↑(S i))) : (jordanHolderCoordinate R ↑(S i)) (exactK0OfFamily S j) = 0

A Jordan--Hölder coordinate is zero on a nonisomorphic member of a simple family.

@[simp]

theorem TauCeti.jordanHolderCoordinate_exactK0OfFamily {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] [DecidableEq I] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (i j : I) : (jordanHolderCoordinate R ↑(S i)) (exactK0OfFamily S j) = if j = i then 1 else 0

On a pairwise nonisomorphic simple family, the Jordan--Hölder coordinates form the Kronecker-delta matrix.

theorem TauCeti.linearIndependent_exactK0OfFamily {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) : LinearIndependent ℤ (exactK0OfFamily S)

Pairwise nonisomorphic simple classes are linearly independent in G₀(mod R).

def TauCeti.IsExhaustiveSimpleFamily {R : Type u} [Ring R] {I : Type v} (S : I → FGModuleCat R) : Prop

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

Equations

• TauCeti.IsExhaustiveSimpleFamily S = ∀ (M : FGModuleCat R), IsSimpleModule R ↑M → ∃ (i : I), Nonempty (↑M ≃ₗ[R] ↑(S i))

theorem TauCeti.isExhaustiveSimpleFamily_iff {R : Type u} [Ring R] {I : Type v} (S : I → FGModuleCat R) : IsExhaustiveSimpleFamily S ↔ ∀ (M : FGModuleCat R), IsSimpleModule R ↑M → ∃ (i : I), Nonempty (↑M ≃ₗ[R] ↑(S i))

Characterization of IsExhaustiveSimpleFamily: the family is exhaustive exactly when every simple finitely generated 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_exactK0OfFamily_eq_top {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) (hexhaustive : IsExhaustiveSimpleFamily S) : Submodule.span ℤ (Set.range (exactK0OfFamily S)) = ⊤

An exhaustive family of simple classes spans G₀(mod R). Every finitely generated module over an Artinian ring has finite length, and induction on a simple-quotient filtration expresses its class as a sum of simple classes.

noncomputable def TauCeti.simpleClassBasis {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hexhaustive : IsExhaustiveSimpleFamily S) : Module.Basis I ℤ (ExactK0 (finiteModulesExactStructure R))

The simple-class basis of G₀(mod R). Its basis vector at i is the class [S i]. The hypotheses say precisely that the chosen modules are simple, pairwise nonisomorphic, and exhaust all simple finitely generated modules.

Equations

• TauCeti.simpleClassBasis S hnoniso hexhaustive = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.simpleClassBasis_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hexhaustive : IsExhaustiveSimpleFamily S) (i : I) : (simpleClassBasis S hnoniso hexhaustive) i = ExactK0.of (S i)

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

@[simp]

theorem TauCeti.simpleClassBasis_repr_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hexhaustive : IsExhaustiveSimpleFamily S) (x : ExactK0 (finiteModulesExactStructure R)) (i : I) : ((simpleClassBasis S hnoniso hexhaustive).repr x) i = (jordanHolderCoordinate R ↑(S i)) x

The ith coefficient in the simple-class basis is the Jordan--Hölder multiplicity coordinate attached to S i.

theorem TauCeti.free_exactK0_of_isExhaustiveSimpleFamily {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hexhaustive : IsExhaustiveSimpleFamily S) : Module.Free ℤ (ExactK0 (finiteModulesExactStructure R))

G₀(mod R) is a free ℤ-module, on the classes of an exhaustive family of pairwise nonisomorphic simple modules.

theorem TauCeti.finite_exactK0_of_isExhaustiveSimpleFamily {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) [Finite I] (hexhaustive : IsExhaustiveSimpleFamily S) : Module.Finite ℤ (ExactK0 (finiteModulesExactStructure R))

G₀(mod R) is a finitely generated ℤ-module when there are finitely many simple classes.

theorem TauCeti.finrank_exactK0_eq_card_of_isExhaustiveSimpleFamily {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) [Fintype I] (hexhaustive : IsExhaustiveSimpleFamily S) : Module.finrank ℤ (ExactK0 (finiteModulesExactStructure R)) = Fintype.card I

The rank of G₀(mod R) is the number of isomorphism classes of simple modules.

Commutative local rings

theorem TauCeti.IsSimpleModule.nonempty_linearEquiv_quot_maximalIdeal {A : Type u} [CommRing A] [IsLocalRing A] (M : Type u) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : Nonempty (M ≃ₗ[A] A ⧸ IsLocalRing.maximalIdeal A)

Every simple module over a commutative local ring is isomorphic to its residue field.

theorem TauCeti.isExhaustiveSimpleFamily_of_isLocalRing {A : Type u} [CommRing A] [IsLocalRing A] (T : FGModuleCat A) [IsSimpleModule A ↑T] : IsExhaustiveSimpleFamily fun (x : Unit) => T

Over a commutative local ring any one simple module is an exhaustive family: every simple module is isomorphic to the quotient by the maximal ideal.