Documentation

TauCeti.RepresentationTheory.GrothendieckGroup.ExtEulerMatrix

The Ext-Euler matrix of a finite-dimensional algebra #

Let A be an algebra over a field k, with finite exhaustive families of pairwise nonisomorphic simple modules S i and indecomposable projectives P i, where P i ⟶ S i is a projective cover. This file computes the Ext-Euler characteristic

χ(M, N) = ∑ n, (-1)ⁿ dim_k Extⁿ_A(M, N)

of TauCeti.extEuler on these two families.

Against simples, the projective covers are dual to the simples up to the division algebras D i = End_A(S i): χ(P i, S j) = dim_k Hom_A(P i, S j) is dim_k D i when i = j and 0 otherwise. Over a general field the diagonal entry is dim_k D i; it is 1 when S i is absolutely simple, that is, when D i is one-dimensional.

If every pair of finitely generated modules is Euler-admissible, the matrix E i j = χ(S i, S j) is therefore constrained by the Cartan matrix C i j = [P j : S i]: column i of C expresses [P i] in the simple basis of G₀(mod A). Over a general field this gives Cᵀ * E = diagonal (fun i ↦ dim_k D i); when every simple is absolutely simple it gives Cᵀ * E = 1. If A is finite-dimensional and every finitely generated module has a finite resolution by finitely generated projectives, all these pairs are Euler-admissible and C is invertible, so E = (C⁻¹)ᵀ * diagonal (fun i ↦ dim_k D i): the entry E i j is the (j, i) entry of C⁻¹ times dim_k D j. If moreover every simple is absolutely simple, then E = (C⁻¹)ᵀ. Rows of E are indexed by the first argument of the Euler form, which is not symmetric in general, so the transpose is part of the statement.

Main results #

References #

The Ext-Euler matrix of the simple modules #

theorem TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_diagonal {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (hadm : IsEulerAdmissibleOn k (ModuleCat.isFG A) (ModuleCat.isFG A)) :
(cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).transpose * extEulerMatrix (ModuleCat.isFG A) (ModuleCat.isFG A) ⋯ ⋯ hadm ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) = Matrix.diagonal fun (i : I) => ↑(Module.finrank k (Module.End A ↑(S i).obj))

The general-field Cartan/Ext-Euler identity. Let P i ⟶ S i be projective covers of simple modules. If every pair of finitely generated modules is Euler-admissible, then Cᵀ * E = diagonal (fun i ↦ dim_k End_A(S i)), where C i j = [P j : S i] is the Cartan matrix and E is the Ext-Euler matrix in the simple-class basis.

theorem TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_one {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (hend : ∀ (i : I), Module.finrank k (Module.End A ↑(S i).obj) = 1) (hadm : IsEulerAdmissibleOn k (ModuleCat.isFG A) (ModuleCat.isFG A)) :
(cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).transpose * extEulerMatrix (ModuleCat.isFG A) (ModuleCat.isFG A) ⋯ ⋯ hadm ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) = 1

The Ext-Euler matrix is a right inverse of the transposed Cartan matrix. Let P i ⟶ S i be projective covers of absolutely simple modules. If every pair of finitely generated modules is Euler-admissible, then Cᵀ * E = 1, where C i j = [P j : S i] is the Cartan matrix and E is the Ext-Euler matrix in the simple-class basis.

theorem TauCeti.extEulerMatrix_eq_inverseCartanMatrix_transpose_mul_diagonal {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [FiniteDimensional k A] {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (h : ModuleCat.isFG A ≤ (ExactStructure.abelian (ModuleCat A)).admitsFiniteResolution (finiteProjectiveModules A)) :
extEulerMatrix (ModuleCat.isFG A) (ModuleCat.isFG A) ⋯ ⋯ ⋯ ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) = (inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h).transpose * Matrix.diagonal fun (i : I) => ↑(Module.finrank k (Module.End A ↑(S i).obj))

The Ext-Euler matrix via the inverse Cartan matrix over a general field. Let P i ⟶ S i be projective covers of simple modules over a finite-dimensional algebra. If every finitely generated module has a finite resolution by finitely generated projectives, then E = (C⁻¹)ᵀ * diagonal (fun i ↦ dim_k End_A(S i)), where C i j = [P j : S i] is the Cartan matrix and E is the Ext-Euler matrix in the simple-class basis.

theorem TauCeti.extEulerMatrix_eq_inverseCartanMatrix_transpose {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [FiniteDimensional k A] {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (hend : ∀ (i : I), Module.finrank k (Module.End A ↑(S i).obj) = 1) (h : ModuleCat.isFG A ≤ (ExactStructure.abelian (ModuleCat A)).admitsFiniteResolution (finiteProjectiveModules A)) :
extEulerMatrix (ModuleCat.isFG A) (ModuleCat.isFG A) ⋯ ⋯ ⋯ ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) ((simpleClassBasis S hSnoniso hSexhaustive).map (finiteModulesExactK0Equiv A).toIntLinearEquiv) = (inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h).transpose

The Ext-Euler matrix is the transposed inverse Cartan matrix. Let P i ⟶ S i be projective covers of absolutely simple modules over a finite-dimensional algebra. If every finitely generated module has a finite resolution by finitely generated projectives, then E = (C⁻¹)ᵀ, where C i j = [P j : S i] is the Cartan matrix and E is the Ext-Euler matrix in the simple-class basis.

theorem TauCeti.extEuler_eq_inverseCartanMatrix_mul_finrank {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [FiniteDimensional k A] {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (h : ModuleCat.isFG A ≤ (ExactStructure.abelian (ModuleCat A)).admitsFiniteResolution (finiteProjectiveModules A)) (i j : I) (hadm : IsEulerAdmissible k (S i).obj (S j).obj) :
extEuler k hadm = inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h j i * ↑(Module.finrank k (Module.End A ↑(S j).obj))

The Ext-Euler characteristic of simples via the inverse Cartan matrix over a general field. Let P i ⟶ S i be projective covers of simple modules over a finite-dimensional algebra. If every finitely generated module has a finite resolution by finitely generated projectives, then χ(S i, S j) is the (j, i) entry of the inverse of the Cartan matrix C i j = [P j : S i] times dim_k End_A(S j).

theorem TauCeti.extEuler_eq_inverseCartanMatrix {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I] (P : I → (finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A) [hS : ∀ (i : I), IsSimpleModule A ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule A ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [FiniteDimensional k A] {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj} (hf : ∀ (i : I), IsProjectiveCover (f i)) (hend : ∀ (i : I), Module.finrank k (Module.End A ↑(S i).obj) = 1) (h : ModuleCat.isFG A ≤ (ExactStructure.abelian (ModuleCat A)).admitsFiniteResolution (finiteProjectiveModules A)) (i j : I) (hadm : IsEulerAdmissible k (S i).obj (S j).obj) :
extEuler k hadm = inverseCartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive h j i

The Ext-Euler characteristic of simples is the transposed inverse Cartan matrix. Let P i ⟶ S i be projective covers of absolutely simple modules over a finite-dimensional algebra. If every finitely generated module has a finite resolution by finitely generated projectives, then χ(S i, S j) is the (j, i) entry of the inverse of the Cartan matrix C i j = [P j : S i].