Koszul complex

Mathlib.lean

@@ -6474,6 +6474,10 @@ public import Mathlib.RingTheory.Kaehler.Basic
 public import Mathlib.RingTheory.Kaehler.JacobiZariski
 public import Mathlib.RingTheory.Kaehler.Polynomial
 public import Mathlib.RingTheory.Kaehler.TensorProduct
+public import Mathlib.RingTheory.KoszulComplex.Cocomplex
+public import Mathlib.RingTheory.KoszulComplex.Complex
+public import Mathlib.RingTheory.KoszulComplex.Dual
+public import Mathlib.RingTheory.KoszulComplex.Homotopy
 public import Mathlib.RingTheory.KrullDimension.Basic
 public import Mathlib.RingTheory.KrullDimension.Field
 public import Mathlib.RingTheory.KrullDimension.LocalRing

Mathlib/Algebra/Module/SpanRank.lean

@@ -238,6 +238,9 @@ lemma FG.finite_generators {p : Submodule R M} (hp : p.FG) :
   rw [← Cardinal.lt_aleph0_iff_set_finite, Submodule.generators_card]
   exact spanRank_finite_iff_fg.mpr hp
 
+instance finite_generators_of_isNoetherian [IsNoetherian R M] (p : Submodule R M) :
+    p.generators.Finite := FG.finite_generators FG.of_finite
+
 /-- The span of the generators equals the submodule. -/
 lemma span_generators (p : Submodule R M) : span R (generators p) = p :=
   (Classical.choose_spec (exists_span_set_card_eq_spanRank p)).2

Mathlib/CategoryTheory/Abelian/Ext.lean

@@ -57,6 +57,14 @@ def ChainComplex.linearYonedaObj {α : Type*} [AddRightCancelSemigroup α] [One
     CochainComplex (ModuleCat A) α :=
   ((((linearYoneda A C).obj Y).rightOp.mapHomologicalComplex _).obj X).unop
 
+/-- Given a cochain complex `X` and an object `Y`, this is the chain complex
+which in degree `i` consists of the module of morphisms `X.X i ⟶ Y`. -/
+@[simps! X d]
+def CochainComplex.linearYonedaObj {α : Type*} [AddRightCancelSemigroup α] [One α]
+    (X : CochainComplex C α) (A : Type*) [Ring A] [Linear A C] (Y : C) :
+    ChainComplex (ModuleCat A) α :=
+  ((((linearYoneda A C).obj Y).rightOp.mapHomologicalComplex _).obj X).unop
+
 namespace CategoryTheory
 
 namespace ProjectiveResolution

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

@@ -297,6 +297,15 @@ theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] N') :
     map n (g ∘ₗ f) = map n g ∘ₗ map n f := by
   aesop
 
+set_option backward.isDefEq.respectTransparency false in
+theorem subtype_comp_map_eq (f : M →ₗ[R] N) :
+    (Submodule.subtype _) ∘ₗ (map n f) =
+    (ExteriorAlgebra.map f).toLinearMap ∘ₗ (Submodule.subtype _) :=
+  linearMap_ext <| AlternatingMap.ext fun m ↦ (by simp)
+
+@[simp]
+theorem coe_map (f : M →ₗ[R] N) (x : ⋀[R]^n M) :
+    map n f x = ExteriorAlgebra.map f x.1 := congr($(subtype_comp_map_eq f) x)
 /-! Exactness properties of the exterior power functor. -/
 
 /-- If a linear map has a retraction, then the map it induces on exterior powers is injective. -/

Mathlib/LinearAlgebra/ExteriorPower/Basis.lean

@@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.ExteriorPower.Basic
 public import Mathlib.LinearAlgebra.ExteriorPower.Pairing
 public import Mathlib.RingTheory.Finiteness.Subalgebra
 public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+public import Mathlib.Data.Fin.Tuple.Sort
 
 /-!
 # Constructs a basis for exterior powers
@@ -183,3 +184,79 @@ lemma ιMulti_family_linearIndependent_field {I : Type*} [LinearOrder I] {v : I
   rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]
 
 end exteriorPower
+
+section
+
+universe u v
+
+variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M]
+
+namespace exteriorPower
+
+lemma span_ιMulti_orderEmbedding_of_span_eq_top {ι : Type*} [LinearOrder ι] {g : ι → M}
+    (hg : Submodule.span R (Set.range g) = ⊤) (n : ℕ) :
+    Submodule.span R (Set.range (fun (x : Fin n ↪o ι) ↦ ιMulti R _ (g ∘ x))) = ⊤ := sorry
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Given a linearly ordered basis `b : Module.Basis ι R M`, the `n`th exterior power `⋀[R]^n M`
+has a basis indexed by order embeddings `Fin n ↪o ι`. -/
+noncomputable def basis {ι : Type*} [LinearOrder ι] (b : Module.Basis ι R M) (n : ℕ) :
+    Module.Basis (Fin n ↪o ι) R (⋀[R]^n M) := by
+  let e : (Fin n ↪o ι) → ⋀[R]^n M := fun a ↦ ιMulti R n (fun i ↦ b (a i))
+  refine Module.Basis.mk (v := e) ?_ ?_
+  · refine (linearIndependent_iff).2 fun l hl ↦ Finsupp.ext fun a0 ↦ ?_
+    have h₁ (i : ι) : b.coord i (b i) = (1 : R) := by simp [Module.Basis.coord]
+    have h₀ (i j : ι) (hij : i ≠ j) : b.coord i (b j) = (0 : R) := by simp [Module.Basis.coord, hij]
+    let φ : ⋀[R]^n M →ₗ[R] R := pairingDual R M n (ιMulti R n (fun i ↦ b.coord (a0 i)))
+    have hx : φ ((Finsupp.linearCombination R e) l) = 0 := by simpa using congr(φ $hl)
+    have hx' : φ ((Finsupp.linearCombination R e) l) = l a0 := by
+      simp only [Finsupp.linearCombination_apply, map_finsuppSum, map_smul]
+      refine (Finsupp.sum_eq_single a0 ?_ fun ha0 ↦ by simp).trans ?_
+      · intro a ha hne
+        have : φ (e a) = 0 := pairingDual_apply_apply_eq_one_zero b b.coord h₀ n a0 a hne.symm
+        simp [this]
+      · have : φ (e a0) = 1 := pairingDual_apply_apply_eq_one b b.coord h₁ h₀ n a0
+        simp [this, smul_eq_mul]
+    exact hx'.symm.trans hx
+  · let S : Submodule R (⋀[R]^n M) := Submodule.span R (Set.range e)
+    have mem_S_of_injective (v : Fin n → ι) (hv : Function.Injective v) :
+        ιMulti R n (b ∘ v) ∈ S := by
+      let σ : Equiv.Perm (Fin n) := Tuple.sort v
+      have hmono : Monotone (v ∘ σ) := Tuple.monotone_sort v
+      have hinj : Function.Injective (v ∘ σ) := hv.comp σ.injective
+      let a : Fin n ↪o ι := OrderEmbedding.ofStrictMono (v ∘ σ) (hmono.strictMono_of_injective hinj)
+      have hperm : ιMulti R n (b ∘ v) = Equiv.Perm.sign σ • ιMulti R n (b ∘ a) := by
+        rw [← Equiv.Perm.sign_inv]
+        convert AlternatingMap.map_perm (ιMulti R n) (b ∘ a) σ⁻¹
+        simp [a, Function.comp_assoc]
+      rw [hperm]
+      exact S.smul_mem _ (Submodule.subset_span ⟨a, rfl⟩)
+    let ψ : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M ⧸ S) := S.mkQ.compAlternatingMap (ιMulti R n)
+    have hψ : ψ = 0 := by
+      refine Module.Basis.ext_alternating b fun v hv ↦ ?_
+      simpa [ψ] using (Submodule.Quotient.mk_eq_zero S).2 (mem_S_of_injective v hv)
+    have hrange : Set.range (ιMulti R n (M := M)) ⊆ S := by
+      rintro _ ⟨m, rfl⟩
+      exact (Submodule.Quotient.mk_eq_zero S).1 (show ψ m = 0 from by simp [hψ])
+    simpa [S, ιMulti_span R n M] using Submodule.span_le.mpr hrange
+
+end exteriorPower
+
+lemma subsingleton_of_card_generators_le {ι : Type*} [Finite ι] (g : ι → M)
+    (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) :
+    Subsingleton (⋀[R]^i M) := by
+  letI : Fintype ι := Fintype.ofFinite ι
+  letI : LinearOrder ι := LinearOrder.lift' (Fintype.equivFin ι) (Fintype.equivFin ι).injective
+  have hcard : Fintype.card ι < i := by simpa [Nat.card_eq_fintype_card] using hi
+  have hempty : IsEmpty (Fin i ↪o ι) := by
+    refine ⟨fun f ↦ ?_⟩
+    absurd f.injective
+    contrapose hcard
+    simpa using Fintype.card_le_of_injective f ‹_›
+  have hbotTop : (⊥ : Submodule R (⋀[R]^i M)) = ⊤ := by
+    rw [← exteriorPower.span_ιMulti_orderEmbedding_of_span_eq_top (R := R) (M := M) hg i]
+    convert Submodule.span_empty.symm
+    exact Set.range_eq_empty_iff.mpr hempty
+  exact (Submodule.subsingleton_iff R).mp <| (subsingleton_iff_bot_eq_top).mp hbotTop
+
+end

Mathlib/RingTheory/KoszulComplex/Cocomplex.lean

@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2026 Jingting Wang, Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jingting Wang, Nailin Guan
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Abelian
+public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower
+public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
+public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+public import Mathlib.Algebra.Module.SpanRank
+public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
+public import Mathlib.LinearAlgebra.ExteriorPower.Basis
+public import Mathlib.RingTheory.Regular.RegularSequence
+public import Mathlib.Data.Fin.Tuple.Sort
+
+/-!
+# Definition of Koszul cocomplex
+-/
+
+@[expose] public section
+
+universe u v w w'
+
+open CategoryTheory Category MonoidalCategory Limits Module
+
+section GradedAlgebra
+
+variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι]
+    [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜]
+    {i j k : ι}
+
+def GradedAlgebra.linearGMul (h : k = i + j) : 𝒜 i →ₗ[R] (𝒜 j →ₗ[R] 𝒜 k) := sorry
+
+@[simp]
+lemma GradedAlgebra.linearGMul_eq_mul (h : k = i + j) (x : 𝒜 i) (y : 𝒜 j) :
+    (GradedAlgebra.linearGMul 𝒜 h) x y = x.1 * y.1 := sorry
+
+end GradedAlgebra
+
+section
+
+variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M]
+
+set_option backward.isDefEq.respectTransparency false in
+variable {M} in
+noncomputable def koszulCocomplex (x : M) : CochainComplex (ModuleCat.{max u v} R) ℕ :=
+  CochainComplex.of
+    (ModuleCat.of R M).exteriorPower
+    (fun n ↦ ModuleCat.ofHom (GradedAlgebra.linearGMul (fun i : ℕ ↦ ⋀[R]^i M) (add_comm n 1)
+      ((exteriorPower.oneEquiv R M).symm x)))
+    (fun n ↦ by
+      simp only [← ModuleCat.ofHom_comp]
+      congr
+      refine LinearMap.ext fun x ↦ Subtype.ext ?_
+      simp only [exteriorPower.oneEquiv_symm_apply, LinearMap.coe_comp, Function.comp_apply,
+        GradedAlgebra.linearGMul_eq_mul, exteriorPower.ιMulti_apply_coe,
+        ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.ιMulti_zero_apply, mul_one, ← mul_assoc,
+        CliffordAlgebra.ι_sq_scalar, QuadraticMap.zero_apply, map_zero, zero_mul]
+      rfl)
+
+namespace koszulCocomplex
+
+noncomputable abbrev ofList (l : List R) :=
+  koszulCocomplex R l.get
+
+instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulCocomplex R x).X i) :=
+  inferInstanceAs <| Module.Free R (⋀[R]^i M)
+
+variable {M} {N : Type v} [AddCommGroup N] [Module R N]
+
+section functoriality
+
+set_option backward.isDefEq.respectTransparency false in
+noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) :
+    koszulCocomplex R x ⟶ koszulCocomplex R y :=
+  CochainComplex.ofHom _ _ _ _ _ _
+    (fun i ↦ (ModuleCat.exteriorPower.functor R i).map (ModuleCat.ofHom f))
+    (fun i ↦ by
+      refine ModuleCat.hom_ext <| LinearMap.ext fun z ↦ Subtype.ext ?_
+      simp only [ModuleCat.exteriorPower, ModuleCat.exteriorPower.functor_map,
+        ModuleCat.exteriorPower.map, ModuleCat.hom_ofHom, ModuleCat.hom_comp, LinearMap.coe_comp,
+        Function.comp_apply, GradedAlgebra.linearGMul_eq_mul, exteriorPower.coe_map,
+        exteriorPower.oneEquiv_symm_apply, map_mul, exteriorPower.ιMulti_apply_coe,
+        ExteriorAlgebra.map_apply_ιMulti]
+      congr
+      exact funext fun _ ↦ h.symm)
+
+lemma map_hom (f : M →ₗ[R] N) (x : M) (y : N) (h : f x = y) (i : ℕ) :
+    (map R f h).f i = (ModuleCat.exteriorPower.functor R i).map (ModuleCat.ofHom f) := rfl
+
+lemma map_id_refl (x : M) : koszulCocomplex.map R (M := M) .id (Eq.refl x) = 𝟙 _ := by
+  ext i x
+  simp only [map_hom, ModuleCat.ofHom_id, ModuleCat.exteriorPower.functor_map,
+    ModuleCat.exteriorPower.map, ModuleCat.hom_id, exteriorPower.map_id, HomologicalComplex.id_f,
+    LinearMap.id_coe, id_eq]
+  rfl
+
+lemma map_id (x y : M) (h : x = y) :
+    koszulCocomplex.map R (M := M) .id h = eqToHom (by rw [h]) := by
+  subst h
+  exact map_id_refl R x
+
+set_option backward.isDefEq.respectTransparency false in
+lemma map_comp {P : Type v} [AddCommGroup P] [Module R P]
+    (f : M →ₗ[R] N) (g : N →ₗ[R] P) {x : M} {y : N} {z : P} (hxy : f x = y) (hyz : g y = z) :
+    koszulCocomplex.map R f hxy ≫ koszulCocomplex.map R g hyz =
+    koszulCocomplex.map R (g ∘ₗ f) (hxy ▸ hyz : g (f x) = z) := by
+  refine HomologicalComplex.hom_ext _ _ fun i ↦ ?_
+  simp only [HomologicalComplex.comp_f, map_hom, ModuleCat.ofHom_comp, Functor.map_comp]
+
+noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) :
+    koszulCocomplex R x ≅ koszulCocomplex R y where
+  hom := koszulCocomplex.map R f h
+  inv := koszulCocomplex.map R f.symm (f.injective (by simpa using h.symm))
+  hom_inv_id := by
+    simp only [map_comp, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm,
+      LinearEquiv.refl_toLinearMap]
+    exact map_id_refl R x
+  inv_hom_id := by
+    simp only [map_comp, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self,
+      LinearEquiv.refl_toLinearMap]
+    exact map_id_refl R y
+
+end functoriality
+
+section specialX
+
+noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder ι] (x : M)
+    (b : Basis ι R M) : (koszulCocomplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry
+
+noncomputable def topXLinearEquivOfBasisOfList (l : List R) :
+    (ofList R l).X l.length ≃ₗ[R] R := by
+  have : l.length = Nat.card (Fin l.length) := by simp
+  rw [this]
+  exact topXLinearEquivOfBasis R l.get (Pi.basisFun R (Fin l.length))
+
+set_option backward.isDefEq.respectTransparency false in
+lemma X_isZero_of_card_generators_le (x : M) {ι : Type*} [Finite ι] (g : ι → M)
+    (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) :
+    IsZero ((koszulCocomplex R x).X i) := by
+  have hIsZero : IsZero (ModuleCat.of R (⋀[R]^i M)) := by
+    apply ModuleCat.isZero_of_iff_subsingleton.mpr
+    exact subsingleton_of_card_generators_le R M g hg i hi
+  simpa [koszulCocomplex, ModuleCat.exteriorPower] using hIsZero
+
+lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) :
+    IsZero ((koszulCocomplex.ofList R l).X i) :=
+  X_isZero_of_card_generators_le R l.get
+  (Pi.basisFun R (Fin l.length)) (Pi.basisFun R (Fin l.length)).span_eq i
+  (by simpa [Nat.card_eq_fintype_card] using hi)
+
+end specialX
+
+section Htop
+
+noncomputable def topHomologyLinearEquiv (l : List R) :
+    (ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry
+
+end Htop
+
+section regular
+
+open RingTheory.Sequence
+
+lemma exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs)
+    (i : ℕ) (lt : i < rs.length) : (koszulCocomplex.ofList R rs).ExactAt i := by
+  sorry
+
+theorem exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs)
+    (i : ℕ) (lt : i ≠ rs.length) : (koszulCocomplex.ofList R rs).ExactAt i := by
+  sorry
+
+end regular
+
+section change_generators
+
+lemma nonempty_linearEquiv_of_minimal_generators (I : Ideal R) (hI : I ≤ Ring.jacobson R)
+    (l l' : List R) (hl : Ideal.ofList l = I) (hl' : Ideal.ofList l' = I)
+    (hl_min : l.length = I.spanFinrank) (hl'_min : l'.length = I.spanFinrank) :
+  ∃ e : (Fin l.length → R) ≃ₗ[R] (Fin l'.length → R), e l.get = l'.get := sorry
+
+theorem nonempty_iso_of_minimal_generators [IsLocalRing R]
+    {I : Ideal R} {l l' : List R}
+    (hl : Ideal.ofList l = I) (hl' : Ideal.ofList l' = I)
+    (hl_min : l.length = I.spanFinrank) (hl'_min : l'.length = I.spanFinrank) :
+    Nonempty <| ofList R l ≅ ofList R l' := by
+  have hI : I ≤ Ring.jacobson R := sorry
+  obtain ⟨e, h⟩ := nonempty_linearEquiv_of_minimal_generators R I hI l l' hl hl' hl_min hl'_min
+  exact ⟨isoOfEquiv R e h⟩
+
+theorem nonempty_iso_of_minimal_generators'
+    [IsNoetherianRing R] [IsLocalRing R] {I : Ideal R} {l : List R}
+    (eq : Ideal.ofList l = I) (min : l.length = I.spanFinrank) :
+    Nonempty <| ofList R I.finite_generators_of_isNoetherian.toFinset.toList ≅ ofList R l := by
+  refine nonempty_iso_of_minimal_generators R ?_ eq ?_ min
+  · simp only [Ideal.ofList, Finset.mem_toList, Set.Finite.mem_toFinset, Set.setOf_mem_eq]
+    exact I.span_generators
+  · simp only [Finset.length_toList, ← Set.ncard_eq_toFinset_card _ _]
+    exact Submodule.FG.generators_ncard Submodule.FG.of_finite
+
+end change_generators
+
+section basechange
+
+variable (S : Type (max u v)) [CommRing S] (f : R →+* S)
+
+instance (T : Type v) [CommRing T] (g : R →+* T) :
+    (ModuleCat.extendScalars.{u, v, u} g).Additive where
+  map_add {X Y a b} := by
+    simp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
+      ModuleCat.hom_add, LinearMap.baseChange_add]
+    rfl
+
+open TensorProduct in
+noncomputable def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') :
+    ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex _).obj (ofList R l) := by
+  refine HomologicalComplex.Hom.isoOfComponents
+    (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_)
+  · sorry
+  · sorry
+
+end basechange
+
+end koszulCocomplex