Documentation

TauCeti.Algebra.Module.Dual.Indecomposable

Linear duality preserves indecomposability #

A reflexive right module is indecomposable exactly when its scalar dual, with the left action by precomposition, is indecomposable. This applies in particular to finite-dimensional modules over an arbitrary algebra over a field. The result supplies the duality step in passing from indecomposable transposes to indecomposable Auslander–Reiten translates.

The dual action is specified by an equivariant linear identification. No finiteness of the algebra, algebraic closedness, or choice of a global module structure on scalar duals is needed.

References #

theorem LinearEquiv.isIndecomposableModule_iff_of_dual {k : Type u} [CommSemiring k] {A : Type v} [Ring A] [Algebra k A] {N : Type w} [AddCommGroup N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] [Module.IsReflexive k N] {Q : Type z} [AddCommGroup Q] [Module A Q] [Module k Q] (e : Q ≃ₗ[k] Module.Dual k N) (he : ∀ (a : A) (q : Q) (x : N), (e (a • q)) x = (e q) (MulOpposite.op a • x)) :

A reflexive right module is indecomposable exactly when its left scalar dual is. Finite-dimensional modules over a field satisfy the reflexivity hypothesis automatically.