Two-periodic free resolutions of cyclic modules

Let A be a ring and let a, b : A annihilate each other exactly: the right annihilator of a is bA and the right annihilator of b is aA. Then the cyclic right A-module A ⧸ aA has the two-periodic free resolution

⋯ ⟶ A --b--> A --a--> A --b--> A --a--> A ⟶ A ⧸ aA ⟶ 0,

whose differentials alternate left multiplication by a and by b, and whose augmentation is the quotient map. Right A-modules are left Aᵐᵒᵖ-modules, so the resolution lives in ModuleCat Aᵐᵒᵖ, and A ⧸ aA is the quotient of Aᵐᵒᵖ by the left ideal generated by op a; this is the underlying module of TauCeti.FGModuleCat.cyclicModule a.

The basic example is the truncated polynomial ring A = R[X]/(X ^ n) over any commutative 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 M_i = A ⧸ (x ^ i) has the free resolution whose differentials alternate multiplication by x ^ i and x ^ (n - i). For 0 < i < n every differential has image in xA; when R is a field, xA is the maximal ideal of the local ring A, so this is the minimal free resolution of M_i.

Main definitions

• TauCeti.cyclicModuleResolutionComplex: the two-periodic complex of free rank-one right A-modules with differentials alternating left multiplication by a and b.
• TauCeti.cyclicModuleProjectiveResolution: the resulting projective resolution of A ⧸ aA.
• TauCeti.cyclicModuleRootPowProjectiveResolution: over R[X]/(X ^ n), the projective resolution of M_i alternating multiplication by x ^ i and x ^ (n - i).
• TauCeti.cyclicModuleProjectiveResolutionXIso, TauCeti.cyclicModuleRootPowProjectiveResolutionXIso: every term of these resolutions is the free module A of rank one; the lemmas below are stated through these identifications.

Main results

• TauCeti.range_toSpanSingleton_op_eq_ker: if the right annihilator of a is bA, then on the regular right module the image of left multiplication by b is the kernel of that by a.
• TauCeti.cyclicModuleProjectiveResolution_complex_d: the differential into degree j is left multiplication by a for even j and by b for odd j.
• TauCeti.cyclicModuleProjectiveResolution_π_f_zero: the augmentation is the quotient map.
• TauCeti.unop_cyclicModuleRootPowProjectiveResolution_complex_d_op: the specialized differentials agree with TauCeti.MatrixFactorization.rootPowHom after passing between left and right modules.
• TauCeti.range_cyclicModuleRootPowProjectiveResolution_complex_d_le: for 0 < i < n, every differential of the resolution of M_i has image in xA.

The construction and its quasi-isomorphism proof follow Rep.FiniteCyclicGroup.resolution in Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean and TauCeti.dualNumberProjectiveResolution in TauCeti/Algebra/Homology/Ext/DualNumbers.lean.

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.
• Inês B. Henriques and Liana M. Sega, Free resolutions over short Gorenstein local rings, Mathematische Zeitschrift 267 (2011), 645–663: exact pairs of zero-divisors.

The periodic complex

@[reducible, inline]

noncomputable abbrev TauCeti.cyclicModuleResolutionComplex {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) (hba : b * a = 0) : ChainComplex (ModuleCat Aᵐᵒᵖ) ℕ

For a * b = 0 and b * a = 0, the two-periodic chain complex of right A-modules ⋯ ⟶ A --b--> A --a--> A --b--> A --a--> A in degrees ⋯, 3, 2, 1, 0. Every term is the free module A of rank one, and the differential into degree j is left multiplication by a for even j and by b for odd j; on Aᵐᵒᵖ these are right multiplications by op a and op b.

theorem TauCeti.cyclicModuleResolutionComplex_d {A : Type u} [Ring A] {a b : A} (hab : a * b = 0) (hba : b * a = 0) (j : ℕ) : (cyclicModuleResolutionComplex a b hab hba).d (j + 1) j = ModuleCat.ofHom (LinearMap.toSpanSingleton Aᵐᵒᵖ Aᵐᵒᵖ (MulOpposite.op (if Even j then a else b)))

The differential of TauCeti.cyclicModuleResolutionComplex into degree j is left multiplication by a for even j and by b for odd j.

theorem TauCeti.cyclicModuleResolutionComplex_d_apply {A : Type u} [Ring A] {a b : A} (hab : a * b = 0) (hba : b * a = 0) (j : ℕ) (c : Aᵐᵒᵖ) : (ModuleCat.Hom.hom ((cyclicModuleResolutionComplex a b hab hba).d (j + 1) j)) c = c * MulOpposite.op (if Even j then a else b)

The differential of TauCeti.cyclicModuleResolutionComplex into degree j sends c to c * op a for even j and to c * op b for odd j.

The resolution

theorem TauCeti.range_toSpanSingleton_op_eq_ker {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) : (LinearMap.toSpanSingleton Aᵐᵒᵖ Aᵐᵒᵖ (MulOpposite.op b)).range = (LinearMap.toSpanSingleton Aᵐᵒᵖ Aᵐᵒᵖ (MulOpposite.op a)).ker

If the right annihilator of a is bA, then the image of left multiplication by b on the regular right A-module is the kernel of left multiplication by a.

noncomputable def TauCeti.cyclicModuleProjectiveResolution {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) : CategoryTheory.ProjectiveResolution ↧(Aᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op a})

The two-periodic free resolution of a cyclic module. If the right annihilator of a is bA and the right annihilator of b is aA, then ⋯ ⟶ A --b--> A --a--> A --b--> A --a--> A ⟶ A ⧸ aA ⟶ 0 is a projective resolution of the cyclic right A-module A ⧸ aA.

@[simp]

theorem TauCeti.cyclicModuleProjectiveResolution_complex {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) : (cyclicModuleProjectiveResolution hab hba).complex = cyclicModuleResolutionComplex a b ⋯ ⋯

The complex of TauCeti.cyclicModuleProjectiveResolution is TauCeti.cyclicModuleResolutionComplex.

noncomputable def TauCeti.cyclicModuleProjectiveResolutionXIso {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) (j : ℕ) : (cyclicModuleProjectiveResolution hab hba).complex.X j ≅ ↧Aᵐᵒᵖ

Every term of TauCeti.cyclicModuleProjectiveResolution is the free right A-module A of rank one.

@[simp]

theorem TauCeti.cyclicModuleProjectiveResolution_complex_d {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) (j : ℕ) : (cyclicModuleProjectiveResolution hab hba).complex.d (j + 1) j = CategoryTheory.CategoryStruct.comp (cyclicModuleProjectiveResolutionXIso hab hba (j + 1)).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.toSpanSingleton Aᵐᵒᵖ Aᵐᵒᵖ (MulOpposite.op (if Even j then a else b)))) (cyclicModuleProjectiveResolutionXIso hab hba j).inv)

The differential of TauCeti.cyclicModuleProjectiveResolution into degree j is left multiplication by a for even j and by b for odd j, read through TauCeti.cyclicModuleProjectiveResolutionXIso.

theorem TauCeti.cyclicModuleProjectiveResolution_complex_d_apply {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) (j : ℕ) (c : Aᵐᵒᵖ) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (cyclicModuleProjectiveResolutionXIso hab hba (j + 1)).inv (CategoryTheory.CategoryStruct.comp ((cyclicModuleProjectiveResolution hab hba).complex.d (j + 1) j) (cyclicModuleProjectiveResolutionXIso hab hba j).hom))) c = c * MulOpposite.op (if Even j then a else b)

The differential of TauCeti.cyclicModuleProjectiveResolution into degree j, read through TauCeti.cyclicModuleProjectiveResolutionXIso, sends c to c * op a for even j and to c * op b for odd j.

@[simp]

theorem TauCeti.cyclicModuleProjectiveResolution_π_f_zero {A : Type u} [Ring A] {a b : A} (hab : ∀ (c : A), a * c = 0 ↔ b ∣ c) (hba : ∀ (c : A), b * c = 0 ↔ a ∣ c) : CategoryTheory.CategoryStruct.comp (cyclicModuleProjectiveResolutionXIso hab hba 0).inv ((cyclicModuleProjectiveResolution hab hba).π.f 0) = ModuleCat.ofHom (Submodule.mkQ (Ideal.span {MulOpposite.op a}))

The augmentation of TauCeti.cyclicModuleProjectiveResolution is the quotient map A ⟶ A ⧸ aA, read through TauCeti.cyclicModuleProjectiveResolutionXIso.

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

noncomputable def TauCeti.cyclicModuleRootPowProjectiveResolution (R : Type u) [CommRing R] (n i : ℕ) : CategoryTheory.ProjectiveResolution ↧((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})

The periodic free resolution of M_i over R[X]/(X ^ n). With x the class of X and M_i = A ⧸ (x ^ i), the complex ⋯ ⟶ A --x^(n-i)--> A --x^i--> A --x^(n-i)--> A --x^i--> A ⟶ M_i ⟶ 0 is a projective resolution of M_i.

@[simp]

theorem TauCeti.cyclicModuleRootPowProjectiveResolution_complex (R : Type u) [CommRing R] (n i : ℕ) : (cyclicModuleRootPowProjectiveResolution R n i).complex = (cyclicModuleProjectiveResolution ⋯ ⋯).complex

The complex of TauCeti.cyclicModuleRootPowProjectiveResolution is the general cyclic-module resolution complex specialized to x ^ i and x ^ (n - i).

noncomputable def TauCeti.cyclicModuleRootPowProjectiveResolutionXIso (R : Type u) [CommRing R] (n i j : ℕ) : (cyclicModuleRootPowProjectiveResolution R n i).complex.X j ≅ ↧(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ

Every term of TauCeti.cyclicModuleRootPowProjectiveResolution is the free module A = R[X]/(X ^ n) of rank one.

@[simp]

theorem TauCeti.cyclicModuleRootPowProjectiveResolution_π_f_zero (R : Type u) [CommRing R] (n i : ℕ) : CategoryTheory.CategoryStruct.comp (cyclicModuleRootPowProjectiveResolutionXIso R n i 0).inv ((cyclicModuleRootPowProjectiveResolution R n i).π.f 0) = ModuleCat.ofHom (Submodule.mkQ (Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)}))

The augmentation of TauCeti.cyclicModuleRootPowProjectiveResolution is the quotient map, read through TauCeti.cyclicModuleRootPowProjectiveResolutionXIso.

@[simp]

theorem TauCeti.cyclicModuleRootPowProjectiveResolution_complex_d (R : Type u) [CommRing R] (n i j : ℕ) : (cyclicModuleRootPowProjectiveResolution R n i).complex.d (j + 1) j = CategoryTheory.CategoryStruct.comp (cyclicModuleRootPowProjectiveResolutionXIso R n i (j + 1)).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.toSpanSingleton (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ (MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ if Even j then i else n - i)))) (cyclicModuleRootPowProjectiveResolutionXIso R n i j).inv)

The differential of TauCeti.cyclicModuleRootPowProjectiveResolution into degree j is multiplication by x ^ i for even j and by x ^ (n - i) for odd j, read through TauCeti.cyclicModuleRootPowProjectiveResolutionXIso.

theorem TauCeti.cyclicModuleRootPowProjectiveResolution_complex_d_apply (R : Type u) [CommRing R] (n i j : ℕ) (c : (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (cyclicModuleRootPowProjectiveResolutionXIso R n i (j + 1)).inv (CategoryTheory.CategoryStruct.comp ((cyclicModuleRootPowProjectiveResolution R n i).complex.d (j + 1) j) (cyclicModuleRootPowProjectiveResolutionXIso R n i j).hom))) c = c * MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ if Even j then i else n - i)

The differential of TauCeti.cyclicModuleRootPowProjectiveResolution into degree j, read through TauCeti.cyclicModuleRootPowProjectiveResolutionXIso, sends c to c * op (x ^ i) for even j and to c * op (x ^ (n - i)) for odd j.

theorem TauCeti.unop_cyclicModuleRootPowProjectiveResolution_complex_d_op (R : Type u) [CommRing R] (n i j : ℕ) (c : AdjoinRoot (Polynomial.X ^ n)) : MulOpposite.unop ((ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (cyclicModuleRootPowProjectiveResolutionXIso R n i (j + 1)).inv (CategoryTheory.CategoryStruct.comp ((cyclicModuleRootPowProjectiveResolution R n i).complex.d (j + 1) j) (cyclicModuleRootPowProjectiveResolutionXIso R n i j).hom))) (MulOpposite.op c)) = (CategoryTheory.ConcreteCategory.hom (MatrixFactorization.rootPowHom R n (if Even j then i else n - i))) c

After identifying right modules with opposites, the specialized resolution differential is the multiplication map underlying TauCeti.MatrixFactorization.powerXPeriodicComplex.

theorem TauCeti.range_cyclicModuleRootPowProjectiveResolution_complex_d_le (R : Type u) [CommRing R] (n i : ℕ) (hi₀ : 0 < i) (hin : i < n) (j : ℕ) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (cyclicModuleRootPowProjectiveResolutionXIso R n i (j + 1)).inv (CategoryTheory.CategoryStruct.comp ((cyclicModuleRootPowProjectiveResolution R n i).complex.d (j + 1) j) (cyclicModuleRootPowProjectiveResolutionXIso R n i j).hom))).range ≤ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n))}

For 0 < i < n, every differential of the free resolution of M_i = A ⧸ (x ^ i) over A = R[X]/(X ^ n), read through TauCeti.cyclicModuleRootPowProjectiveResolutionXIso, has image in xA. When R is a field, xA is the maximal ideal of the local ring A, and this is the condition for a free resolution over A to be minimal.