The Koszul differential in a basis

Let M be a free module with basis (bᵢ) and let φ : M → R be a linear functional. In the exterior-power basis, the contraction by the coordinate bᵢ* deletes the index i, so the Koszul differential of φ is d(z) = ∑ᵢ φ(bᵢ) ιᵢ(z) with ιᵢ the contraction by bᵢ*. The family of all contractions z ↦ (ιᵢ(z))ᵢ is the linearized Koszul differential ⋀ⁿ⁺¹ M → ⋀ⁿ M ⊗ M, and it is split injective coordinatewise: the coordinate of z at an index set s ∋ i is, up to sign, the coordinate of ιᵢ(z) at s \ {i}. Hence for every ideal I, an element z of positive degree lies in I • ⋀ M exactly when all its contractions ιᵢ(z) do.

Main results

• Module.Basis.koszulDifferential_eq_sum: the Koszul differential of φ is ∑ᵢ φ(bᵢ) ιᵢ.
• Module.Basis.koszulDifferential_coord_exteriorPower_basis_of_mem and Module.Basis.koszulDifferential_coord_exteriorPower_basis_of_notMem: contraction by a coordinate on the exterior-power basis.
• Module.Basis.exteriorPower_basis_repr_koszulDifferential_coord: the coordinates of a contraction.
• Module.Basis.mem_smul_top_iff_forall_koszulDifferential_coord_mem: an element of positive degree lies in I • ⋀ M exactly when all its coordinate contractions do.

References

• The Stacks Project, Lemma 10.110.3

theorem Module.Basis.koszulDifferential_eq_sum {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [Fintype ι] (b : Basis ι R M) (φ : Dual R M) (n : ℕ) (z : ↥(⋀[R]^(n + 1) M)) : (TauCeti.koszulDifferential φ n) z = ∑ i : ι, φ (b i) • (TauCeti.koszulDifferential (b.coord i) n) z

The Koszul differential of φ is the combination of the contractions by the coordinates of a finite basis, with coefficients φ(bᵢ): d(z) = ∑ᵢ φ(bᵢ) ιᵢ(z).

theorem Module.Basis.koszulDifferential_coord_exteriorPower_basis_of_mem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [LinearOrder ι] (b : Basis ι R M) {n : ℕ} {i : ι} {s : ↑(Set.powersetCard ι (n + 1))} (h : i ∈ ↑s) : (TauCeti.koszulDifferential (b.coord i) n) ((exteriorPower (n + 1) b) s) = TauCeti.ExteriorAlgebra.basisEraseSign i ↑s • (exteriorPower n b) (Set.powersetCard.ofCard ⋯)

Contraction by the coordinate bᵢ* erases i from an exterior-basis vector whose index set contains it, with the shuffle sign that moves i to the front.

theorem Module.Basis.koszulDifferential_coord_exteriorPower_basis_of_notMem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [LinearOrder ι] (b : Basis ι R M) {n : ℕ} {i : ι} {s : ↑(Set.powersetCard ι (n + 1))} (h : i ∉ ↑s) : (TauCeti.koszulDifferential (b.coord i) n) ((exteriorPower (n + 1) b) s) = 0

Contraction by the coordinate bᵢ* kills an exterior-basis vector whose index set does not contain i.

theorem Module.Basis.exteriorPower_basis_repr_koszulDifferential_coord {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [LinearOrder ι] (b : Basis ι R M) {n : ℕ} (z : ↥(⋀[R]^(n + 1) M)) {i : ι} {s : ↑(Set.powersetCard ι (n + 1))} (h : i ∈ ↑s) : ((exteriorPower n b).repr ((TauCeti.koszulDifferential (b.coord i) n) z)) (Set.powersetCard.ofCard ⋯) = TauCeti.ExteriorAlgebra.basisEraseSign i ↑s • ((exteriorPower (n + 1) b).repr z) s

The coordinates of a contraction: for i ∈ s, the coordinate of ιᵢ(z) at s \ {i} is the coordinate of z at s, up to the shuffle sign moving i to the front of s.

theorem Module.Basis.mem_smul_top_iff_forall_koszulDifferential_coord_mem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) (I : Ideal R) {n : ℕ} (z : ↥(⋀[R]^(n + 1) M)) : z ∈ I • ⊤ ↔ ∀ (i : ι), (TauCeti.koszulDifferential (b.coord i) n) z ∈ I • ⊤

The linearized Koszul differential is injective modulo every ideal. For a module with a basis (bᵢ), an element z of positive exterior degree lies in I • ⋀ M exactly when its contractions by all coordinates bᵢ* do.