Maps out of a Koszul complex that are injective modulo an ideal

Let M be a free module with basis (bᵢ) and let φ : M → R be a linear functional, with values xᵢ = φ(bᵢ). This file proves the inductive step of the proof of Stacks, Lemma 10.110.3 (00OA). Suppose the xᵢ lie in an ideal I and are linearly independent in I/I², and compare the Koszul complex with a complex whose differential d' lands in I times its target, as for a minimal free resolution over a local ring with I the maximal ideal. If a chain map α is injective modulo I in degree n, with free target, then it is injective modulo I in degree n + 1: if α(z) ∈ I F' then α(d z) = d'(α z) ∈ I² F, so ∑ xᵢ α(ιᵢ z) ∈ I² F, where ιᵢ is the contraction by the coordinate bᵢ*, whence every α(ιᵢ z) ∈ I F, every ιᵢ z ∈ I ⋀ⁿ M, and finally z ∈ I ⋀ⁿ⁺¹ M by Module.Basis.mem_smul_top_iff_forall_koszulDifferential_coord_mem.

Iterating the step, a chain map from the Koszul complex into a complex of free modules whose differentials land in I times their targets is injective modulo I in every degree as soon as it is so in degree 0. In degree 0 this holds whenever the chain map lies over the augmentation ⋀⁰ M ≅ R → R ⧸ I.

Main results

• LinearMap.comap_smul_top_le_of_comp_eq_mkQ_zeroEquiv: a map out of ⋀⁰ M lifting the augmentation ⋀⁰ M ≅ R → R ⧸ I is injective modulo I.
• Module.Basis.comap_smul_top_le_of_comp_koszulDifferential: a map compatible with the Koszul differential and a differential landing in I times its target is injective modulo I in degree n + 1 if it is so in degree n.
• Module.Basis.comap_smul_top_le_of_hom_koszulComplex: a chain map from the Koszul complex into such a complex of free modules is injective modulo I in every degree if it is so in degree 0.

References

• The Stacks Project, Lemma 10.110.3

theorem LinearMap.comap_smul_top_le_of_comp_eq_mkQ_zeroEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {F : Type u_1} [AddCommGroup F] [Module R F] {I : Ideal R} (α : ↥(⋀[R]^0 M) →ₗ[R] F) (π : F →ₗ[R] R ⧸ I) (h : π ∘ₗ α = Submodule.mkQ I ∘ₗ ↑(exteriorPower.zeroEquiv R M)) : Submodule.comap α (I • ⊤) ≤ I • ⊤

Degree 0 of the comparison with a Koszul complex. A map α : ⋀⁰ M → F lifting the augmentation ⋀⁰ M ≅ R → R ⧸ I along some π : F → R ⧸ I is injective modulo I: α(z) ∈ I F forces z ∈ I ⋀⁰ M, as π carries I F into I (R ⧸ I) = 0.

theorem Module.Basis.comap_smul_top_le_of_comp_koszulDifferential {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) (φ : Dual R M) {I : Ideal R} (hφ : ∀ (i : ι), φ (b i) ∈ I) (hli : LinearIndependent (R ⧸ I) fun (i : ι) => I.toCotangent ⟨φ (b i), ⋯⟩) {F : Type u_2} {F' : Type u_3} [AddCommGroup F] [Module R F] [Free R F] [AddCommGroup F'] [Module R F'] {d : F' →ₗ[R] F} (hd : d.range ≤ I • ⊤) {n : ℕ} {α : ↥(⋀[R]^n M) →ₗ[R] F} {α' : ↥(⋀[R]^(n + 1) M) →ₗ[R] F'} (hcomm : d ∘ₗ α' = α ∘ₗ TauCeti.koszulDifferential φ n) (hα : Submodule.comap α (I • ⊤) ≤ I • ⊤) : Submodule.comap α' (I • ⊤) ≤ I • ⊤

The inductive step of Stacks 00OA. Let φ(bᵢ) ∈ I be linearly independent in I/I², let d : F' → F be a map into a free module with image in I F, and let α, α' be maps out of ⋀ⁿ M and ⋀ⁿ⁺¹ M with d ∘ α' = α ∘ d_φ, where d_φ is the Koszul differential of φ. If α is injective modulo I, i.e. α(z) ∈ I F forces z ∈ I ⋀ⁿ M, then so is α'.

theorem Module.Basis.comap_smul_top_le_of_hom_koszulComplex {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) (φ : Dual R M) {I : Ideal R} (hφ : ∀ (i : ι), φ (b i) ∈ I) (hli : LinearIndependent (R ⧸ I) fun (i : ι) => I.toCotangent ⟨φ (b i), ⋯⟩) {F : ChainComplex (ModuleCat R) ℕ} [∀ (k : ℕ), Free R ↑(F.X k)] (hF : ∀ (k : ℕ), (ModuleCat.Hom.hom (F.d (k + 1) k)).range ≤ I • ⊤) (α : TauCeti.koszulComplex φ ⟶ F) (hα : Submodule.comap (ModuleCat.Hom.hom (α.f 0)) (I • ⊤) ≤ I • ⊤) (n : ℕ) : Submodule.comap (ModuleCat.Hom.hom (α.f n)) (I • ⊤) ≤ I • ⊤

Comparison of a Koszul complex with a minimal complex (Stacks 00OA). Let φ(bᵢ) ∈ I be linearly independent in I/I², and let α : K(φ) → F be a chain map into a complex of free modules whose differentials land in I times their targets. If α is injective modulo I in degree 0, then it is injective modulo I in every degree: α(z) ∈ I Fₙ forces z ∈ I ⋀ⁿ M.