Koszul complexes of weakly regular sequences

For a weakly regular sequence x = (x₁, …, xₙ) in a commutative ring R, the Koszul complex K(x) is acyclic in positive degrees: Hₖ(K(x)) = 0 for k > 0. Together with H₀(K(x)) ≃ R ⧸ (x₁, …, xₙ) (TauCeti.koszulComplex.homologyZeroEquivSpan), this says that the complex of finite free modules K(x)ₖ = ⋀ᵏ Rⁿ resolves R ⧸ (x₁, …, xₙ).

The proof adjoins one element at a time. For a linear functional φ : M → R and x : R, the functional (m, r) ↦ φ(m) + r x on M × R is the Koszul complex K(φ, x) of φ with x adjoined. Writing e = (0, 1), every element of ⋀ᵏ⁺¹ (M × R) is uniquely a + e ∧ b with a ∈ ⋀ᵏ⁺¹ M and b ∈ ⋀ᵏ M, and the Koszul differential is d(a + e ∧ b) = (d a + x b) - e ∧ d b. Hence a cycle a + e ∧ b of K(φ, x) has d b = 0 and x b = -d a. If K(φ) is exact at ⋀ᵏ⁺¹ M and b is a boundary, then a + e ∧ b is a boundary. In degree k + 2 the cycle b is a boundary when Hₖ₊₁(K(φ)) = 0; in degree one, x b ∈ φ(M) forces b ∈ φ(M) when x is a nonzerodivisor on R ⧸ φ(M) ≃ H₀(K(φ)). For a weakly regular sequence, induction on its length provides these hypotheses: the higher homology of the shorter sequence vanishes, and the last element is a nonzerodivisor on its zeroth homology R ⧸ (x₁, …, xₙ₋₁).

Main declarations

• TauCeti.exact_koszulDifferential_coprod_succ: if Hₖ₊₂(K(φ)) and Hₖ₊₁(K(φ)) both vanish, then adjoining any element x to φ gives Hₖ₊₂(K(φ, x)) = 0.
• TauCeti.exact_koszulDifferential_coprod_zero: if H₁(K(φ)) vanishes and x is a nonzerodivisor on R ⧸ φ(M), then H₁(K(φ, x)) = 0.
• TauCeti.koszulComplex.exactAt_of_isWeaklyRegular: the Koszul complex of a weakly regular sequence is acyclic in positive degrees.

References

• The Stacks Project, Tags 0626 and 062F

Adjoining one element to a linear functional

theorem TauCeti.exact_koszulDifferential_coprod_succ {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (x : R) (k : ℕ) (h₁ : Function.Exact ⇑(koszulDifferential φ (k + 2)) ⇑(koszulDifferential φ (k + 1))) (h₀ : Function.Exact ⇑(koszulDifferential φ (k + 1)) ⇑(koszulDifferential φ k)) : Function.Exact ⇑(koszulDifferential (LinearMap.coprod φ (LinearMap.toSpanSingleton R R x)) (k + 2)) ⇑(koszulDifferential (LinearMap.coprod φ (LinearMap.toSpanSingleton R R x)) (k + 1))

Adjoining an element preserves higher acyclicity. If the Koszul complex K(φ) is exact at ⋀ᵏ⁺² M and at ⋀ᵏ⁺¹ M, then for every x : R the Koszul complex K(φ, x) of the functional (m, r) ↦ φ(m) + r x on M × R is exact at ⋀ᵏ⁺² (M × R).

theorem TauCeti.exact_koszulDifferential_coprod_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (x : R) (hx : IsSMulRegular (R ⧸ LinearMap.range φ) x) (h₀ : Function.Exact ⇑(koszulDifferential φ 1) ⇑(koszulDifferential φ 0)) : Function.Exact ⇑(koszulDifferential (LinearMap.coprod φ (LinearMap.toSpanSingleton R R x)) 1) ⇑(koszulDifferential (LinearMap.coprod φ (LinearMap.toSpanSingleton R R x)) 0)

Adjoining a nonzerodivisor preserves acyclicity in degree one. If the Koszul complex K(φ) is exact at ⋀¹ M and x is a nonzerodivisor on R ⧸ φ(M) ≃ H₀(K(φ)), then the Koszul complex K(φ, x) of the functional (m, r) ↦ φ(m) + r x on M × R is exact at ⋀¹ (M × R).

theorem TauCeti.koszulComplex.exactAt_of_isWeaklyRegular {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (hx : RingTheory.Sequence.IsWeaklyRegular R (List.ofFn x)) (k : ℕ) : HomologicalComplex.ExactAt (koszulComplex (Fintype.linearCombination R x)) (k + 1)

The Koszul complex of a weakly regular sequence is acyclic in positive degrees: if x = (x₀, …, xₙ₋₁) is a weakly regular sequence in R, then Hₖ₊₁(K(x)) = 0 for every k. With homologyZeroEquivSpan, the complex of finite free modules K(x) resolves R ⧸ (x₀, …, xₙ₋₁).