The Koszul complex of a linear functional

For a linear functional φ : M → R on a module over a commutative ring, the Koszul complex K(φ) is the chain complex ⋯ → ⋀³ M → ⋀² M → M → R with K(φ)ₙ = ⋀ⁿ M and differential the contraction by φ, d(v₀ ∧ ⋯ ∧ vₙ) = ∑ᵢ (-1) ^ i φ(vᵢ) v₀ ∧ ⋯ ∧ v̂ᵢ ∧ ⋯ ∧ vₙ. For a finite sequence x = (x₁, …, xₙ) in R, the functional v ↦ ∑ᵢ vᵢ xᵢ on Rⁿ gives the Koszul complex K(x) of the sequence, whose zeroth homology is R ⧸ (x₁, …, xₙ).

Main declarations

• TauCeti.koszulComplex φ: the Koszul complex of φ, as an ℕ-indexed chain complex of R-modules.
• TauCeti.koszulDifferential φ n: its differential ⋀ⁿ⁺¹ M → ⋀ⁿ M, the contraction by φ, with the alternating-deletion formula TauCeti.koszulDifferential_ιMulti.
• TauCeti.zeroEquiv_koszulDifferential_zero: under ⋀⁰ M ≅ R and ⋀¹ M ≅ M, the first differential is φ itself.
• TauCeti.exact_koszulDifferential_of_retract: exactness of a Koszul complex passes to a retract along linear maps compatible with the functionals.
• TauCeti.map_fst_koszulDifferential_coprod: the coordinate formula for the differential after adjoining one scalar to a linear functional.
• TauCeti.koszulComplex.exactAt_succ_iff: Hₖ₊₁(K(φ)) = 0 exactly when the Koszul differentials out of and into ⋀ᵏ⁺¹ M are exact.
• TauCeti.koszulComplex.map: the chain map K(φ) → K(ψ) induced by a linear map g with ψ ∘ g = φ, functorial in g, and TauCeti.koszulComplex.mapIso, the isomorphism induced by a linear equivalence.
• TauCeti.koszulComplex.smulHomotopy: for m : M, exterior multiplication by m is a null-homotopy of multiplication by φ(m), so that φ(m) annihilates the Koszul homology (TauCeti.koszulComplex.smul_homology_eq_zero).
• TauCeti.koszulComplex.homologyZeroEquiv: H₀(K(φ)) ≃ R ⧸ φ(M), and its specialization TauCeti.koszulComplex.homologyZeroEquivSpan to H₀(K(x)) ≃ R ⧸ (x₁, …, xₙ) for a finite sequence.

References

• The Stacks Project, Tags 0622, 0623 and 0624

The interface (the Koszul complex of a linear functional with exterior-power terms, the alternating-deletion differential, koszulComplex.map along ψ ∘ g = φ, and the homotopy d(m ∧ v) + m ∧ d(v) = φ(m) v) follows the design of Nailin Guan in the Mathlib pull requests mathlib4#43708 (definition of the Koszul complex) and mathlib4#43706 (homotopy of the Koszul complex). No code from those pull requests is vendored here.

def TauCeti.koszulDifferential {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : ↥(⋀[R]^(n + 1) M) →ₗ[R] ↥(⋀[R]^n M)

The Koszul differential ⋀ⁿ⁺¹ M → ⋀ⁿ M of a linear functional φ: the contraction by φ, v₀ ∧ ⋯ ∧ vₙ ↦ ∑ᵢ (-1) ^ i φ(vᵢ) v₀ ∧ ⋯ ∧ v̂ᵢ ∧ ⋯ ∧ vₙ (see koszulDifferential_ιMulti).

@[simp]

theorem TauCeti.coe_koszulDifferential_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) (x : ↥(⋀[R]^(n + 1) M)) : ↑((koszulDifferential φ n) x) = (CliffordAlgebra.contractLeft φ) ↑x

The Koszul differential is the contraction by φ.

theorem TauCeti.koszulDifferential_ιMulti {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) (v : Fin (n + 1) → M) : (koszulDifferential φ n) ((exteriorPower.ιMulti R (n + 1)) v) = ∑ i : Fin (n + 1), ((-1) ^ ↑i * φ (v i)) • (exteriorPower.ιMulti R n) (i.removeNth v)

The Koszul differential on a wedge product of vectors is the alternating sum of deletions: d(v₀ ∧ ⋯ ∧ vₙ) = ∑ᵢ (-1) ^ i φ(vᵢ) v₀ ∧ ⋯ ∧ v̂ᵢ ∧ ⋯ ∧ vₙ.

@[simp]

theorem TauCeti.koszulDifferential_comp_koszulDifferential {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : koszulDifferential φ n ∘ₗ koszulDifferential φ (n + 1) = 0

The Koszul differential squares to zero.

@[simp]

theorem TauCeti.koszulDifferential_koszulDifferential {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) (x : ↥(⋀[R]^(n + 2) M)) : (koszulDifferential φ n) ((koszulDifferential φ (n + 1)) x) = 0

The Koszul differential squares to zero, elementwise.

theorem TauCeti.zeroEquiv_comp_koszulDifferential_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) : ↑(exteriorPower.zeroEquiv R M) ∘ₗ koszulDifferential φ 0 = φ ∘ₗ ↑(exteriorPower.oneEquiv R M)

The first Koszul differential is φ: under the identifications ⋀⁰ M ≅ R and ⋀¹ M ≅ M, the differential ⋀¹ M → ⋀⁰ M is φ.

@[simp]

theorem TauCeti.zeroEquiv_koszulDifferential_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (x : ↥(⋀[R]^1 M)) : (exteriorPower.zeroEquiv R M) ((koszulDifferential φ 0) x) = φ ((exteriorPower.oneEquiv R M) x)

The first Koszul differential is φ, elementwise.

@[simp]

theorem TauCeti.koszulDifferential_zero_oneEquiv_symm {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) : (koszulDifferential φ 0) ((exteriorPower.oneEquiv R M).symm m) = φ m • (exteriorPower.zeroEquiv R M).symm 1

The first Koszul differential sends a vector, viewed in ⋀¹ M, to its value under φ, viewed in ⋀⁰ M.

@[simp]

theorem TauCeti.oneEquiv_koszulDifferential_one {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (v : Fin 2 → M) : (exteriorPower.oneEquiv R M) ((koszulDifferential φ 1) ((exteriorPower.ιMulti R 2) v)) = φ (v 0) • v 1 - φ (v 1) • v 0

In degree two, the Koszul differential sends u ∧ v to φ(u) v - φ(v) u.

theorem TauCeti.map_zeroEquiv_range_koszulDifferential_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) : Submodule.map (↑(exteriorPower.zeroEquiv R M)) (koszulDifferential φ 0).range = LinearMap.range φ

The image of the first Koszul differential, transported along ⋀⁰ M ≅ R, is the image of φ.

theorem TauCeti.koszulDifferential_comp_map {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) {N : Type u_1} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} {g : M →ₗ[R] N} (h : ψ ∘ₗ g = φ) (n : ℕ) : koszulDifferential ψ n ∘ₗ exteriorPower.map (n + 1) g = exteriorPower.map n g ∘ₗ koszulDifferential φ n

The Koszul differential is natural: if ψ ∘ g = φ, then ⋀ g intertwines the Koszul differentials of φ and ψ.

@[simp]

theorem TauCeti.koszulDifferential_map {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] (ψ : Module.Dual R N) (g : M →ₗ[R] N) (n : ℕ) (x : ↥(⋀[R]^(n + 1) M)) : (koszulDifferential ψ n) ((exteriorPower.map (n + 1) g) x) = (exteriorPower.map n g) ((koszulDifferential (ψ ∘ₗ g) n) x)

The Koszul differential is natural, elementwise: ⋀ g carries the Koszul differential of ψ ∘ g to that of ψ.

theorem TauCeti.map_fst_koszulDifferential_coprod {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (x : R) (k : ℕ) (z : ↥(⋀[R]^(k + 1) (M × R))) : (exteriorPower.map k (LinearMap.fst R M R)) ((koszulDifferential (LinearMap.coprod φ (LinearMap.toSpanSingleton R R x)) k) z) = (koszulDifferential φ k) ((exteriorPower.map (k + 1) (LinearMap.fst R M R)) z) + x • (exteriorPower.map k (LinearMap.fst R M R)) ((koszulDifferential (LinearMap.snd R M R) k) z)

The ⋀ M-component of the Koszul differential of K(φ, x): writing z = a + e ∧ b, it is d a + x b.

theorem TauCeti.exact_koszulDifferential_of_retract {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type u_1} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (g : M →ₗ[R] N) (h : N →ₗ[R] M) (hhg : h ∘ₗ g = LinearMap.id) (hψ : φ ∘ₗ h = ψ) (n : ℕ) (hex : Function.Exact ⇑(koszulDifferential ψ (n + 1)) ⇑(koszulDifferential ψ n)) : Function.Exact ⇑(koszulDifferential φ (n + 1)) ⇑(koszulDifferential φ n)

Exactness passes to retracts. If g : M → N has a retraction h and ψ = φ ∘ h (so that also φ = ψ ∘ g), then the Koszul complex K(φ) is a retract of K(ψ), and exactness of K(ψ) at ⋀ⁿ⁺¹ N implies exactness of K(φ) at ⋀ⁿ⁺¹ M.

theorem TauCeti.koszulDifferential_comp_wedgeLeft_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) : koszulDifferential φ 0 ∘ₗ ExteriorAlgebra.wedgeLeft m 0 = φ m • LinearMap.id

The Koszul homotopy identity in degree zero: d(m ∧ r) = φ(m) r for r ∈ ⋀⁰ M.

theorem TauCeti.wedgeLeft_comp_koszulDifferential_add {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) (n : ℕ) : ExteriorAlgebra.wedgeLeft m n ∘ₗ koszulDifferential φ n + koszulDifferential φ (n + 1) ∘ₗ ExteriorAlgebra.wedgeLeft m (n + 1) = φ m • LinearMap.id

The Koszul homotopy identity in positive degrees: m ∧ d(v) + d(m ∧ v) = φ(m) v.

def TauCeti.koszulComplex {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) : ChainComplex (ModuleCat R) ℕ

The Koszul complex K(φ) of a linear functional φ : M → R: the ℕ-indexed chain complex with K(φ)ₙ = ⋀ⁿ M and differential koszulDifferential φ, the contraction by φ.

The body is exposed so that the terms of the complex are definitionally the exterior powers, and elements of (koszulComplex φ).X n can be used as elements of ⋀ⁿ M.

@[simp]

theorem TauCeti.koszulComplex_X {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : (koszulComplex φ).X n = ↧↥(⋀[R]^n M)

The terms of the Koszul complex are the exterior powers.

theorem TauCeti.koszulComplex_d {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : (koszulComplex φ).d (n + 1) n = ModuleCat.ofHom (koszulDifferential φ n)

The differential of the Koszul complex is the Koszul differential.

@[simp]

theorem TauCeti.koszulComplex_d_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) (x : ↥(⋀[R]^(n + 1) M)) : (ModuleCat.Hom.hom ((koszulComplex φ).d (n + 1) n)) x = (koszulDifferential φ n) x

The differential of the Koszul complex is the Koszul differential, elementwise.

theorem TauCeti.koszulComplex.exactAt_succ_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (k : ℕ) : HomologicalComplex.ExactAt (koszulComplex φ) (k + 1) ↔ Function.Exact ⇑(koszulDifferential φ (k + 1)) ⇑(koszulDifferential φ k)

The Koszul complex K(φ) is exact at ⋀ᵏ⁺¹ M, i.e. Hₖ₊₁(K(φ)) = 0, exactly when the Koszul differentials ⋀ᵏ⁺² M → ⋀ᵏ⁺¹ M → ⋀ᵏ M are exact.

noncomputable def TauCeti.koszulComplex.map {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type v} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (g : M →ₗ[R] N) (h : ψ ∘ₗ g = φ) : koszulComplex φ ⟶ koszulComplex ψ

The chain map K(φ) → K(ψ) induced by a linear map g : M → N with ψ ∘ g = φ: in degree n it is ⋀ⁿ g.

@[simp]

theorem TauCeti.koszulComplex.map_f {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type v} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (g : M →ₗ[R] N) (h : ψ ∘ₗ g = φ) (n : ℕ) : (map g h).f n = ModuleCat.ofHom (exteriorPower.map n g)

In degree n, the chain map induced by g is ⋀ⁿ g.

@[simp]

theorem TauCeti.koszulComplex.map_id {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} : map LinearMap.id ⋯ = CategoryTheory.CategoryStruct.id (koszulComplex φ)

The identity of M induces the identity of K(φ).

theorem TauCeti.koszulComplex.map_comp {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N P : Type v} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {ψ : Module.Dual R N} {χ : Module.Dual R P} (g : M →ₗ[R] N) (h : ψ ∘ₗ g = φ) (g' : N →ₗ[R] P) (h' : χ ∘ₗ g' = ψ) : map (g' ∘ₗ g) ⋯ = CategoryTheory.CategoryStruct.comp (map g h) (map g' h')

The chain map induced by a composite is the composite of the induced chain maps.

theorem TauCeti.koszulComplex.map_comp_assoc {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N P : Type v} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {ψ : Module.Dual R N} {χ : Module.Dual R P} (g : M →ₗ[R] N) (h : ψ ∘ₗ g = φ) (g' : N →ₗ[R] P) (h' : χ ∘ₗ g' = ψ) {Z : ChainComplex (ModuleCat R) ℕ} (h✝ : koszulComplex χ ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (g' ∘ₗ g) ⋯) h✝ = CategoryTheory.CategoryStruct.comp (map g h) (CategoryTheory.CategoryStruct.comp (map g' h') h✝)

The chain map induced by a composite is the composite of the induced chain maps.

noncomputable def TauCeti.koszulComplex.mapIso {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type v} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (e : M ≃ₗ[R] N) (h : ψ ∘ₗ ↑e = φ) : koszulComplex φ ≅ koszulComplex ψ

The isomorphism K(φ) ≅ K(ψ) induced by a linear equivalence e : M ≃ N with ψ ∘ e = φ; in degree n it is ⋀ⁿ e.

@[simp]

theorem TauCeti.koszulComplex.mapIso_hom {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type v} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (e : M ≃ₗ[R] N) (h : ψ ∘ₗ ↑e = φ) : (mapIso e h).hom = map (↑e) h

The isomorphism induced by a linear equivalence e is the chain map induced by e.

@[simp]

theorem TauCeti.koszulComplex.mapIso_inv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : Module.Dual R M} {N : Type v} [AddCommGroup N] [Module R N] {ψ : Module.Dual R N} (e : M ≃ₗ[R] N) (h : ψ ∘ₗ ↑e = φ) : (mapIso e h).inv = map ↑e.symm ⋯

The inverse of the isomorphism induced by e is the chain map induced by e.symm.

def TauCeti.koszulComplex.smulHomotopy {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) : Homotopy (φ m • CategoryTheory.CategoryStruct.id (koszulComplex φ)) 0

Koszul homotopy: for m : M, exterior multiplication v ↦ m ∧ v is a null-homotopy of multiplication by φ(m) on K(φ); see koszulDifferential_comp_wedgeLeft_zero and wedgeLeft_comp_koszulDifferential_add.

@[simp]

theorem TauCeti.koszulComplex.smulHomotopy_hom {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) (n : ℕ) : (smulHomotopy φ m).hom n (n + 1) = ModuleCat.ofHom (ExteriorAlgebra.wedgeLeft m n)

The components of the Koszul homotopy are exterior multiplication by m.

theorem TauCeti.koszulComplex.smul_homology_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (m : M) (n : ℕ) (z : ↑(HomologicalComplex.homology (koszulComplex φ) n)) : φ m • z = 0

Every value of φ annihilates the Koszul homology: φ(m) • z = 0 for every class z in every homology module of K(φ).

theorem TauCeti.koszulComplex.range_le_annihilator_homology {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : LinearMap.range φ ≤ Module.annihilator R ↑(HomologicalComplex.homology (koszulComplex φ) n)

The image ideal of the functional annihilates Koszul homology.

@[simp]

theorem TauCeti.koszulComplex.primaryComponent_homology_eq_top {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (n : ℕ) : Ideal.primaryComponent (↑(HomologicalComplex.homology (koszulComplex φ) n)) (LinearMap.range φ) = ⊤

Koszul homology is power torsion for the image ideal of the functional.

noncomputable def TauCeti.koszulComplex.homologyZeroEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) : ↑(HomologicalComplex.homology (koszulComplex φ) 0) ≃ₗ[R] R ⧸ LinearMap.range φ

Zeroth Koszul homology: H₀(K(φ)) ≃ R ⧸ φ(M). It is the cokernel of the first differential, transported along ⋀⁰ M ≅ R; see homologyZeroEquiv_apply.

@[simp]

theorem TauCeti.koszulComplex.homologyZeroEquiv_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : Module.Dual R M) (x : ↥(⋀[R]^0 M)) : (homologyZeroEquiv φ) ((ModuleCat.Hom.hom (koszulComplex φ).isoHomologyι₀.inv) ((ModuleCat.Hom.hom (HomologicalComplex.pOpcycles (koszulComplex φ) 0)) x)) = (Ideal.Quotient.mk (LinearMap.range φ)) ((exteriorPower.zeroEquiv R M) x)

homologyZeroEquiv sends the class of x ∈ ⋀⁰ M to the class of the corresponding scalar.

noncomputable def TauCeti.koszulComplex.homologyZeroEquivSpan {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (x : ι → R) : ↑(HomologicalComplex.homology (koszulComplex (Fintype.linearCombination R x)) 0) ≃ₗ[R] R ⧸ Ideal.span (Set.range x)

Zeroth Koszul homology of a finite sequence: for x = (xᵢ) in R, the Koszul complex of the functional v ↦ ∑ᵢ vᵢ xᵢ has H₀ ≃ R ⧸ (xᵢ).

@[simp]

theorem TauCeti.koszulComplex.homologyZeroEquivSpan_apply {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (x : ι → R) (y : ↥(⋀[R]^0 (ι → R))) : (homologyZeroEquivSpan x) ((ModuleCat.Hom.hom (koszulComplex (Fintype.linearCombination R x)).isoHomologyι₀.inv) ((ModuleCat.Hom.hom (HomologicalComplex.pOpcycles (koszulComplex (Fintype.linearCombination R x)) 0)) y)) = (Ideal.Quotient.mk (Ideal.span (Set.range x))) ((exteriorPower.zeroEquiv R (ι → R)) y)

homologyZeroEquivSpan sends the class of y ∈ ⋀⁰ Rⁿ to the class of the corresponding scalar modulo (xᵢ).