Polynomial matrix factorizations modulo their potential

The rank-one factorization of X ^ n with maps X ^ i and X ^ (n - i) reduces modulo X ^ n to the two-periodic complex of free rank-one modules with maps given by multiplication by the corresponding powers of the residue class x of X. This file constructs that complex, proves it is exact in both parities, and identifies it with the generic reduction of MatrixFactorization.powerXOfLE.

Thus the matrix factorization supplies the unaugmented exact periodic complex underlying the free resolution of the cyclic module R[X]/(X ^ i), viewed as a module over R[X]/(X ^ n). The augmentation and cokernel identification are separate from this construction. The exactness argument works over every commutative base ring: the annihilator of x ^ i in R[X]/(X ^ n) is generated by x ^ (n - i).

References

• D. Eisenbud, Homological algebra on a complete intersection, with an application to group representations, Trans. Amer. Math. Soc. 260 (1980), Section 5.

noncomputable def TauCeti.MatrixFactorization.rootPowHom (R : Type u) [CommRing R] (n j : ℕ) : ↧(AdjoinRoot (Polynomial.X ^ n)) ⟶ ↧(AdjoinRoot (Polynomial.X ^ n))

Multiplication by the jth power of the residue class of X on the regular module over R[X]/(X ^ n).

@[simp]

theorem TauCeti.MatrixFactorization.rootPowHom_apply (R : Type u) [CommRing R] (n j : ℕ) (a : AdjoinRoot (Polynomial.X ^ n)) : (CategoryTheory.ConcreteCategory.hom (rootPowHom R n j)) a = AdjoinRoot.root (Polynomial.X ^ n) ^ j * a

Multiplication by x ^ j sends a to x ^ j * a.

theorem TauCeti.MatrixFactorization.rootPowHom_eq_smul_id (R : Type u) [CommRing R] (n j : ℕ) : rootPowHom R n j = AdjoinRoot.root (Polynomial.X ^ n) ^ j • CategoryTheory.CategoryStruct.id ↧(AdjoinRoot (Polynomial.X ^ n))

Multiplication by x ^ j is scalar multiplication of the identity by x ^ j.

@[simp]

theorem TauCeti.MatrixFactorization.rootPowHom_comp (R : Type u) [CommRing R] (n a b : ℕ) : CategoryTheory.CategoryStruct.comp (rootPowHom R n a) (rootPowHom R n b) = rootPowHom R n (a + b)

Composing multiplication by x ^ a with multiplication by x ^ b multiplies by x ^ (a + b).

@[simp]

theorem TauCeti.MatrixFactorization.rootPowHom_self (R : Type u) [CommRing R] (n : ℕ) : rootPowHom R n n = 0

Multiplication by x ^ n vanishes on R[X]/(X ^ n).

noncomputable def TauCeti.MatrixFactorization.powerXPeriodicDuplex (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : CurvedDuplex (ModuleCat (AdjoinRoot (Polynomial.X ^ n))) 0

The square-zero duplex of free rank-one R[X]/(X ^ n)-modules with differentials x ^ i and x ^ (n - i).

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicDuplex_d₀ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicDuplex R hi).d₀ = rootPowHom R n i

The zero-to-one differential is multiplication by x ^ i.

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicDuplex_d₁ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicDuplex R hi).d₁ = rootPowHom R n (n - i)

The one-to-zero differential is multiplication by x ^ (n - i).

noncomputable def TauCeti.MatrixFactorization.powerXPeriodicComplex (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : HomologicalComplex (ModuleCat (AdjoinRoot (Polynomial.X ^ n))) (ComplexShape.up (ZMod 2))

The explicit two-periodic free complex over R[X]/(X ^ n) associated to the factorization X ^ i · X ^ (n - i) = X ^ n.

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicComplex_X_zero (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicComplex R hi).X 0 = ↧(AdjoinRoot (Polynomial.X ^ n))

The even term of powerXPeriodicComplex is the free rank-one module.

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicComplex_X_one (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicComplex R hi).X 1 = ↧(AdjoinRoot (Polynomial.X ^ n))

The odd term of powerXPeriodicComplex is the free rank-one module.

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicComplex_d_zero_one (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicComplex R hi).d 0 1 = rootPowHom R n i

The differential from parity zero to parity one is multiplication by x ^ i.

@[simp]

theorem TauCeti.MatrixFactorization.powerXPeriodicComplex_d_one_zero (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicComplex R hi).d 1 0 = rootPowHom R n (n - i)

The differential from parity one to parity zero is multiplication by x ^ (n - i).

theorem TauCeti.MatrixFactorization.powerXPeriodicComplex_acyclic (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXPeriodicComplex R hi).Acyclic

The two-periodic complex with alternating maps x ^ i and x ^ (n - i) is exact in every degree. No field or positivity hypothesis is needed.

Comparison with reduction of the matrix factorization

theorem TauCeti.MatrixFactorization.extendScalars_η_comp_rootPowHom (R : Type u) [CommRing R] (n j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))) (rootPowHom R n j) = CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n))).map (Polynomial.X ^ j • CategoryTheory.CategoryStruct.id ↧(Polynomial R))) (CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n))))

The counit morphism η of the monoidal functor ModuleCat.extendScalars intertwines the base change of multiplication by X ^ j with multiplication by x ^ j.

noncomputable def TauCeti.MatrixFactorization.powerXOfLEBaseChangeDuplexIso (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (baseChangeToCurvedDuplex (AdjoinRoot.mk (Polynomial.X ^ n)) ⋯).obj (powerXOfLE R hi) ≅ powerXPeriodicDuplex R hi

Reducing powerXOfLE along R[X] → R[X]/(X ^ n) gives the explicit square-zero duplex with alternating differentials x ^ i and x ^ (n - i).

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangeDuplexIso_hom_f₀ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangeDuplexIso R hi).hom.f₀ = CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The even component of powerXOfLEBaseChangeDuplexIso.hom is the counit morphism η of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangeDuplexIso_hom_f₁ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangeDuplexIso R hi).hom.f₁ = CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The odd component of powerXOfLEBaseChangeDuplexIso.hom is the counit morphism η of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangeDuplexIso_inv_f₀ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangeDuplexIso R hi).inv.f₀ = CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The even component of powerXOfLEBaseChangeDuplexIso.inv is the unit morphism ε of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangeDuplexIso_inv_f₁ (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangeDuplexIso R hi).inv.f₁ = CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The odd component of powerXOfLEBaseChangeDuplexIso.inv is the unit morphism ε of ModuleCat.extendScalars.

noncomputable def TauCeti.MatrixFactorization.powerXOfLEBaseChangePeriodicIso (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (toPeriodicComplex (AdjoinRoot.mk (Polynomial.X ^ n)) ⋯).obj (powerXOfLE R hi) ≅ powerXPeriodicComplex R hi

The canonical base change of powerXOfLE is isomorphic to the explicit two-periodic free complex powerXPeriodicComplex.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangePeriodicIso_hom_f_zero (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangePeriodicIso R hi).hom.f 0 = CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The degree-zero component of powerXOfLEBaseChangePeriodicIso.hom is the counit morphism η of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangePeriodicIso_hom_f_one (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangePeriodicIso R hi).hom.f 1 = CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The degree-one component of powerXOfLEBaseChangePeriodicIso.hom is the counit morphism η of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangePeriodicIso_inv_f_zero (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangePeriodicIso R hi).inv.f 0 = CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The degree-zero component of powerXOfLEBaseChangePeriodicIso.inv is the unit morphism ε of ModuleCat.extendScalars.

@[simp]

theorem TauCeti.MatrixFactorization.powerXOfLEBaseChangePeriodicIso_inv_f_one (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : (powerXOfLEBaseChangePeriodicIso R hi).inv.f 1 = CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.extendScalars (AdjoinRoot.mk (Polynomial.X ^ n)))

The degree-one component of powerXOfLEBaseChangePeriodicIso.inv is the unit morphism ε of ModuleCat.extendScalars.

theorem TauCeti.MatrixFactorization.powerXOfLE_baseChange_acyclic (R : Type u) [CommRing R] {i n : ℕ} (hi : i ≤ n) : ((toPeriodicComplex (AdjoinRoot.mk (Polynomial.X ^ n)) ⋯).obj (powerXOfLE R hi)).Acyclic

The two-periodic complex obtained by reducing powerXOfLE modulo X ^ n is exact in every degree.