Indecomposability and projectivity of the inverse Auslander–Reiten translate

The inverse translate Tr D takes non-injective indecomposable modules over a finite-dimensional algebra to non-projective indecomposable modules. Here D E is specified by an equivariant scalar-dual pairing, and Tr is the A-valued right transpose of a finite minimal projective presentation. This gives an actual left A-module, with no change of its scalars to the double opposite.

The underlying right-transpose results hold over any ring: a minimal right transpose is projective exactly when its source is projective, and for a finite-length indecomposable source it is indecomposable exactly when the source is not projective. The scalar-dual specializations characterize projectivity by injectivity of E, and indecomposability by non-injectivity of an indecomposable E. Algebraic closedness is not required.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.

theorem TauCeti.FiniteProjectivePresentation.nonempty_linearEquiv_rightTranspose {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) {N' : ModuleCat Aᵐᵒᵖ} (P : FiniteProjectivePresentation N') (f : ↑N ≃ₗ[Aᵐᵒᵖ] ↑N') (hQ : IsMinimalProjectivePresentation Q.p Q.π) (hP : IsMinimalProjectivePresentation P.p P.π) : Nonempty (↑Q.rightTranspose ≃ₗ[A] ↑P.rightTranspose)

Minimal right presentations of isomorphic modules compute isomorphic left transposes.

theorem TauCeti.FiniteProjectivePresentation.subsingleton_rightTranspose_iff_projective {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) (hQ : IsMinimalProjectivePresentation Q.p Q.π) : Subsingleton ↑Q.rightTranspose ↔ Module.Projective Aᵐᵒᵖ ↑N

A minimal right transpose vanishes exactly on projective right modules.

@[simp]

theorem TauCeti.FiniteProjectivePresentation.projective_rightTranspose_iff {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) (hQ : IsMinimalProjectivePresentation Q.p Q.π) : Module.Projective A ↑Q.rightTranspose ↔ Module.Projective Aᵐᵒᵖ ↑N

A finite minimal right transpose is projective exactly when its source is projective. Neither finite length nor indecomposability of the source is required.

@[simp]

theorem TauCeti.FiniteProjectivePresentation.isIndecomposableModule_rightTranspose_iff {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) (hQ : IsMinimalProjectivePresentation Q.p Q.π) [Small.{v, u} Aᵐᵒᵖ] (hN : IsFiniteLength Aᵐᵒᵖ ↑N) (hiN : IsIndecomposableModule Aᵐᵒᵖ ↑N) : IsIndecomposableModule A ↑Q.rightTranspose ↔ ¬Module.Projective Aᵐᵒᵖ ↑N

The finite minimal right transpose of a finite-length indecomposable module is indecomposable exactly when the source is not projective.

theorem TauCeti.FiniteProjectivePresentation.projective_rightTranspose_iff_injective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {N : ModuleCat Aᵐᵒᵖ} [Module k ↑N] [IsScalarTower k Aᵐᵒᵖ ↑N] [FiniteDimensional k ↑N] {E : Type z} [AddCommGroup E] [Module A E] [Module k E] [Small.{z, v} A] (Q : FiniteProjectivePresentation N) (hQ : IsMinimalProjectivePresentation Q.p Q.π) (e : E ≃ₗ[k] Module.Dual k ↑N) (he : ∀ (a : A) (y : E) (x : ↑N), (e (a • y)) x = (e y) (MulOpposite.op a • x)) : Module.Projective A ↑Q.rightTranspose ↔ Module.Injective A E

The inverse translate Tr D E, formed from a finite minimal presentation of the right scalar dual of E, is projective exactly when E is injective. The equivariant pairing specifies the scalar dual without a competing global dual action.

theorem TauCeti.FiniteProjectivePresentation.isIndecomposableModule_rightTranspose_iff_not_injective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {N : ModuleCat Aᵐᵒᵖ} [Module k ↑N] [IsScalarTower k Aᵐᵒᵖ ↑N] [FiniteDimensional k ↑N] {E : Type z} [AddCommGroup E] [Module A E] [Module k E] [Small.{z, v} A] (Q : FiniteProjectivePresentation N) (hQ : IsMinimalProjectivePresentation Q.p Q.π) [Small.{w, v} Aᵐᵒᵖ] (e : E ≃ₗ[k] Module.Dual k ↑N) (he : ∀ (a : A) (y : E) (x : ↑N), (e (a • y)) x = (e y) (MulOpposite.op a • x)) (hiE : IsIndecomposableModule A E) : IsIndecomposableModule A ↑Q.rightTranspose ↔ ¬Module.Injective A E

For an indecomposable E, its inverse translate Tr D E is indecomposable exactly when E is not injective. Together with projective_rightTranspose_iff_injective, this places the inverse translate of a non-injective indecomposable among the non-projective indecomposables.