Syzygies of cyclic modules in the stable module category

Let A be a ring and let a, b : A be such that the right annihilator of a is bA, that is, a * c = 0 exactly when b ∣ c. Then left multiplication by a and the quotient map form a short exact sequence of right A-modules

0 ⟶ A ⧸ bA ⟶ A ⟶ A ⧸ aA ⟶ 0,

whose middle term is free. It is therefore a projective presentation of A ⧸ aA, and the syzygy (loop) functor Ω of the stable module category sends A ⧸ aA to A ⧸ bA. If moreover the right annihilator of b is aA, then Ω² (A ⧸ aA) ≅ A ⧸ aA: the module is periodic of period at most two in the stable module category.

The basic example is the truncated polynomial ring A = R[X]/(X ^ n) over a commutative Noetherian ring R, with x the class of X. For i ≤ n the annihilator of x ^ i is generated by x ^ (n - i) (AdjoinRoot.root_X_pow_pow_mul_eq_zero_iff), so the modules M_i = A ⧸ (x ^ i) satisfy Ω M_i ≅ M_(n - i) and Ω² M_i ≅ M_i in stmod-A. The module M_n = A is projective and hence zero there. Over a field k, the algebra k[X]/(X ^ n) is a symmetric Frobenius algebra (AdjoinRoot.isSymmetricFrobeniusFunctional_lastCoeff_X_pow), hence self-injective, so its finite-dimensional modules form a Frobenius exact category (FGModuleCat.abelian_isFrobenius) on whose stable category Ω is quasi-inverse to the suspension (TauCeti.ExactStructure.IsFrobenius.stableSuspensionEquivalence).

Right A-modules are left Aᵐᵒᵖ-modules. The cyclic right module A ⧸ aA is represented as the quotient of the regular module Aᵐᵒᵖ by the left ideal generated by op a, which is op (aA) (TauCeti.FGModuleCat.cyclicModule).

Main definitions

• TauCeti.FGModuleCat.cyclicMulLeft: left multiplication by a, as a map A ⧸ bA ⟶ A.
• TauCeti.FGModuleCat.cyclicShortComplex: the short complex A ⧸ bA ⟶ A ⟶ A ⧸ aA.
• TauCeti.FGModuleCat.cyclicPresentation: the resulting projective presentation of A ⧸ aA.
• TauCeti.FGModuleCat.stableModuleLoop: the loop functor Ω of the stable module category.
• TauCeti.FGModuleCat.stableModuleLoopCyclicModuleIso: Ω (A ⧸ aA) ≅ A ⧸ bA.
• TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleIso: Ω² (A ⧸ aA) ≅ A ⧸ aA.
• TauCeti.FGModuleCat.stableModuleLoopCyclicModuleRootPowIso, TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleRootPowIso: over R[X]/(X ^ n), Ω M_i ≅ M_(n - i) and Ω² M_i ≅ M_i.

Main results

• TauCeti.FGModuleCat.cyclicShortComplex_shortExact: the short complex is short exact.
• TauCeti.FGModuleCat.isZero_stableModuleFunctor_obj_cyclicModule_zero: the module A ⧸ 0A, the free module of rank one, is zero in the stable module category.
• TauCeti.FGModuleCat.isZero_stableModuleFunctor_obj_cyclicModule_root_pow_self: the module M_n = R[X]/(X ^ n) is zero in the stable module category.

References

• David Eisenbud, Homological algebra on a complete intersection, with an application to group representations, Trans. Amer. Math. Soc. 260 (1980), 35–64, Section 5: the periodic resolution ⋯ ⟶ A --x^(n-i)--> A --x^i--> A ⟶ A/(x^i) ⟶ 0.
• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2: the loop functor of a stable category.

noncomputable def TauCeti.FGModuleCat.cyclicMulLeft {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : Aᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op b} →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ

For a * b = 0, left multiplication by a, as a map of right A-modules A ⧸ bA ⟶ A. On Aᵐᵒᵖ it is right multiplication by op a, which kills op b.

Equations

• TauCeti.FGModuleCat.cyclicMulLeft a b hab = Submodule.liftQ (Ideal.span {MulOpposite.op b}) (LinearMap.toSpanSingleton Aᵐᵒᵖ Aᵐᵒᵖ (MulOpposite.op a)) ⋯

@[simp]

theorem TauCeti.FGModuleCat.cyclicMulLeft_mk {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) (c : Aᵐᵒᵖ) : (cyclicMulLeft a b hab) (Submodule.Quotient.mk c) = c * MulOpposite.op a

Left multiplication by a sends the class of c to c * op a = op (a * unop c).

theorem TauCeti.FGModuleCat.exact_cyclicMulLeft_mkQ {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : Function.Exact ⇑(cyclicMulLeft a b hab) ⇑(Submodule.mkQ (Ideal.span {MulOpposite.op a}))

The image of left multiplication by a is aA, the kernel of the quotient map onto A ⧸ aA.

theorem TauCeti.FGModuleCat.cyclicMulLeft_injective {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : Function.Injective ⇑(cyclicMulLeft a b ⋯)

If the right annihilator of a is bA, then left multiplication by a is injective on A ⧸ bA.

noncomputable def TauCeti.FGModuleCat.cyclicShortComplex {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : CategoryTheory.ShortComplex (FGModuleCat Aᵐᵒᵖ)

For a * b = 0, the short complex of right A-modules A ⧸ bA ⟶ A ⟶ A ⧸ aA, whose maps are left multiplication by a and the quotient map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FGModuleCat.cyclicShortComplex_X₃ {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : (cyclicShortComplex a b hab).X₃ = cyclicModule a

@[simp]

theorem TauCeti.FGModuleCat.cyclicShortComplex_X₂ {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : (cyclicShortComplex a b hab).X₂ = ↧Aᵐᵒᵖ

@[simp]

theorem TauCeti.FGModuleCat.cyclicShortComplex_g {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : (cyclicShortComplex a b hab).g = FGModuleCat.ofHom (Submodule.mkQ (Ideal.span {MulOpposite.op a}))

@[simp]

theorem TauCeti.FGModuleCat.cyclicShortComplex_X₁ {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : (cyclicShortComplex a b hab).X₁ = cyclicModule b

@[simp]

theorem TauCeti.FGModuleCat.cyclicShortComplex_f {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) : (cyclicShortComplex a b hab).f = FGModuleCat.ofHom (cyclicMulLeft a b hab)

theorem TauCeti.FGModuleCat.cyclicShortComplex_shortExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (cyclicShortComplex a b ⋯).ShortExact

If the right annihilator of a is bA, then 0 ⟶ A ⧸ bA ⟶ A ⟶ A ⧸ aA ⟶ 0 is short exact.

noncomputable def TauCeti.FGModuleCat.cyclicPresentation {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (ExactStructure.abelian (FGModuleCat Aᵐᵒᵖ)).ProjectivePresentation (cyclicModule a)

If the right annihilator of a is bA, then A ⧸ bA ⟶ A ⟶ A ⧸ aA is a projective presentation of A ⧸ aA: its middle term is the free module of rank one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FGModuleCat.cyclicPresentation_K {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (cyclicPresentation hab).K = cyclicModule b

The kernel term of cyclicPresentation is A ⧸ bA.

@[simp]

theorem TauCeti.FGModuleCat.cyclicPresentation_P {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (cyclicPresentation hab).P = ↧Aᵐᵒᵖ

The middle term of cyclicPresentation is the regular module.

@[simp]

theorem TauCeti.FGModuleCat.cyclicPresentation_i {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (cyclicPresentation hab).i = FGModuleCat.ofHom (cyclicMulLeft a b ⋯)

The inflation of cyclicPresentation is left multiplication by a.

@[simp]

theorem TauCeti.FGModuleCat.cyclicPresentation_p {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (cyclicPresentation hab).p = FGModuleCat.ofHom (Submodule.mkQ (Ideal.span {MulOpposite.op a}))

The deflation of cyclicPresentation is the quotient map.

@[reducible, inline]

noncomputable abbrev TauCeti.FGModuleCat.stableModuleLoop (A : Type u) [Ring A] [IsNoetherianRing Aᵐᵒᵖ] : CategoryTheory.Functor (stableModuleCategory A) (stableModuleCategory A)

The loop (syzygy) functor Ω of the stable module category of finitely generated right A-modules: it sends a module to the kernel of a chosen epimorphism onto it from a projective module.

Equations

• TauCeti.FGModuleCat.stableModuleLoop A = ⋯.stableLoop

noncomputable def TauCeti.FGModuleCat.stableModuleLoopCyclicModuleIso {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (stableModuleLoop A).obj ((stableModuleFunctor A).obj (cyclicModule a)) ≅ (stableModuleFunctor A).obj (cyclicModule b)

If the right annihilator of a is bA, then Ω (A ⧸ aA) ≅ A ⧸ bA in the stable module category.

Equations

• TauCeti.FGModuleCat.stableModuleLoopCyclicModuleIso hab = ⋯.stableLoopObjIso (TauCeti.FGModuleCat.cyclicPresentation hab)

noncomputable def TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleIso {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) : (stableModuleLoop A).obj ((stableModuleLoop A).obj ((stableModuleFunctor A).obj (cyclicModule a))) ≅ (stableModuleFunctor A).obj (cyclicModule a)

If the right annihilators of a and of b are bA and aA, then Ω² (A ⧸ aA) ≅ A ⧸ aA in the stable module category.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.FGModuleCat.isZero_stableModuleFunctor_obj_cyclicModule_zero {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] : CategoryTheory.Limits.IsZero ((stableModuleFunctor A).obj (cyclicModule 0))

The module A ⧸ 0A, which is the free module of rank one, is zero in the stable module category.

The truncated polynomial ring R[X]/(X ^ n)

noncomputable def TauCeti.FGModuleCat.stableModuleLoopCyclicModuleRootPowIso (R : Type u) [CommRing R] [IsNoetherianRing R] {n i : ℕ} (hi : i ≤ n) : (stableModuleLoop (AdjoinRoot (Polynomial.X ^ n))).obj ((stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ i))) ≅ (stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ (n - i)))

Over R[X]/(X ^ n), with x the class of X and M_i = A ⧸ (x ^ i), the stable syzygy Ω M_i is M_(n - i) for i ≤ n.

Equations

• TauCeti.FGModuleCat.stableModuleLoopCyclicModuleRootPowIso R hi = TauCeti.FGModuleCat.stableModuleLoopCyclicModuleIso ⋯

noncomputable def TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleRootPowIso (R : Type u) [CommRing R] [IsNoetherianRing R] {n i : ℕ} (hi : i ≤ n) : (stableModuleLoop (AdjoinRoot (Polynomial.X ^ n))).obj ((stableModuleLoop (AdjoinRoot (Polynomial.X ^ n))).obj ((stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ i)))) ≅ (stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ i))

Over R[X]/(X ^ n), with x the class of X and M_i = A ⧸ (x ^ i), the module M_i is periodic of period at most two in the stable module category: Ω² M_i ≅ M_i for i ≤ n.

Equations

• TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleRootPowIso R hi = TauCeti.FGModuleCat.stableModuleLoopLoopCyclicModuleIso ⋯ ⋯

theorem TauCeti.FGModuleCat.isZero_stableModuleFunctor_obj_cyclicModule_root_pow_self (R : Type u) [CommRing R] [IsNoetherianRing R] (n : ℕ) : CategoryTheory.Limits.IsZero ((stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ n)))

Over R[X]/(X ^ n), the module M_n = A ⧸ (x ^ n), which is the free module A since x ^ n = 0, is zero in the stable module category.