The indecomposable modules over k[X]/(Xⁿ)

Let k be a field, A = k[X]/(Xⁿ) the truncated polynomial algebra, with x the class of X, and for i ≤ n let M_i = A ⧸ (x ^ i), a cyclic right A-module of dimension i. Right A-modules are left Aᵐᵒᵖ-modules, and M_i is the quotient of the regular module Aᵐᵒᵖ by the ideal generated by op (x ^ i). This file proves that M_1, …, M_n are, up to isomorphism, exactly the indecomposable finitely generated right A-modules, and that every finitely generated right A-module is a finite direct sum of them.

The modules M_i are the cyclic modules whose stable syzygies and stable morphism spaces over the self-injective algebra A are computed in TauCeti.Algebra.Category.FGModuleCat.Stable.Syzygy and TauCeti.Algebra.Category.FGModuleCat.Stable.CyclicHom; the classification says that up to finite direct sums they are all the finitely generated right A-modules.

Main results

• TauCeti.isIndecomposableModule_quotient_span_op_root_X_pow_pow: M_i is indecomposable for 0 < i ≤ n.
• TauCeti.nonempty_linearEquiv_quotient_span_op_root_X_pow_pow_iff: for i, j ≤ n, M_i and M_j are isomorphic only when i = j.
• TauCeti.exists_linearEquiv_quotient_span_op_root_X_pow_pow_of_isIndecomposableModule: every indecomposable finitely generated right A-module is isomorphic to some M_i with 0 < i ≤ n, packaged with the converse as TauCeti.isIndecomposableModule_iff_exists_linearEquiv_quotient_span_op_root_X_pow_pow.
• TauCeti.exists_linearEquiv_directSum_quotient_span_op_root_X_pow_pow: every finitely generated right A-module is isomorphic to a finite direct sum of modules M_i with 0 < i ≤ n.

Implementation notes

A right A-module M becomes a k[X]-module through the surjection k[X] → A → Aᵐᵒᵖ, killed by Xⁿ, and k[X]-submodules and Aᵐᵒᵖ-submodules of M agree (TauCeti.isIndecomposableModule_iff_isIndecomposableModule_of_algebraMap_surjective). An indecomposable M is therefore a cyclic primary k[X]-module k[X] ⧸ (pᵉ) by the structure theorem over a principal ideal domain (TauCeti.exists_linearEquiv_quotient_pow_of_isIndecomposableModule); as pᵉ divides Xⁿ, the prime p is associated to X and e ≤ n, and k[X] ⧸ (Xᵉ) is M_e with its scalars restricted. The k[X]-linear isomorphism is then Aᵐᵒᵖ-linear, by LinearEquiv.extendScalarsOfSurjective. Indecomposability of M_i holds because M_i is a quotient ring of the local ring Aᵐᵒᵖ, hence local, and a local ring is indecomposable over itself. The decomposition into the M_i is the Krull–Schmidt existence theorem for the Artinian module M, followed by the classification of its indecomposable summands.

References

The classification is the special case k[X]/(Xⁿ) of the description of the indecomposable modules over a Nakayama algebra: see I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Chapter V.

theorem TauCeti.isIndecomposableModule_quotient_span_op_root_X_pow_pow {K : Type u} [Field K] {n i : ℕ} (hi : 0 < i) (hin : i ≤ n) : IsIndecomposableModule (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})

The cyclic module M_i = A ⧸ (x ^ i) over A = K[X]/(Xⁿ) is indecomposable for 0 < i ≤ n.

theorem TauCeti.nonempty_linearEquiv_quotient_span_op_root_X_pow_pow_iff {K : Type u} [Field K] {n i j : ℕ} (hi : i ≤ n) (hj : j ≤ n) : Nonempty (((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)}) ≃ₗ[(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ] (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ j)}) ↔ i = j

The modules M_i are pairwise non-isomorphic: for i, j ≤ n, the cyclic modules A ⧸ (x ^ i) and A ⧸ (x ^ j) over A = K[X]/(Xⁿ) are isomorphic exactly when i = j, since they have dimensions i and j over K.

theorem TauCeti.exists_linearEquiv_quotient_span_op_root_X_pow_pow_of_isIndecomposableModule {K : Type u} [Field K] {n : ℕ} {M : Type v} [AddCommGroup M] [Module (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] [Module.Finite (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] (h : IsIndecomposableModule (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M) : ∃ (i : ℕ), 0 < i ∧ i ≤ n ∧ Nonempty (M ≃ₗ[(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ] (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})

Every indecomposable finitely generated right module over A = K[X]/(Xⁿ) is one of the M_i: it is isomorphic to A ⧸ (x ^ i) for some 0 < i ≤ n.

theorem TauCeti.isIndecomposableModule_iff_exists_linearEquiv_quotient_span_op_root_X_pow_pow {K : Type u} [Field K] {n : ℕ} {M : Type v} [AddCommGroup M] [Module (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] [Module.Finite (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] : IsIndecomposableModule (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M ↔ ∃ (i : ℕ), 0 < i ∧ i ≤ n ∧ Nonempty (M ≃ₗ[(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ] (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})

The indecomposable finitely generated right modules over A = K[X]/(Xⁿ) are exactly the M_i, up to isomorphism: such a module is indecomposable exactly when it is isomorphic to A ⧸ (x ^ i) for some 0 < i ≤ n.

theorem TauCeti.exists_linearEquiv_directSum_quotient_span_op_root_X_pow_pow {K : Type u} [Field K] {n : ℕ} (M : Type v) [AddCommGroup M] [Module (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] [Module.Finite (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] : ∃ (k : ℕ) (e : Fin k → ℕ), (∀ (j : Fin k), 0 < e j ∧ e j ≤ n) ∧ Nonempty (M ≃ₗ[(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ] DirectSum (Fin k) fun (j : Fin k) => (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ e j)})

Every finitely generated right module over A = K[X]/(Xⁿ) is a direct sum of the M_i: it is isomorphic to ⨁ j, A ⧸ (x ^ e j) for finitely many exponents 0 < e j ≤ n.