The Cartan matrix of the dual numbers

Let k be a field, let A = k[ε] be the dual numbers k[ε]/(ε²), and let S = A/(ε) be its residue field, viewed as an A-module. The ring A is local and Artinian, its only indecomposable finitely generated projective module is A itself, and its only simple module is S. The short exact sequence

0 ⟶ S --ε--> A ⟶ S ⟶ 0

shows that A has two composition factors, both isomorphic to S. Hence the Cartan map K₀(proj A) ⟶ G₀(mod A) sends [A] to 2 • [S], and the Cartan matrix of A is the one-by-one matrix 2. Its determinant is 2, so it is not invertible over ℤ.

This is the example showing that unimodularity of the Cartan matrix needs finite projective resolutions: every class in the image of the Cartan map has even S-coordinate, while [S] has coordinate one. Since the Cartan map sends the alternating class of a finite projective resolution of a module to the class of that module, S admits no finite resolution by finitely generated projective modules.

Main results

• TauCeti.jordanHolderMultiplicity_dualNumber_dualNumberResidue: [A : S] = 2.
• TauCeti.cartanMap_dualNumberFreeProj: the Cartan map sends [A] to 2 • [S].
• TauCeti.cartanMatrix_dualNumber: the Cartan matrix of A is 2, with TauCeti.det_cartanMatrix_dualNumber and TauCeti.not_isUnit_cartanMatrix_dualNumber.
• TauCeti.cartanMap_dualNumber_ne_dualNumberResidueFG: [S] is not in the image of the Cartan map, so TauCeti.not_surjective_cartanMap_dualNumber: the Cartan map is not surjective.
• TauCeti.not_admitsFiniteResolution_dualNumberResidue: S has no finite resolution by finitely generated projective modules.

References

• Ibrahim Assem, Daniel Simson and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3.

The composition factors of k[ε]

@[simp]

theorem TauCeti.jordanHolderMultiplicity_dualNumber_dualNumberResidue (k : Type u) [Field k] : jordanHolderMultiplicity (DualNumber k) (DualNumber k) ↑(dualNumberResidue k) = 2

k[ε] has two composition factors isomorphic to its residue field: [k[ε] : k[ε]/(ε)] = 2, read off the short exact sequence 0 ⟶ S --ε--> A ⟶ S ⟶ 0.

The Cartan map and matrix

@[reducible, inline]

noncomputable abbrev TauCeti.dualNumberFreeProj (k : Type u) [Field k] : (finiteProjectiveModules (DualNumber k)).FullSubcategory

The rank-one free module over k[ε], as an object of the category of finitely generated projective modules.

@[reducible, inline]

noncomputable abbrev TauCeti.dualNumberResidueFG (k : Type u) [Field k] : FGModuleCat (DualNumber k)

The residue module k[ε]/(ε), as an object of the category of finitely generated modules.

theorem TauCeti.isExhaustiveIndecomposableProjectiveFamily_dualNumberFreeProj (k : Type u) [Field k] : IsExhaustiveIndecomposableProjectiveFamily fun (x : Unit) => dualNumberFreeProj k

k[ε] is, up to isomorphism, the only indecomposable finitely generated projective k[ε]-module.

theorem TauCeti.isExhaustiveSimpleFamily_dualNumberResidueFG (k : Type u) [Field k] : IsExhaustiveSimpleFamily fun (x : Unit) => dualNumberResidueFG k

k[ε]/(ε) is, up to isomorphism, the only simple finitely generated k[ε]-module.

theorem TauCeti.cartanMap_dualNumberFreeProj (k : Type u) [Field k] : (cartanMap (DualNumber k)) (ExactK0.of (dualNumberFreeProj k)) = 2 • ExactK0.of (dualNumberResidueFG k)

The Cartan map of k[ε] sends the class of the regular module to twice the class of the residue field.

@[simp]

theorem TauCeti.cartanMatrix_dualNumber (k : Type u) [Field k] : cartanMatrix (fun (x : Unit) => dualNumberFreeProj k) (fun (x : Unit) => dualNumberResidueFG k) ⋯ ⋯ ⋯ ⋯ ⋯ = 2

The Cartan matrix of k[ε] is the one-by-one matrix 2, in the bases given by the regular module and the residue field.

theorem TauCeti.det_cartanMatrix_dualNumber (k : Type u) [Field k] : (cartanMatrix (fun (x : Unit) => dualNumberFreeProj k) (fun (x : Unit) => dualNumberResidueFG k) ⋯ ⋯ ⋯ ⋯ ⋯).det = 2

The Cartan matrix of k[ε] has determinant 2.

theorem TauCeti.not_isUnit_cartanMatrix_dualNumber (k : Type u) [Field k] : ¬IsUnit (cartanMatrix (fun (x : Unit) => dualNumberFreeProj k) (fun (x : Unit) => dualNumberResidueFG k) ⋯ ⋯ ⋯ ⋯ ⋯)

The Cartan matrix of k[ε] is not unimodular: it is not invertible over ℤ.

The residue field has no finite projective resolution

theorem TauCeti.two_dvd_jordanHolderCoordinate_cartanMap_dualNumber (k : Type u) [Field k] (x : ExactK0 (finiteProjectiveModulesExactStructure (DualNumber k))) : 2 ∣ (jordanHolderCoordinate (DualNumber k) ↑(dualNumberResidue k)) ((cartanMap (DualNumber k)) x)

Every class in the image of the Cartan map of k[ε] has even S-coordinate, because K₀(proj k[ε]) is generated by [k[ε]], which is sent to 2 • [S].

theorem TauCeti.cartanMap_dualNumber_ne_dualNumberResidueFG (k : Type u) [Field k] (x : ExactK0 (finiteProjectiveModulesExactStructure (DualNumber k))) : (cartanMap (DualNumber k)) x ≠ ExactK0.of (dualNumberResidueFG k)

The class of the residue field is not in the image of the Cartan map of k[ε]: its S-coordinate is one, which is odd.

theorem TauCeti.not_surjective_cartanMap_dualNumber (k : Type u) [Field k] : ¬Function.Surjective ⇑(cartanMap (DualNumber k))

The Cartan map of k[ε] is not surjective.

theorem TauCeti.not_admitsFiniteResolution_dualNumberResidue (k : Type u) [Field k] : ¬(ExactStructure.abelian (ModuleCat (DualNumber k))).admitsFiniteResolution (finiteProjectiveModules (DualNumber k)) (dualNumberResidue k)

The residue field of k[ε] has no finite projective resolution: the Cartan map would send the alternating class of such a resolution to [S].