Ext-Euler characteristics of projective covers against simple modules

Let P ⟶ S be a projective cover of a simple module over an algebra A over a field k. Since P is projective, its Ext-Euler characteristic against a simple module T is χ(P, T) = dim_k Hom_A(P, T). This is the dimension of the division algebra End_A(S) when T ≅ S, and 0 otherwise.

Main results

• TauCeti.IsProjectiveCover.extEuler_eq_finrank_end: χ(P, T) = dim_k End_A(S) if T ≅ S.
• TauCeti.IsProjectiveCover.extEuler_eq_zero: χ(P, T) = 0 if T is not isomorphic to S.

theorem TauCeti.IsProjectiveCover.extEuler_eq_finrank_end {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] {P T : ModuleCat A} {S : Type u_2} [AddCommGroup S] [Module A S] {f : ↑P →ₗ[A] S} [Module k S] [IsScalarTower k A S] (hf : IsProjectiveCover f) [IsSimpleModule A ↑T] (e : ↑T ≃ₗ[A] S) (h : IsEulerAdmissible k P T) : extEuler k h = ↑(Module.finrank k (Module.End A S))

The diagonal Ext-Euler value. For a projective cover P ⟶ S of a simple module and a simple module T ≅ S, χ(P, T) is the dimension of the division algebra End_A(S).

theorem TauCeti.IsProjectiveCover.extEuler_eq_zero {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] {P T : ModuleCat A} {S : Type u_2} [AddCommGroup S] [Module A S] {f : ↑P →ₗ[A] S} [IsSimpleModule A S] (hf : IsProjectiveCover f) [IsSimpleModule A ↑T] (he : IsEmpty (↑T ≃ₗ[A] S)) (h : IsEulerAdmissible k P T) : extEuler k h = 0

The off-diagonal Ext-Euler value. For a projective cover P ⟶ S of a simple module and a simple module T not isomorphic to S, χ(P, T) = 0.