Unimodularity of the Cartan matrix

Let R be an Artinian ring with finite exhaustive families of indecomposable projectives and simple modules, indexed so that their classes give the projective and simple bases. If every finitely generated R-module admits a finite resolution by finitely generated projectives, the Cartan map is an isomorphism. Consequently its matrix in these bases is invertible over ℤ, and its determinant is 1 or -1.

The inverse matrix records the projective-basis coordinates of the alternating projective resolution class of each simple-basis vector. Thus the finite-resolution hypothesis appears exactly where the inverse is constructed; no unimodularity statement is made for arbitrary Artinian rings.

Main definitions

• TauCeti.inverseCartanMatrix: the matrix of the inverse Cartan map in the simple and projective bases.

Main results

• TauCeti.cartanMatrix_mul_inverseCartanMatrix and TauCeti.inverseCartanMatrix_mul_cartanMatrix: the two inverse identities.
• TauCeti.isUnit_cartanMatrix: the Cartan matrix is invertible over ℤ.
• TauCeti.cartanMatrix_det_eq_one_or_neg_one: its determinant is 1 or -1.

References

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

noncomputable def TauCeti.inverseCartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : Matrix I I ℤ

The matrix of the inverse Cartan map in the simple-class basis on the source and the indecomposable-projective basis on the target. Its columns are the projective coordinates of the alternating finite-resolution classes of the selected simples.

@[simp]

theorem TauCeti.inverseCartanMatrix_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) (i j : I) : inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h i j = ((indecomposableProjectiveClassBasis P hind hPnoniso hPexhaustive).repr ((cartanInverse R h) ((simpleClassBasis S hSnoniso hSexhaustive) j))) i

The (i, j) entry of the inverse Cartan matrix is the ith projective-basis coordinate of the inverse Cartan map applied to the jth simple-basis vector.

@[simp]

theorem TauCeti.cartanMatrix_mul_inverseCartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive * inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h = 1

The inverse Cartan matrix is a right inverse of the Cartan matrix.

@[simp]

theorem TauCeti.inverseCartanMatrix_mul_cartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h * cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive = 1

The inverse Cartan matrix is a left inverse of the Cartan matrix.

theorem TauCeti.isUnit_cartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : IsUnit (cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive)

Under the finite-projective-resolution hypothesis, the Cartan matrix is invertible over ℤ.

theorem TauCeti.isUnit_det_cartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : IsUnit (cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).det

Under the finite-projective-resolution hypothesis, the determinant of the Cartan matrix is a unit in ℤ.

theorem TauCeti.cartanMatrix_det_eq_one_or_neg_one {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : (cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).det = 1 ∨ (cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).det = -1

Cartan-matrix unimodularity. If every finitely generated module admits a finite resolution by finitely generated projectives, the Cartan determinant is 1 or -1. No positivity of its sign is asserted.