From 78f06712b9f7938fb1256f5a627fb8efed60096b Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Sun, 25 Jan 2026 13:38:51 +0800 Subject: [PATCH 01/34] initialize --- Mathlib.lean | 1 + Mathlib/RingTheory/KoszulComplex/Defs.lean | 59 ++++++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 Mathlib/RingTheory/KoszulComplex/Defs.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5145dc48a8497e..89e66670af7ec2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6111,6 +6111,7 @@ 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.Defs public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.LocalRing diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean new file mode 100644 index 00000000000000..bb0f8eb674a6dd --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Jingting Wang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jingting Wang +-/ +module + +public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading +public import Mathlib.Algebra.Homology.HomologicalComplex +public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower +public import Mathlib.Algebra.Homology.Monoidal + +/-! +# Definition of Koszul complex +-/ + +@[expose] public section + +universe u v + +open CategoryTheory Category MonoidalCategory + +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] + +abbrev ExteriorAlgebra.ι₁ : M →ₗ[R] ⋀[R]^1 M := + (ExteriorAlgebra.ι R).codRestrict _ (fun c ↦ by + rw [exteriorPower, Submodule.pow_one] + exact ⟨c, rfl⟩) + +variable {M} in +def koszulComplex (x : M) : HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := + CochainComplex.of + (ModuleCat.of R M).exteriorPower + (fun n ↦ ModuleCat.ofHom (GradedAlgebra.linearGMul (fun i : ℕ ↦ ⋀[R]^i M) (add_comm n 1) + (ExteriorAlgebra.ι₁ R M x))) + (fun n ↦ by + simp only [← ModuleCat.ofHom_comp] + congr + refine LinearMap.ext fun x ↦ Subtype.ext ?_ + simp only [LinearMap.coe_comp, Function.comp_apply, GradedAlgebra.linearGMul_eq_mul, + LinearMap.codRestrict_apply, ← mul_assoc, CliffordAlgebra.ι_sq_scalar, + QuadraticMap.zero_apply, map_zero, zero_mul] + rfl) From db72fc3e9184efb241e43e9a118abdc3804246bc Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Sun, 25 Jan 2026 15:15:02 +0800 Subject: [PATCH 02/34] add koszulComplex.map --- .../LinearAlgebra/ExteriorPower/Basic.lean | 5 ++ Mathlib/RingTheory/KoszulComplex/Defs.lean | 51 +++++++++++++++++-- 2 files changed, 51 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean index 074f6e203d6eff..d198e0922e7946 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean @@ -262,6 +262,11 @@ theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] N') : map n (g ∘ₗ f) = map n g ∘ₗ map n f := by aesop +@[simp] +theorem coe_map (f : M →ₗ[R] N) (x : ⋀[R]^n M) : + map n f x = ExteriorAlgebra.map f x.1 := by + sorry + /-! Linear equivalences in degrees 0 and 1. -/ variable (R M) in diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index bb0f8eb674a6dd..58c93dea664f8b 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -5,6 +5,7 @@ Authors: Jingting Wang -/ module +public import Mathlib.LinearAlgebra.ExteriorPower.Basic public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.Algebra.Homology.HomologicalComplex public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower @@ -44,16 +45,56 @@ abbrev ExteriorAlgebra.ι₁ : M →ₗ[R] ⋀[R]^1 M := exact ⟨c, rfl⟩) variable {M} in -def koszulComplex (x : M) : HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := +noncomputable def koszulComplex (x : M) : + HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := CochainComplex.of (ModuleCat.of R M).exteriorPower (fun n ↦ ModuleCat.ofHom (GradedAlgebra.linearGMul (fun i : ℕ ↦ ⋀[R]^i M) (add_comm n 1) - (ExteriorAlgebra.ι₁ R M x))) + ((exteriorPower.oneEquiv R M).symm x))) (fun n ↦ by simp only [← ModuleCat.ofHom_comp] congr refine LinearMap.ext fun x ↦ Subtype.ext ?_ - simp only [LinearMap.coe_comp, Function.comp_apply, GradedAlgebra.linearGMul_eq_mul, - LinearMap.codRestrict_apply, ← mul_assoc, CliffordAlgebra.ι_sq_scalar, - QuadraticMap.zero_apply, map_zero, zero_mul] + 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 koszulComplex + +variable {M} {N : Type v} [AddCommGroup N] [Module R N] + +noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : + koszulComplex R x ⟶ koszulComplex 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 (x y : M) (h : x = y) : koszulComplex.map R (M := M) .id h = eqToHom (by rw [h]) := by + subst h + ext i x + simp only [map_hom, ModuleCat.ofHom_id, ModuleCat.exteriorPower.functor_map, + ModuleCat.exteriorPower.map, ModuleCat.hom_id, exteriorPower.map_id, eqToHom_refl, + HomologicalComplex.id_f, LinearMap.id_coe, id_eq] + rfl + +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) : + koszulComplex.map R f hxy ≫ koszulComplex.map R g hyz = + koszulComplex.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] + +end koszulComplex From 5d46837dc023476054a6c653fdf2229e68eff098 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Sun, 25 Jan 2026 15:34:54 +0800 Subject: [PATCH 03/34] prove basic lemma --- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean index d198e0922e7946..e16c4e808bf8a4 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean @@ -262,10 +262,14 @@ theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] N') : map n (g ∘ₗ f) = map n g ∘ₗ map n f := by aesop +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 := by - sorry + map n f x = ExteriorAlgebra.map f x.1 := congr($(subtype_comp_map_eq f) x) /-! Linear equivalences in degrees 0 and 1. -/ From 3ad5b32597caa1c05f91c6517bb66bd5b9ddad64 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 14:03:22 +0800 Subject: [PATCH 04/34] add a new definition --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 58c93dea664f8b..6ff729b644864a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -10,6 +10,11 @@ public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.Algebra.Homology.HomologicalComplex public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower public import Mathlib.Algebra.Homology.Monoidal +public import Mathlib.Algebra.Homology.ShortComplex.Abelian +public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex +public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.RingTheory.Regular.RegularSequence +public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic /-! # Definition of Koszul complex @@ -17,7 +22,7 @@ public import Mathlib.Algebra.Homology.Monoidal @[expose] public section -universe u v +universe u v w w' open CategoryTheory Category MonoidalCategory @@ -35,6 +40,15 @@ lemma GradedAlgebra.linearGMul_eq_mul (h : k = i + j) (x : 𝒜 i) (y : 𝒜 j) end GradedAlgebra +section ModuleCat + +variable {R : Type u} [CommRing R] + +def ModuleCat.tensorFunctor (M : ModuleCat.{v} R) [Small.{w'} M] [UnivLE.{w, w'}] : + ModuleCat.{w} R ⥤ ModuleCat.{w'} R := sorry + +end ModuleCat + section variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] @@ -97,4 +111,10 @@ lemma map_comp {P : Type v} [AddCommGroup P] [Module R P] refine HomologicalComplex.hom_ext _ _ fun i ↦ ?_ simp only [HomologicalComplex.comp_f, map_hom, ModuleCat.ofHom_comp, Functor.map_comp] +noncomputable abbrev ofList (l : List R) := + koszulComplex R l.get + +def topHomologyLinearEquiv (l : List R) : + (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + end koszulComplex From df8b9d6fbf9190f1d1e53e1f1564cc2d6af90bc7 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 26 Jan 2026 15:54:52 +0800 Subject: [PATCH 05/34] add API for CI --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 48 +++++++++++++++++++++- 1 file changed, 46 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 6ff729b644864a..2ae32940820b02 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -7,12 +7,14 @@ module public import Mathlib.LinearAlgebra.ExteriorPower.Basic public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading -public import Mathlib.Algebra.Homology.HomologicalComplex +public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower +public import Mathlib.Algebra.Homology.HomologicalComplex public import Mathlib.Algebra.Homology.Monoidal public import Mathlib.Algebra.Homology.ShortComplex.Abelian public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex -public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.RingTheory.Regular.RegularSequence public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic @@ -118,3 +120,45 @@ def topHomologyLinearEquiv (l : List R) : (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry end koszulComplex + +section changegenerators + +variable [IsNoetherianRing R] [IsLocalRing R] + +def koszulComplex.iso_of_minimal_generators {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) + (min : l.length = I.spanFinrank) : + letI : Fintype I.generators := + (Submodule.FG.finite_generators I.fg_of_isNoetherianRing).fintype + koszulComplex.ofList R I.generators.toFinset.toList ≅ koszulComplex.ofList R l := + sorry + +end changegenerators + +section basechange + +variable (S : Type u) [CommRing S] (f : R →+* S) + +def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + koszulComplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex + (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := + sorry + +end basechange + +section IsRegular + +open RingTheory.Sequence + +lemma koszulComplex.exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i < rs.length) : (koszulComplex.ofList R rs).ExactAt i := by + sorry + +theorem koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i ≠ rs.length) : (koszulComplex.ofList R rs).ExactAt i := by + sorry + +lemma koszulComplex.free_of_free (M : Type u) [AddCommGroup M] [Module R M] [Module.Free R M] + (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := by + sorry + +end IsRegular From f4d2c4908d7693e7a18db7b3da171ee8ace6b12f Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 26 Jan 2026 16:04:39 +0800 Subject: [PATCH 06/34] Update Defs.lean --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 2ae32940820b02..cffb66baffb5b8 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -121,6 +121,14 @@ def topHomologyLinearEquiv (l : List R) : end koszulComplex +section homologyannihilator + +lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) + (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by + sorry + +end homologyannihilator + section changegenerators variable [IsNoetherianRing R] [IsLocalRing R] From 47984177fc90293e9779b22b3da0a4c4e5787463 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 16:30:55 +0800 Subject: [PATCH 07/34] basis of exteriorPower --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 103 +++++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 6ff729b644864a..36b80491b8f233 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -6,6 +6,7 @@ Authors: Jingting Wang module public import Mathlib.LinearAlgebra.ExteriorPower.Basic +public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.Algebra.Homology.HomologicalComplex public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower @@ -15,6 +16,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex public import Mathlib.Algebra.Category.ModuleCat.Abelian public import Mathlib.RingTheory.Regular.RegularSequence public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic +public import Mathlib.Data.Fin.Tuple.Sort /-! # Definition of Koszul complex @@ -58,6 +60,107 @@ abbrev ExteriorAlgebra.ι₁ : M →ₗ[R] ⋀[R]^1 M := rw [exteriorPower, Submodule.pow_one] exact ⟨c, rfl⟩) +namespace exteriorPower + +variable {ι : Type*} [LinearOrder ι] + +/-- 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 (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)) + let S : Submodule R (⋀[R]^n M) := Submodule.span R (Set.range e) + have h₁ : ∀ i : ι, b.coord i (b i) = (1 : R) := by + intro i + simp [Module.Basis.coord] + have h₀ : ∀ ⦃i j : ι⦄, i ≠ j → b.coord i (b j) = (0 : R) := by + intro i j hij + simp [Module.Basis.coord, hij] + have mem_S_of_injective (v : Fin n → ι) (hv : Function.Injective v) : + ιMulti R n (fun i ↦ b (v i)) ∈ 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 (fun i ↦ b (v i)) = Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by + have hperm' : + ιMulti R n (fun i ↦ b (a ((Equiv.symm σ) i))) = + Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by + simpa using + (AlternatingMap.map_perm (g := ιMulti R n) (v := fun i ↦ b (a i)) + (σ := (σ⁻¹ : Equiv.Perm (Fin n)))) + have hcomp : (fun i ↦ b (a ((Equiv.symm σ) i))) = fun i ↦ b (v i) := by + ext i + simp [a, Function.comp] + simpa [hcomp] using hperm' + rw [hperm] + refine S.smul_mem _ (Submodule.subset_span ?_) + exact ⟨a, rfl⟩ + have hli : LinearIndependent R e := by + refine (linearIndependent_iff).2 ?_ + intro l hl + ext a0 + 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 congrArg (fun x ↦ φ x) hl + have hx' : φ ((Finsupp.linearCombination R e) l) = l a0 := by + simp only [Finsupp.linearCombination_apply] + simp_rw [map_finsuppSum, map_smul] + refine (Finsupp.sum_eq_single a0 ?_ ?_).trans ?_ + · intro a ha hne + have : φ (e a) = (0 : R) := by + dsimp [φ, e] + exact + pairingDual_apply_apply_eq_one_zero (R := R) (M := M) (ι := ι) (x := b) + (f := fun i ↦ b.coord i) (n := n) (h₀ := by + intro i j hij; exact h₀ hij) a0 a hne.symm + simp [this] + · intro ha0 + simp + · have : φ (e a0) = 1 := by + dsimp [φ, e] + exact + pairingDual_apply_apply_eq_one (R := R) (M := M) (ι := ι) (x := b) + (f := fun i ↦ b.coord i) h₁ (by + intro i j hij; exact h₀ hij) n a0 + simp [this, smul_eq_mul] + exact by simpa [hx', Finsupp.zero_apply] using hx + have hsp : (⊤ : Submodule R (⋀[R]^n M)) ≤ S := by + let π : ⋀[R]^n M →ₗ[R] (⋀[R]^n M ⧸ S) := S.mkQ + let ψ : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M ⧸ S) := π.compAlternatingMap (ιMulti R n) + have hψ : ψ = 0 := by + refine (Module.Basis.ext_alternating (ι := Fin n) (e := b) (f := ψ) (g := 0) ?_) + intro v hv + have hvmem : ιMulti R n (fun i ↦ b (v i)) ∈ S := + mem_S_of_injective v hv + have : π (ιMulti R n (fun i ↦ b (v i))) = 0 := by + simpa [π, Submodule.mkQ_apply] using (Submodule.Quotient.mk_eq_zero S).2 hvmem + simpa [ψ, Function.comp] using this + have hrange : Set.range (ιMulti R n (M := M)) ⊆ S := by + rintro _ ⟨m, rfl⟩ + have : ψ m = 0 := by + simp [hψ] + have : π (ιMulti R n m) = 0 := by + simpa [ψ] using this + have : Submodule.Quotient.mk (p := S) (ιMulti R n m) = 0 := by + simpa [π, Submodule.mkQ_apply] using this + exact (Submodule.Quotient.mk_eq_zero S).1 this + have hspanle : Submodule.span R (Set.range (ιMulti R n (M := M))) ≤ S := + Submodule.span_le.2 hrange + simpa [S, ιMulti_span (R := R) (n := n) (M := M)] using hspanle + exact Module.Basis.mk hli (by simpa [S] using hsp) + +end exteriorPower + +theorem Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by + classical + let ι := Module.Free.ChooseBasisIndex R M + letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) + exact + Module.Free.of_basis + (exteriorPower.basis (R := R) (M := M) (ι := ι) (Module.Free.chooseBasis R M) n) + variable {M} in noncomputable def koszulComplex (x : M) : HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := From e4c054096b4cb3e736075d5fcebfa04d0d410c4b Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 16:32:33 +0800 Subject: [PATCH 08/34] easy proof --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 75f734fc807fef..fb01eade21bc45 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -155,7 +155,7 @@ noncomputable def basis (b : Module.Basis ι R M) (n : ℕ) : end exteriorPower -theorem Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by +instance Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by classical let ι := Module.Free.ChooseBasisIndex R M letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) @@ -269,7 +269,7 @@ theorem koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsR sorry lemma koszulComplex.free_of_free (M : Type u) [AddCommGroup M] [Module R M] [Module.Free R M] - (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := by - sorry + (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := + inferInstanceAs <| Module.Free R (⋀[R]^i M) end IsRegular From c67ea48186e4201904defd03078f0c7d7d875bd7 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 16:40:09 +0800 Subject: [PATCH 09/34] move file --- Mathlib.lean | 1 + Mathlib/RingTheory/KoszulComplex/Basic.lean | 72 +++++++++++++++++++++ Mathlib/RingTheory/KoszulComplex/Defs.lean | 55 +--------------- 3 files changed, 76 insertions(+), 52 deletions(-) create mode 100644 Mathlib/RingTheory/KoszulComplex/Basic.lean diff --git a/Mathlib.lean b/Mathlib.lean index 89e66670af7ec2..2f50bbd7df4794 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6111,6 +6111,7 @@ 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.Basic public import Mathlib.RingTheory.KoszulComplex.Defs public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.KrullDimension.Field diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean new file mode 100644 index 00000000000000..cf21f2ea158622 --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -0,0 +1,72 @@ +/- +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.RingTheory.KoszulComplex.Defs + +/-! +# Definition of Koszul complex +-/ + +@[expose] public section + +universe u v + +variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] + +section homology_annihilator + +lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) + (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by + sorry + +lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : + Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList R l).homology i) := by + sorry + +end homology_annihilator + +section change_generators + +variable [IsNoetherianRing R] [IsLocalRing R] + +def koszulComplex.iso_of_minimal_generators {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) + (min : l.length = I.spanFinrank) : + letI : Fintype I.generators := + (Submodule.FG.finite_generators I.fg_of_isNoetherianRing).fintype + koszulComplex.ofList R I.generators.toFinset.toList ≅ koszulComplex.ofList R l := + sorry + +end change_generators + +section basechange + +variable (S : Type u) [CommRing S] (f : R →+* S) + +def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + koszulComplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex + (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := + sorry + +end basechange + +section IsRegular + +open RingTheory.Sequence + +lemma koszulComplex.exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i < rs.length) : (koszulComplex.ofList R rs).ExactAt i := by + sorry + +theorem koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i ≠ rs.length) : (koszulComplex.ofList R rs).ExactAt i := by + sorry + +lemma koszulComplex.free_of_free (M : Type u) [AddCommGroup M] [Module R M] [Module.Free R M] + (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := + inferInstanceAs <| Module.Free R (⋀[R]^i M) + +end IsRegular diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index fb01eade21bc45..a9637affe84071 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Jingting Wang. All rights reserved. +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 +Authors: Jingting Wang, Nailin Guan -/ module @@ -66,6 +66,7 @@ namespace exteriorPower variable {ι : Type*} [LinearOrder ι] +-- to be golfed /-- 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 (b : Module.Basis ι R M) (n : ℕ) : @@ -223,53 +224,3 @@ def topHomologyLinearEquiv (l : List R) : (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry end koszulComplex - -section homologyannihilator - -lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) - (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by - sorry - -end homologyannihilator - -section changegenerators - -variable [IsNoetherianRing R] [IsLocalRing R] - -def koszulComplex.iso_of_minimal_generators {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) - (min : l.length = I.spanFinrank) : - letI : Fintype I.generators := - (Submodule.FG.finite_generators I.fg_of_isNoetherianRing).fintype - koszulComplex.ofList R I.generators.toFinset.toList ≅ koszulComplex.ofList R l := - sorry - -end changegenerators - -section basechange - -variable (S : Type u) [CommRing S] (f : R →+* S) - -def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : - koszulComplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex - (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := - sorry - -end basechange - -section IsRegular - -open RingTheory.Sequence - -lemma koszulComplex.exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) - (i : ℕ) (lt : i < rs.length) : (koszulComplex.ofList R rs).ExactAt i := by - sorry - -theorem koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) - (i : ℕ) (lt : i ≠ rs.length) : (koszulComplex.ofList R rs).ExactAt i := by - sorry - -lemma koszulComplex.free_of_free (M : Type u) [AddCommGroup M] [Module R M] [Module.Free R M] - (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := - inferInstanceAs <| Module.Free R (⋀[R]^i M) - -end IsRegular From afc04103de96df2f7a5cfe00c6d969e8daba45d6 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 16:57:55 +0800 Subject: [PATCH 10/34] easy proof --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index cf21f2ea158622..30965361591971 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -25,7 +25,13 @@ lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Modu lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList R l).homology i) := by - sorry + intro r hr + have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] + rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ + let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c + have hφ : φ l.get = r := by + simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] + exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i end homology_annihilator From 6235c1eb87eb3ded12b2152f7c6a91709cedc81a Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 17:23:25 +0800 Subject: [PATCH 11/34] add koszulComplex.isoOfEquiv --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 24 ++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index a9637affe84071..e79245c384a62a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -202,14 +202,17 @@ noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : 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 (x y : M) (h : x = y) : koszulComplex.map R (M := M) .id h = eqToHom (by rw [h]) := by - subst h +lemma map_id_refl (x : M) : koszulComplex.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, eqToHom_refl, - HomologicalComplex.id_f, LinearMap.id_coe, id_eq] + 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) : koszulComplex.map R (M := M) .id h = eqToHom (by rw [h]) := by + subst h + exact map_id_refl R x + 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) : koszulComplex.map R f hxy ≫ koszulComplex.map R g hyz = @@ -217,6 +220,19 @@ lemma map_comp {P : Type v} [AddCommGroup P] [Module R P] 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) : + koszulComplex R x ≅ koszulComplex R y where + hom := koszulComplex.map R f h + inv := koszulComplex.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 + noncomputable abbrev ofList (l : List R) := koszulComplex R l.get From 800e51b04667f084e109e660de09d0084c75cddf Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Mon, 26 Jan 2026 17:32:32 +0800 Subject: [PATCH 12/34] refactor lemma --- Mathlib/Algebra/Module/SpanRank.lean | 3 +++ Mathlib/RingTheory/KoszulComplex/Basic.lean | 12 ++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index f894195d05c718..bc96bc2fa6d18b 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -222,6 +222,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 diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index 30965361591971..37d3fd53e32e74 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -39,12 +39,12 @@ section change_generators variable [IsNoetherianRing R] [IsLocalRing R] -def koszulComplex.iso_of_minimal_generators {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) - (min : l.length = I.spanFinrank) : - letI : Fintype I.generators := - (Submodule.FG.finite_generators I.fg_of_isNoetherianRing).fintype - koszulComplex.ofList R I.generators.toFinset.toList ≅ koszulComplex.ofList R l := - sorry +noncomputable def koszulComplex.isoOfMinimalGenerators {I : Ideal R} {l : List R} + (eq : Ideal.ofList l = I) (min : l.length = I.spanFinrank) : + koszulComplex.ofList R I.finite_generators_of_isNoetherian.toFinset.toList ≅ + koszulComplex.ofList R l := by + refine isoOfEquiv R ?_ ?_ + all_goals sorry end change_generators From 6cb4623d6be63665891ad47f9016b7b590f5b774 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Tue, 27 Jan 2026 10:43:50 +0800 Subject: [PATCH 13/34] finish refactor code about basis of exterior power --- .../LinearAlgebra/ExteriorPower/Basis.lean | 83 +++++++++++++ Mathlib/RingTheory/KoszulComplex/Defs.lean | 111 +----------------- 2 files changed, 84 insertions(+), 110 deletions(-) create mode 100644 Mathlib/LinearAlgebra/ExteriorPower/Basis.lean diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean new file mode 100644 index 00000000000000..3ba75aaa39858a --- /dev/null +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Jingting Wang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jingting Wang +-/ + +module + +public import Mathlib.LinearAlgebra.ExteriorPower.Basic +public import Mathlib.LinearAlgebra.ExteriorPower.Pairing +public import Mathlib.Data.Fin.Tuple.Sort + +/-! +# Basis of exterior power + +In this file we construct a basis of the exterior power `⋀[R]^n M` given a linearly ordered +basis of `M`, and deduce that exterior powers of free modules are free. +-/ + +@[expose] public section + +universe u v + +variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] + +namespace exteriorPower + +/-- 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) ?_ ?_ + · have h₁ : ∀ i : ι, b.coord i (b i) = (1 : R) := by + intro i + simp [Module.Basis.coord] + have h₀ : ∀ i j : ι, i ≠ j → b.coord i (b j) = (0 : R) := by + intro i j hij + simp [Module.Basis.coord, hij] + refine (linearIndependent_iff).2 fun l hl ↦ Finsupp.ext fun a0 ↦ ?_ + 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 (fun i ↦ b (v i)) ∈ 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 (fun i ↦ b (v i)) = Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by + rw [← Equiv.Perm.sign_inv] + convert (AlternatingMap.map_perm (g := ιMulti R n) (v := fun i ↦ b (a i)) + (σ := (σ⁻¹ : Equiv.Perm (Fin n)))) + simp [a] + 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 (ι := Fin n) (e := b) (f := ψ) (g := 0) 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 := R) (n := n) (M := M)] using Submodule.span_le.mpr hrange + +end exteriorPower + +instance Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by + classical + let ι := Module.Free.ChooseBasisIndex R M + letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) + exact Module.Free.of_basis + (exteriorPower.basis (R := R) (M := M) (ι := ι) (Module.Free.chooseBasis R M) n) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index e79245c384a62a..5f06bd38384416 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -5,8 +5,7 @@ Authors: Jingting Wang, Nailin Guan -/ module -public import Mathlib.LinearAlgebra.ExteriorPower.Basic -public import Mathlib.LinearAlgebra.ExteriorPower.Pairing +public import Mathlib.LinearAlgebra.ExteriorPower.Basis public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.Algebra.Category.ModuleCat.Abelian public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings @@ -18,7 +17,6 @@ public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex public import Mathlib.Algebra.Module.SpanRank public import Mathlib.RingTheory.Regular.RegularSequence public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic -public import Mathlib.Data.Fin.Tuple.Sort /-! # Definition of Koszul complex @@ -57,113 +55,6 @@ section variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] -abbrev ExteriorAlgebra.ι₁ : M →ₗ[R] ⋀[R]^1 M := - (ExteriorAlgebra.ι R).codRestrict _ (fun c ↦ by - rw [exteriorPower, Submodule.pow_one] - exact ⟨c, rfl⟩) - -namespace exteriorPower - -variable {ι : Type*} [LinearOrder ι] - --- to be golfed -/-- 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 (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)) - let S : Submodule R (⋀[R]^n M) := Submodule.span R (Set.range e) - have h₁ : ∀ i : ι, b.coord i (b i) = (1 : R) := by - intro i - simp [Module.Basis.coord] - have h₀ : ∀ ⦃i j : ι⦄, i ≠ j → b.coord i (b j) = (0 : R) := by - intro i j hij - simp [Module.Basis.coord, hij] - have mem_S_of_injective (v : Fin n → ι) (hv : Function.Injective v) : - ιMulti R n (fun i ↦ b (v i)) ∈ 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 (fun i ↦ b (v i)) = Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by - have hperm' : - ιMulti R n (fun i ↦ b (a ((Equiv.symm σ) i))) = - Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by - simpa using - (AlternatingMap.map_perm (g := ιMulti R n) (v := fun i ↦ b (a i)) - (σ := (σ⁻¹ : Equiv.Perm (Fin n)))) - have hcomp : (fun i ↦ b (a ((Equiv.symm σ) i))) = fun i ↦ b (v i) := by - ext i - simp [a, Function.comp] - simpa [hcomp] using hperm' - rw [hperm] - refine S.smul_mem _ (Submodule.subset_span ?_) - exact ⟨a, rfl⟩ - have hli : LinearIndependent R e := by - refine (linearIndependent_iff).2 ?_ - intro l hl - ext a0 - 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 congrArg (fun x ↦ φ x) hl - have hx' : φ ((Finsupp.linearCombination R e) l) = l a0 := by - simp only [Finsupp.linearCombination_apply] - simp_rw [map_finsuppSum, map_smul] - refine (Finsupp.sum_eq_single a0 ?_ ?_).trans ?_ - · intro a ha hne - have : φ (e a) = (0 : R) := by - dsimp [φ, e] - exact - pairingDual_apply_apply_eq_one_zero (R := R) (M := M) (ι := ι) (x := b) - (f := fun i ↦ b.coord i) (n := n) (h₀ := by - intro i j hij; exact h₀ hij) a0 a hne.symm - simp [this] - · intro ha0 - simp - · have : φ (e a0) = 1 := by - dsimp [φ, e] - exact - pairingDual_apply_apply_eq_one (R := R) (M := M) (ι := ι) (x := b) - (f := fun i ↦ b.coord i) h₁ (by - intro i j hij; exact h₀ hij) n a0 - simp [this, smul_eq_mul] - exact by simpa [hx', Finsupp.zero_apply] using hx - have hsp : (⊤ : Submodule R (⋀[R]^n M)) ≤ S := by - let π : ⋀[R]^n M →ₗ[R] (⋀[R]^n M ⧸ S) := S.mkQ - let ψ : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M ⧸ S) := π.compAlternatingMap (ιMulti R n) - have hψ : ψ = 0 := by - refine (Module.Basis.ext_alternating (ι := Fin n) (e := b) (f := ψ) (g := 0) ?_) - intro v hv - have hvmem : ιMulti R n (fun i ↦ b (v i)) ∈ S := - mem_S_of_injective v hv - have : π (ιMulti R n (fun i ↦ b (v i))) = 0 := by - simpa [π, Submodule.mkQ_apply] using (Submodule.Quotient.mk_eq_zero S).2 hvmem - simpa [ψ, Function.comp] using this - have hrange : Set.range (ιMulti R n (M := M)) ⊆ S := by - rintro _ ⟨m, rfl⟩ - have : ψ m = 0 := by - simp [hψ] - have : π (ιMulti R n m) = 0 := by - simpa [ψ] using this - have : Submodule.Quotient.mk (p := S) (ιMulti R n m) = 0 := by - simpa [π, Submodule.mkQ_apply] using this - exact (Submodule.Quotient.mk_eq_zero S).1 this - have hspanle : Submodule.span R (Set.range (ιMulti R n (M := M))) ≤ S := - Submodule.span_le.2 hrange - simpa [S, ιMulti_span (R := R) (n := n) (M := M)] using hspanle - exact Module.Basis.mk hli (by simpa [S] using hsp) - -end exteriorPower - -instance Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by - classical - let ι := Module.Free.ChooseBasisIndex R M - letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) - exact - Module.Free.of_basis - (exteriorPower.basis (R := R) (M := M) (ι := ι) (Module.Free.chooseBasis R M) n) - variable {M} in noncomputable def koszulComplex (x : M) : HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := From 2622aa42b0654bd9198901e91f6351712781fba3 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Tue, 27 Jan 2026 10:48:31 +0800 Subject: [PATCH 14/34] golf proof --- .../LinearAlgebra/ExteriorPower/Basis.lean | 24 +++++++------------ 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 3ba75aaa39858a..0071be874e87fb 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -31,13 +31,9 @@ noncomputable def basis {ι : Type*} [LinearOrder ι] (b : Module.Basis ι R M) 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) ?_ ?_ - · have h₁ : ∀ i : ι, b.coord i (b i) = (1 : R) := by - intro i - simp [Module.Basis.coord] - have h₀ : ∀ i j : ι, i ≠ j → b.coord i (b j) = (0 : R) := by - intro i j hij - simp [Module.Basis.coord, hij] - refine (linearIndependent_iff).2 fun l hl ↦ Finsupp.ext fun a0 ↦ ?_ + · 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 @@ -51,27 +47,25 @@ noncomputable def basis {ι : Type*} [LinearOrder ι] (b : Module.Basis ι R M) 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 (fun i ↦ b (v i)) ∈ S := by + ι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 (fun i ↦ b (v i)) = Equiv.Perm.sign σ • ιMulti R n (fun i ↦ b (a i)) := by + 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 (g := ιMulti R n) (v := fun i ↦ b (a i)) - (σ := (σ⁻¹ : Equiv.Perm (Fin n)))) - simp [a] + 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 (ι := Fin n) (e := b) (f := ψ) (g := 0) fun v hv ↦ ?_) + 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 := R) (n := n) (M := M)] using Submodule.span_le.mpr hrange + simpa [S, ιMulti_span R n M] using Submodule.span_le.mpr hrange end exteriorPower From 41b0c30764c4d69104f5136a737c5146ad3068a5 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Tue, 27 Jan 2026 11:07:19 +0800 Subject: [PATCH 15/34] add note (so that we dont PR ExteriorPower.Basis) --- Mathlib/LinearAlgebra/ExteriorPower/Basis.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 0071be874e87fb..4de147be3d37e9 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -15,6 +15,8 @@ public import Mathlib.Data.Fin.Tuple.Sort In this file we construct a basis of the exterior power `⋀[R]^n M` given a linearly ordered basis of `M`, and deduce that exterior powers of free modules are free. + +Note: Joel Riou is PRing this at #18771 -/ @[expose] public section From 42ab1de0f14081f646bc17f84e9983ec37660162 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Tue, 27 Jan 2026 12:40:59 +0800 Subject: [PATCH 16/34] add easy lemma --- .../LinearAlgebra/ExteriorPower/Basis.lean | 4 +++ Mathlib/RingTheory/KoszulComplex/Basic.lean | 4 --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 33 ++++++++++++++++++- 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 4de147be3d37e9..34fae2c32af591 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -27,6 +27,10 @@ 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 + /-- 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 : ℕ) : diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index 37d3fd53e32e74..5da8d094a9091a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -71,8 +71,4 @@ theorem koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsR (i : ℕ) (lt : i ≠ rs.length) : (koszulComplex.ofList R rs).ExactAt i := by sorry -lemma koszulComplex.free_of_free (M : Type u) [AddCommGroup M] [Module R M] [Module.Free R M] - (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := - inferInstanceAs <| Module.Free R (⋀[R]^i M) - end IsRegular diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 5f06bd38384416..c33f6b396718f8 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -26,7 +26,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic universe u v w w' -open CategoryTheory Category MonoidalCategory +open CategoryTheory Category MonoidalCategory Limits section GradedAlgebra @@ -130,4 +130,35 @@ noncomputable abbrev ofList (l : List R) := def topHomologyLinearEquiv (l : List R) : (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry +instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := + inferInstanceAs <| Module.Free R (⋀[R]^i M) + +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 ((koszulComplex R x).X i) := by + classical + 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 + have hSubsingleton : Subsingleton (⋀[R]^i M) := + (Submodule.subsingleton_iff R).mp <| (subsingleton_iff_bot_eq_top).mp hbotTop + have hIsZero : IsZero (ModuleCat.of R (⋀[R]^i M)) := + ModuleCat.isZero_of_iff_subsingleton.mpr hSubsingleton + simpa [koszulComplex, ModuleCat.exteriorPower] using hIsZero + +lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : + IsZero ((koszulComplex.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 koszulComplex From 22dcd412419ccb447f61f1a48329c8e06e894353 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Tue, 27 Jan 2026 18:29:22 +0800 Subject: [PATCH 17/34] change def into nonempty because the construction is not canonical --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index 5da8d094a9091a..b39cf8bb823bb1 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -39,12 +39,23 @@ section change_generators variable [IsNoetherianRing R] [IsLocalRing R] -noncomputable def koszulComplex.isoOfMinimalGenerators {I : Ideal R} {l : List R} +theorem koszulComplex.nonempty_iso_of_minimal_generators {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 + refine ⟨isoOfEquiv R ?_ ?_⟩ + · sorry + · sorry + +theorem koszulComplex.noncmpty_iso_of_minimal_generators' {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) (min : l.length = I.spanFinrank) : - koszulComplex.ofList R I.finite_generators_of_isNoetherian.toFinset.toList ≅ - koszulComplex.ofList R l := by - refine isoOfEquiv R ?_ ?_ - all_goals sorry + 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 From cf3288128d1697e965f19c775bd042116278d26d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 29 Jan 2026 17:32:09 +0800 Subject: [PATCH 18/34] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 2be2851cead460..d733d5f1eec9d9 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4629,6 +4629,7 @@ public import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating public import Mathlib.LinearAlgebra.ExteriorPower.Basic +public import Mathlib.LinearAlgebra.ExteriorPower.Basis public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.LinearAlgebra.FiniteDimensional.Basic public import Mathlib.LinearAlgebra.FiniteDimensional.Defs From 95df8913a89db3d129b22e6c1199a0fc3539c264 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Sat, 31 Jan 2026 19:56:29 +0800 Subject: [PATCH 19/34] move files and update Mathlib.lean --- Mathlib.lean | 1 + Mathlib/RingTheory/KoszulComplex/Basic.lean | 28 +++-------- Mathlib/RingTheory/KoszulComplex/Defs.lean | 9 +++- Mathlib/RingTheory/KoszulComplex/Dual.lean | 51 +++++++++++++++++++++ 4 files changed, 67 insertions(+), 22 deletions(-) create mode 100644 Mathlib/RingTheory/KoszulComplex/Dual.lean diff --git a/Mathlib.lean b/Mathlib.lean index d733d5f1eec9d9..e7616cd0828de2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6129,6 +6129,7 @@ public import Mathlib.RingTheory.Kaehler.Polynomial public import Mathlib.RingTheory.Kaehler.TensorProduct public import Mathlib.RingTheory.KoszulComplex.Basic public import Mathlib.RingTheory.KoszulComplex.Defs +public import Mathlib.RingTheory.KoszulComplex.Dual public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.LocalRing diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index b39cf8bb823bb1..c916be2ecbf0b5 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -8,7 +8,7 @@ module public import Mathlib.RingTheory.KoszulComplex.Defs /-! -# Definition of Koszul complex +# Basic Properties of Koszul complex -/ @[expose] public section @@ -17,24 +17,6 @@ universe u v variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] -section homology_annihilator - -lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) - (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by - sorry - -lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : - Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList R l).homology i) := by - intro r hr - have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] - rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ - let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c - have hφ : φ l.get = r := by - simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] - exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i - -end homology_annihilator - section change_generators variable [IsNoetherianRing R] [IsLocalRing R] @@ -63,10 +45,14 @@ section basechange variable (S : Type u) [CommRing S] (f : R →+* S) +open TensorProduct in def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : koszulComplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex - (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := - sorry + (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := by + refine HomologicalComplex.Hom.isoOfComponents + (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) + · sorry + · sorry end basechange diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index c33f6b396718f8..30a0be3f9d11d6 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -26,7 +26,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic universe u v w w' -open CategoryTheory Category MonoidalCategory Limits +open CategoryTheory Category MonoidalCategory Limits Module section GradedAlgebra @@ -36,6 +36,10 @@ variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι] def GradedAlgebra.linearGMul (h : k = i + j) : 𝒜 i →ₗ[R] (𝒜 j →ₗ[R] 𝒜 k) := sorry +#check GradedMonoid.GMul + +#check GradedRing + @[simp] lemma GradedAlgebra.linearGMul_eq_mul (h : k = i + j) (x : 𝒜 i) (y : 𝒜 j) : (GradedAlgebra.linearGMul 𝒜 h) x y = x.1 * y.1 := sorry @@ -124,6 +128,9 @@ noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) : LinearEquiv.refl_toLinearMap] exact map_id_refl R y +noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder ι] (x : M) + (b : Basis ι R M) : (koszulComplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry + noncomputable abbrev ofList (l : List R) := koszulComplex R l.get diff --git a/Mathlib/RingTheory/KoszulComplex/Dual.lean b/Mathlib/RingTheory/KoszulComplex/Dual.lean new file mode 100644 index 00000000000000..509c56b829f894 --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Dual.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Jingting Wang, Nailin Guan, Yi Yuan, Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jingting Wang, Nailin Guan, Yi Yuan, Yongle Hu +-/ +module + +public import Mathlib.RingTheory.KoszulComplex.Defs +public import Mathlib.RingTheory.KoszulComplex.Basic + +/-! +# The dual of Koszul complex +-/ + +@[expose] public section + +universe u v + +open ExteriorAlgebra + +variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) + +noncomputable def koszulComplexDual_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M := + exteriorPower.alternatingMapLinearEquiv { + toFun x := ∑ i : Fin (n + 1), + ((-1) ^ i.1 * (φ (x i))) • exteriorPower.ιMulti R n (x ∘ i.succAbove) + map_update_add' := sorry + map_update_smul' := sorry + map_eq_zero_of_eq' := sorry + } + +lemma koszulComplexDual_aux_comp_eq_zero (n : ℕ) : + koszulComplexDual_aux φ n ∘ₗ koszulComplexDual_aux φ (n + 1) = 0 := sorry + +section homology_annihilator + +lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) + (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by + sorry + +lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : + Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList R l).homology i) := by + intro r hr + have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] + rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ + let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c + have hφ : φ l.get = r := by + simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] + exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i + +end homology_annihilator From 1bdae408f44f6bf587d870206136e11d8b86995a Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 1 Feb 2026 14:11:53 +0800 Subject: [PATCH 20/34] generalize universe --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index c916be2ecbf0b5..e703938637cc4c 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -43,7 +43,14 @@ end change_generators section basechange -variable (S : Type u) [CommRing S] (f : R →+* S) +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', Algebra.algebraMap_self, + ModuleCat.hom_add, LinearMap.baseChange_add] + rfl open TensorProduct in def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : From 3f4fdfb8ac58b65bb8dabc59e84f387fe16354b1 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 1 Feb 2026 14:15:37 +0800 Subject: [PATCH 21/34] fix typo --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index e703938637cc4c..fcf2beb57bb457 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -29,7 +29,7 @@ theorem koszulComplex.nonempty_iso_of_minimal_generators {I : Ideal R} {l l' : L · sorry · sorry -theorem koszulComplex.noncmpty_iso_of_minimal_generators' {I : Ideal R} {l : List R} +theorem koszulComplex.nonempty_iso_of_minimal_generators' {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 From 38268b7c5cd216af45a034c3d40b03d1be764b9d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 3 Feb 2026 14:56:06 +0800 Subject: [PATCH 22/34] add a variant --- Mathlib/RingTheory/KoszulComplex/Defs.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 30a0be3f9d11d6..288701bbbd2a0e 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -137,6 +137,9 @@ noncomputable abbrev ofList (l : List R) := def topHomologyLinearEquiv (l : List R) : (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry +noncomputable def topXLinearEquivOfBasisOfList (l : List R) : + (koszulComplex.ofList R l).X l.length ≃ₗ[R] R := sorry + instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := inferInstanceAs <| Module.Free R (⋀[R]^i M) From 51127ec986c6c547b49b86482eb2fc42c078f829 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 17:31:56 +0800 Subject: [PATCH 23/34] update --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 19 +- Mathlib/RingTheory/KoszulComplex/Defs.lean | 51 ++-- Mathlib/RingTheory/KoszulComplex/Dual.lean | 259 +++++++++++++++++++- 3 files changed, 278 insertions(+), 51 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index fcf2beb57bb457..352b7729e0d145 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -21,7 +21,7 @@ section change_generators variable [IsNoetherianRing R] [IsLocalRing R] -theorem koszulComplex.nonempty_iso_of_minimal_generators {I : Ideal R} {l l' : List R} +theorem koszulCocomplex.nonempty_iso_of_minimal_generators {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 @@ -29,7 +29,7 @@ theorem koszulComplex.nonempty_iso_of_minimal_generators {I : Ideal R} {l l' : L · sorry · sorry -theorem koszulComplex.nonempty_iso_of_minimal_generators' {I : Ideal R} {l : List R} +theorem koszulCocomplex.nonempty_iso_of_minimal_generators' {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 @@ -38,7 +38,6 @@ theorem koszulComplex.nonempty_iso_of_minimal_generators' {I : Ideal R} {l : Lis · simp only [Finset.length_toList, ← Set.ncard_eq_toFinset_card _ _] exact Submodule.FG.generators_ncard Submodule.FG.of_finite - end change_generators section basechange @@ -53,9 +52,9 @@ instance (T : Type v) [CommRing T] (g : R →+* T) : rfl open TensorProduct in -def koszulComplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : - koszulComplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex - (ComplexShape.up ℕ)).obj (koszulComplex.ofList R l) := by +def koszulCocomplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + koszulCocomplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex + (ComplexShape.up ℕ)).obj (koszulCocomplex.ofList R l) := by refine HomologicalComplex.Hom.isoOfComponents (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) · sorry @@ -67,12 +66,12 @@ section IsRegular open RingTheory.Sequence -lemma koszulComplex.exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) - (i : ℕ) (lt : i < rs.length) : (koszulComplex.ofList R rs).ExactAt i := by +lemma koszulCocomplex.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 koszulComplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) - (i : ℕ) (lt : i ≠ rs.length) : (koszulComplex.ofList R rs).ExactAt i := by +theorem koszulCocomplex.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 IsRegular diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Defs.lean index 30a0be3f9d11d6..dc3e7151b68191 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Defs.lean @@ -36,32 +36,18 @@ variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι] def GradedAlgebra.linearGMul (h : k = i + j) : 𝒜 i →ₗ[R] (𝒜 j →ₗ[R] 𝒜 k) := sorry -#check GradedMonoid.GMul - -#check GradedRing - @[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 ModuleCat - -variable {R : Type u} [CommRing R] - -def ModuleCat.tensorFunctor (M : ModuleCat.{v} R) [Small.{w'} M] [UnivLE.{w, w'}] : - ModuleCat.{w} R ⥤ ModuleCat.{w'} R := sorry - -end ModuleCat - section variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] variable {M} in -noncomputable def koszulComplex (x : M) : - HomologicalComplex (ModuleCat.{max u v} R) (ComplexShape.up ℕ) := +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) @@ -76,12 +62,12 @@ noncomputable def koszulComplex (x : M) : CliffordAlgebra.ι_sq_scalar, QuadraticMap.zero_apply, map_zero, zero_mul] rfl) -namespace koszulComplex +namespace koszulCocomplex variable {M} {N : Type v} [AddCommGroup N] [Module R N] noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : - koszulComplex R x ⟶ koszulComplex R y := + koszulCocomplex R x ⟶ koszulCocomplex R y := CochainComplex.ofHom _ _ _ _ _ _ (fun i ↦ (ModuleCat.exteriorPower.functor R i).map (ModuleCat.ofHom f)) (fun i ↦ by @@ -97,28 +83,29 @@ noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : 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) : koszulComplex.map R (M := M) .id (Eq.refl x) = 𝟙 _ := by +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) : koszulComplex.map R (M := M) .id h = eqToHom (by rw [h]) := by +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 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) : - koszulComplex.map R f hxy ≫ koszulComplex.map R g hyz = - koszulComplex.map R (g ∘ₗ f) (hxy ▸ hyz : g (f x) = z) := by + 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) : - koszulComplex R x ≅ koszulComplex R y where - hom := koszulComplex.map R f h - inv := koszulComplex.map R f.symm (f.injective (by simpa using h.symm)) + 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] @@ -129,20 +116,20 @@ noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) : exact map_id_refl R y noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder ι] (x : M) - (b : Basis ι R M) : (koszulComplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry + (b : Basis ι R M) : (koszulCocomplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry noncomputable abbrev ofList (l : List R) := - koszulComplex R l.get + koszulCocomplex R l.get def topHomologyLinearEquiv (l : List R) : - (koszulComplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + (koszulCocomplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry -instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulComplex R x).X i) := +instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulCocomplex R x).X i) := inferInstanceAs <| Module.Free R (⋀[R]^i M) 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 ((koszulComplex R x).X i) := by + IsZero ((koszulCocomplex R x).X i) := by classical letI : Fintype ι := Fintype.ofFinite ι letI : LinearOrder ι := LinearOrder.lift' (Fintype.equivFin ι) (Fintype.equivFin ι).injective @@ -160,12 +147,12 @@ lemma X_isZero_of_card_generators_le (x : M) {ι : Type*} [Finite ι] (g : ι (Submodule.subsingleton_iff R).mp <| (subsingleton_iff_bot_eq_top).mp hbotTop have hIsZero : IsZero (ModuleCat.of R (⋀[R]^i M)) := ModuleCat.isZero_of_iff_subsingleton.mpr hSubsingleton - simpa [koszulComplex, ModuleCat.exteriorPower] using hIsZero + simpa [koszulCocomplex, ModuleCat.exteriorPower] using hIsZero lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : - IsZero ((koszulComplex.ofList R l).X 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 koszulComplex +end koszulCocomplex diff --git a/Mathlib/RingTheory/KoszulComplex/Dual.lean b/Mathlib/RingTheory/KoszulComplex/Dual.lean index 509c56b829f894..15d919f92f2912 100644 --- a/Mathlib/RingTheory/KoszulComplex/Dual.lean +++ b/Mathlib/RingTheory/KoszulComplex/Dual.lean @@ -6,7 +6,8 @@ Authors: Jingting Wang, Nailin Guan, Yi Yuan, Yongle Hu module public import Mathlib.RingTheory.KoszulComplex.Defs -public import Mathlib.RingTheory.KoszulComplex.Basic +public import Mathlib.Algebra.Homology.Homotopy +public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin /-! # The dual of Koszul complex @@ -20,26 +21,266 @@ open ExteriorAlgebra variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) -noncomputable def koszulComplexDual_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M := +noncomputable def koszulComplex_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M := exteriorPower.alternatingMapLinearEquiv { toFun x := ∑ i : Fin (n + 1), ((-1) ^ i.1 * (φ (x i))) • exteriorPower.ιMulti R n (x ∘ i.succAbove) - map_update_add' := sorry - map_update_smul' := sorry - map_eq_zero_of_eq' := sorry + map_update_add' := by + classical + intro _ m p x y + have hremove (v : Fin (n + 1) → M) (k : Fin (n + 1)) : v ∘ k.succAbove = k.removeNth v := rfl + let term (v : Fin (n + 1) → M) (k : Fin (n + 1)) := + ((-1) ^ (k : ℕ) * φ (v k)) • exteriorPower.ιMulti R n (v ∘ k.succAbove) + have hcalc : + ∑ k, term (Function.update m p (x + y)) k = + ∑ k, term (Function.update m p x) k + ∑ k, term (Function.update m p y) k := by + calc + ∑ k, term (Function.update m p (x + y)) k = + ∑ k, (term (Function.update m p x) k + term (Function.update m p y) k) := by + refine Finset.sum_congr rfl ?_ + intro k hk + by_cases hk' : k = p + · subst hk' + have hupdate (z : M) : k.removeNth (Function.update m k z) = k.removeNth m := by + ext i + simp [Fin.removeNth, Function.update, Fin.succAbove_ne] + simp [term, hremove, LinearMap.map_add, mul_add, add_smul, hupdate (x + y), + hupdate x, hupdate y] + · rcases Fin.exists_succAbove_eq (x := p) (y := k) (by + simpa [ne_comm] using hk') with ⟨j, rfl⟩ + have hupdate (z : M) : + k.removeNth (Function.update m (k.succAbove j) z) = + Function.update (k.removeNth m) j z := by + ext i + by_cases hi : i = j + · subst hi; simp [Fin.removeNth, Function.update] + · have hne : k.succAbove i ≠ k.succAbove j := by + exact fun h => hi (Fin.succAbove_right_inj.mp h) + simp [Fin.removeNth, Function.update, hi, hne] + simp [term, hremove, hupdate (x + y), hupdate x, hupdate y, smul_add] + _ = ∑ k, term (Function.update m p x) k + ∑ k, term (Function.update m p y) k := by + simp [Finset.sum_add_distrib] + simpa [term] using hcalc + map_update_smul' := by + classical + intro _ m p c x + have hremove (v : Fin (n + 1) → M) (k : Fin (n + 1)) : v ∘ k.succAbove = k.removeNth v := rfl + let term (v : Fin (n + 1) → M) (k : Fin (n + 1)) := + ((-1) ^ (k : ℕ) * φ (v k)) • exteriorPower.ιMulti R n (v ∘ k.succAbove) + have hcalc : + ∑ k, term (Function.update m p (c • x)) k = + ∑ k, c • term (Function.update m p x) k := by + refine Finset.sum_congr rfl ?_ + intro k hk + by_cases hk' : k = p + · subst hk' + have hupdate (z : M) : k.removeNth (Function.update m k z) = k.removeNth m := by + ext i + simp [Fin.removeNth, Function.update, Fin.succAbove_ne] + simp [term, hremove, LinearMap.map_smul, smul_smul, mul_comm, mul_left_comm, mul_assoc, + hupdate (c • x), hupdate x] + · rcases Fin.exists_succAbove_eq (x := p) (y := k) (by + simpa [ne_comm] using hk') with ⟨j, rfl⟩ + have hupdate (z : M) : + k.removeNth (Function.update m (k.succAbove j) z) = + Function.update (k.removeNth m) j z := by + ext i + by_cases hi : i = j + · subst hi; simp [Fin.removeNth, Function.update] + · have hne : k.succAbove i ≠ k.succAbove j := by + exact fun h => hi (Fin.succAbove_right_inj.mp h) + simp [Fin.removeNth, Function.update, hi, hne] + simp [term, hremove, smul_smul, mul_comm, mul_left_comm, mul_assoc, hupdate (c • x), + hupdate x] + have hcalc' : + ∑ k, term (Function.update m p (c • x)) k = + c • ∑ k, term (Function.update m p x) k := by + calc + ∑ k, term (Function.update m p (c • x)) k = + ∑ k, c • term (Function.update m p x) k := hcalc + _ = c • ∑ k, term (Function.update m p x) k := by + simpa using (Finset.smul_sum (r := c) (f := fun k ↦ term (Function.update m p x) k) + (s := Finset.univ)).symm + simpa [term] using hcalc' + map_eq_zero_of_eq' := by + sorry + -- classical + -- intro v i j hvij hij + -- have hremove (v : Fin (n + 1) → M) (k : Fin (n + 1)) : v ∘ k.succAbove = k.removeNth v := rfl + -- let term (v : Fin (n + 1) → M) (k : Fin (n + 1)) := + -- ((-1) ^ (k : ℕ) * φ (v k)) • exteriorPower.ιMulti R n (v ∘ k.succAbove) + -- have hsum : ∑ k, term v k = term v i + term v j := by + -- refine Fintype.sum_eq_add i j hij ?_ + -- intro k hk + -- rcases hk with ⟨hki, hkj⟩ + -- rcases Fin.exists_succAbove_eq (x := i) (y := k) hki.symm with ⟨i', hi'⟩ + -- rcases Fin.exists_succAbove_eq (x := j) (y := k) hkj.symm with ⟨j', hj'⟩ + -- have hij' : i' ≠ j' := by + -- intro h + -- apply hij + -- have : k.succAbove i' = k.succAbove j' := by simpa [h] + -- simpa [hi', hj'] using this + -- have hzero : exteriorPower.ιMulti R n (v ∘ k.succAbove) = 0 := by + -- refine (exteriorPower.ιMulti R n).map_eq_zero_of_eq (v := v ∘ k.succAbove) ?_ hij' + -- simpa [Function.comp, hi', hj', hvij] + -- simp [term, hzero] + -- have hneg : + -- (-1 : R) ^ (i : ℕ) • exteriorPower.ιMulti R n (i.removeNth v) + + -- (-1 : R) ^ (j : ℕ) • exteriorPower.ιMulti R n (j.removeNth v) = 0 := by + -- rcases Fin.exists_succAbove_eq hij with ⟨i', rfl⟩ + -- obtain ⟨m, rfl⟩ : ∃ m, m + 1 = n := by simp [i'.pos] + -- rw [← (i'.predAbove j).insertNth_self_removeNth (Fin.removeNth _ _), + -- ← Fin.removeNth_removeNth_eq_swap, Fin.removeNth, Fin.succAbove_succAbove_predAbove, + -- AlternatingMap.map_insertNth, ← AlternatingMap.neg_one_pow_smul_map_insertNth, + -- Fin.insertNth_removeNth, Function.update_eq_self_iff.2, smul_smul, ← pow_add, + -- Fin.neg_one_pow_succAbove_add_predAbove, neg_smul, pow_add, mul_smul, + -- smul_smul (_ ^ i'.val), ← sq, ← pow_mul, pow_mul', neg_one_pow_two, one_pow, one_smul, + -- neg_add_cancel] + -- exact hvij.symm + -- have hcancel : term v i + term v j = 0 := by + -- calc + -- term v i + term v j = + -- ((-1) ^ (i : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (i.removeNth v) + + -- ((-1) ^ (j : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (j.removeNth v) := by + -- simp [term, hremove, hvij, mul_comm, mul_left_comm, mul_assoc] + -- _ = + -- φ (v j) • ((-1 : R) ^ (i : ℕ) • exteriorPower.ιMulti R n (i.removeNth v)) + + -- φ (v j) • ((-1 : R) ^ (j : ℕ) • exteriorPower.ιMulti R n (j.removeNth v)) := by + -- have h1 : + -- ((-1 : R) ^ (i : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (i.removeNth v) = + -- φ (v j) • + -- ((-1 : R) ^ (i : ℕ) • exteriorPower.ιMulti R n (i.removeNth v)) := by + -- calc + -- ((-1 : R) ^ (i : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (i.removeNth v) = + -- (φ (v j) * (-1 : R) ^ (i : ℕ)) • + -- exteriorPower.ιMulti R n (i.removeNth v) := by + -- simp [mul_comm, mul_left_comm, mul_assoc] + -- _ = φ (v j) • + -- ((-1 : R) ^ (i : ℕ) • exteriorPower.ιMulti R n (i.removeNth v)) := by + -- simpa using + -- (mul_smul (φ (v j)) ((-1 : R) ^ (i : ℕ)) + -- (exteriorPower.ιMulti R n (i.removeNth v))) + -- have h2 : + -- ((-1 : R) ^ (j : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (j.removeNth v) = + -- φ (v j) • + -- ((-1 : R) ^ (j : ℕ) • exteriorPower.ιMulti R n (j.removeNth v)) := by + -- calc + -- ((-1 : R) ^ (j : ℕ) * φ (v j)) • exteriorPower.ιMulti R n (j.removeNth v) = + -- (φ (v j) * (-1 : R) ^ (j : ℕ)) • + -- exteriorPower.ιMulti R n (j.removeNth v) := by + -- simp [mul_comm, mul_left_comm, mul_assoc] + -- _ = φ (v j) • + -- ((-1 : R) ^ (j : ℕ) • exteriorPower.ιMulti R n (j.removeNth v)) := by + -- simpa using + -- (mul_smul (φ (v j)) ((-1 : R) ^ (j : ℕ)) + -- (exteriorPower.ιMulti R n (j.removeNth v))) + -- rw [h1, h2] + -- _ = φ (v j) • + -- ((-1 : R) ^ (i : ℕ) • exteriorPower.ιMulti R n (i.removeNth v) + + -- (-1 : R) ^ (j : ℕ) • exteriorPower.ιMulti R n (j.removeNth v)) := by + -- simp [smul_add] + -- _ = 0 := by simpa [hneg] + -- calc + -- ∑ k, term v k = term v i + term v j := hsum + -- _ = 0 := hcancel } -lemma koszulComplexDual_aux_comp_eq_zero (n : ℕ) : - koszulComplexDual_aux φ n ∘ₗ koszulComplexDual_aux φ (n + 1) = 0 := sorry +lemma koszulComplex_aux_comp_eq_zero (n : ℕ) : + koszulComplex_aux φ n ∘ₗ koszulComplex_aux φ (n + 1) = 0 := by + -- ext x + -- simp [koszulComplex_aux] + -- classical + -- have hremove (v : Fin (n + 2) → M) (k : Fin (n + 2)) : v ∘ k.succAbove = k.removeNth v := rfl + -- have hremove' (v : Fin (n + 1) → M) (k : Fin (n + 1)) : v ∘ k.succAbove = k.removeNth v := rfl + -- -- rewrite inner compositions using `removeNth` + -- simp [hremove, hremove'] + -- let term : Fin (n + 2) → Fin (n + 1) → ⋀[R]^n M := fun i j => + -- ((-1) ^ (i : ℕ) * φ (x i)) • + -- ((-1) ^ (j : ℕ) * φ (x (i.succAbove j))) • + -- exteriorPower.ιMulti R n (j.removeNth (i.removeNth x)) + -- let f : Fin (n + 2) × Fin (n + 1) → ⋀[R]^n M := fun p => term p.1 p.2 + -- let g : Fin (n + 2) × Fin (n + 1) → Fin (n + 2) × Fin (n + 1) := + -- fun p => (p.1.succAbove p.2, p.2.predAbove p.1) + -- have hpair : ∀ p, f p + f (g p) = 0 := by + -- intro p + -- rcases p with ⟨i, j⟩ + -- have hswap : + -- (j.predAbove i).removeNth ((i.succAbove j).removeNth x) = j.removeNth (i.removeNth x) := by + -- simpa using (Fin.removeNth_removeNth_eq_swap (m := x) (i := j) (j := i)).symm + -- have hsign : + -- (-1 : R) ^ (i.succAbove j + j.predAbove i : ℕ) = + -- -((-1 : R) ^ (i : ℕ) * (-1 : R) ^ (j : ℕ)) := by + -- simpa [pow_add] using + -- (Fin.neg_one_pow_succAbove_add_predAbove (R := R) (i := i) (j := j)) + -- have hsign' : + -- (-1 : R) ^ (i.succAbove j : ℕ) * (-1 : R) ^ (j.predAbove i : ℕ) = + -- -((-1 : R) ^ (i : ℕ) * (-1 : R) ^ (j : ℕ)) := by + -- simpa [pow_add, mul_comm, mul_left_comm, mul_assoc] using hsign + -- let w : ⋀[R]^n M := exteriorPower.ιMulti R n (j.removeNth (i.removeNth x)) + -- have hw : w = exteriorPower.ιMulti R n (j.removeNth (i.removeNth x)) := rfl + -- calc + -- f ⟨i, j⟩ + f (g ⟨i, j⟩) = + -- ( ((-1 : R) ^ (i : ℕ) * φ (x i) * ((-1 : R) ^ (j : ℕ) * φ (x (i.succAbove j)))) + -- + ((-1 : R) ^ (i.succAbove j : ℕ) * φ (x (i.succAbove j)) * + -- ((-1 : R) ^ (j.predAbove i : ℕ) * φ (x i))) ) + -- • w := by + -- simp [f, term, g, hswap, hw, Fin.succAbove_succAbove_predAbove, smul_smul, + -- mul_comm, mul_left_comm, mul_assoc, add_smul] + -- _ = 0 := by + -- -- cancel by pairing the two terms using the sign lemma + -- have hscalar : + -- (-1 : R) ^ (i : ℕ) * φ (x i) * ((-1 : R) ^ (j : ℕ) * φ (x (i.succAbove j))) + + -- (-1 : R) ^ (i.succAbove j : ℕ) * φ (x (i.succAbove j)) * + -- ((-1 : R) ^ (j.predAbove i : ℕ) * φ (x i)) = 0 := by + -- calc + -- _ = ((-1 : R) ^ (i : ℕ) * (-1 : R) ^ (j : ℕ) * + -- (φ (x i) * φ (x (i.succAbove j)))) + + -- ((-1 : R) ^ (i.succAbove j : ℕ) * (-1 : R) ^ (j.predAbove i : ℕ) * + -- (φ (x i) * φ (x (i.succAbove j)))) := by + -- simp [mul_comm, mul_left_comm, mul_assoc] + -- _ = ((-1 : R) ^ (i : ℕ) * (-1 : R) ^ (j : ℕ) * + -- (φ (x i) * φ (x (i.succAbove j)))) + + -- (-((-1 : R) ^ (i : ℕ) * (-1 : R) ^ (j : ℕ)) * + -- (φ (x i) * φ (x (i.succAbove j)))) := by + -- simp [hsign', mul_comm, mul_left_comm, mul_assoc] + -- _ = 0 := by ring + -- simpa [hscalar] + -- have hne : ∀ p, g p ≠ p := by + -- intro p hp + -- have : p.1.succAbove p.2 = p.1 := by simpa [g] using congrArg Prod.fst hp + -- exact (Fin.succAbove_ne _ _) this + -- have hinvol : ∀ p, g (g p) = p := by + -- intro p + -- rcases p with ⟨i, j⟩ + -- simp [g, Fin.succAbove_succAbove_predAbove, Fin.predAbove_predAbove_succAbove] + -- have hsum : ∑ p : Fin (n + 2) × Fin (n + 1), f p = 0 := by + -- simpa using + -- (Finset.sum_ninvolution (s := Finset.univ) (f := f) (g := g) hpair + -- (fun p _ => hne p) (by intro p; simp) hinvol) + -- have hsum' : + -- ∑ i, ∑ j, term i j = ∑ p : Fin (n + 2) × Fin (n + 1), f p := by + -- simpa [f] using (Fintype.sum_prod_type' (f := term)).symm + -- have hmain : ∑ i, ∑ j, term i j = 0 := by + -- calc + -- ∑ i, ∑ j, term i j = ∑ p : Fin (n + 2) × Fin (n + 1), f p := hsum' + -- _ = 0 := hsum + -- simpa [term, Finset.smul_sum] using hmain + sorry + +noncomputable def koszulComplex : ChainComplex (ModuleCat R) ℕ := + ChainComplex.of + (ModuleCat.of R M).exteriorPower + (fun n ↦ ModuleCat.ofHom (koszulComplex_aux φ n)) + (fun n ↦ by simp [← ModuleCat.ofHom_comp, koszulComplex_aux_comp_eq_zero]; rfl) section homology_annihilator lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) - (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulComplex R x).homology i) := by + (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by sorry lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : - Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList R l).homology i) := by + Ideal.ofList l ≤ Module.annihilator R ((koszulCocomplex.ofList R l).homology i) := by intro r hr have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ From 1e19dbd9f10018ea9dbe2db7ad26fb8b07ff0d44 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 17:42:20 +0800 Subject: [PATCH 24/34] File refactor --- Mathlib.lean | 5 ++- Mathlib/RingTheory/KoszulComplex/Basic.lean | 5 ++- .../{Defs.lean => Cocomplex.lean} | 10 +---- .../KoszulComplex/{Dual.lean => Complex.lean} | 26 +++--------- .../RingTheory/KoszulComplex/Homotopy.lean | 40 +++++++++++++++++++ 5 files changed, 55 insertions(+), 31 deletions(-) rename Mathlib/RingTheory/KoszulComplex/{Defs.lean => Cocomplex.lean} (95%) rename Mathlib/RingTheory/KoszulComplex/{Dual.lean => Complex.lean} (93%) create mode 100644 Mathlib/RingTheory/KoszulComplex/Homotopy.lean diff --git a/Mathlib.lean b/Mathlib.lean index e7616cd0828de2..65c3c92c0df450 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6128,8 +6128,9 @@ public import Mathlib.RingTheory.Kaehler.JacobiZariski public import Mathlib.RingTheory.Kaehler.Polynomial public import Mathlib.RingTheory.Kaehler.TensorProduct public import Mathlib.RingTheory.KoszulComplex.Basic -public import Mathlib.RingTheory.KoszulComplex.Defs -public import Mathlib.RingTheory.KoszulComplex.Dual +public import Mathlib.RingTheory.KoszulComplex.Cocomplex +public import Mathlib.RingTheory.KoszulComplex.Complex +public import Mathlib.RingTheory.KoszulComplex.Homotopy public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.LocalRing diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index 352b7729e0d145..f7d22ac5de2d72 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -5,7 +5,10 @@ Authors: Jingting Wang, Nailin Guan -/ module -public import Mathlib.RingTheory.KoszulComplex.Defs +public import Mathlib.RingTheory.KoszulComplex.Complex +public import Mathlib.RingTheory.KoszulComplex.Cocomplex +public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings /-! # Basic Properties of Koszul complex diff --git a/Mathlib/RingTheory/KoszulComplex/Defs.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean similarity index 95% rename from Mathlib/RingTheory/KoszulComplex/Defs.lean rename to Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index 540deb023e0b69..ef36bb5d635d7a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Defs.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -5,18 +5,12 @@ Authors: Jingting Wang, Nailin Guan -/ module -public import Mathlib.LinearAlgebra.ExteriorPower.Basis -public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.Algebra.Category.ModuleCat.Abelian -public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower -public import Mathlib.Algebra.Homology.HomologicalComplex -public import Mathlib.Algebra.Homology.Monoidal -public import Mathlib.Algebra.Homology.ShortComplex.Abelian 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.Algebra.Category.ModuleCat.Monoidal.Basic /-! # Definition of Koszul complex diff --git a/Mathlib/RingTheory/KoszulComplex/Dual.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean similarity index 93% rename from Mathlib/RingTheory/KoszulComplex/Dual.lean rename to Mathlib/RingTheory/KoszulComplex/Complex.lean index 15d919f92f2912..94ee2aa227d423 100644 --- a/Mathlib/RingTheory/KoszulComplex/Dual.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -5,8 +5,12 @@ Authors: Jingting Wang, Nailin Guan, Yi Yuan, Yongle Hu -/ module -public import Mathlib.RingTheory.KoszulComplex.Defs -public import Mathlib.Algebra.Homology.Homotopy +public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower +public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex +public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading +public import Mathlib.LinearAlgebra.ExteriorPower.Basis +public import Mathlib.RingTheory.Regular.RegularSequence public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin /-! @@ -272,21 +276,3 @@ noncomputable def koszulComplex : ChainComplex (ModuleCat R) ℕ := (ModuleCat.of R M).exteriorPower (fun n ↦ ModuleCat.ofHom (koszulComplex_aux φ n)) (fun n ↦ by simp [← ModuleCat.ofHom_comp, koszulComplex_aux_comp_eq_zero]; rfl) - -section homology_annihilator - -lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) - (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by - sorry - -lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : - Ideal.ofList l ≤ Module.annihilator R ((koszulCocomplex.ofList R l).homology i) := by - intro r hr - have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] - rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ - let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c - have hφ : φ l.get = r := by - simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] - exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i - -end homology_annihilator diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean new file mode 100644 index 00000000000000..c5b4fca174156b --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean @@ -0,0 +1,40 @@ +/- +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.Homology.Homotopy +public import Mathlib.RingTheory.KoszulComplex.Complex +public import Mathlib.RingTheory.KoszulComplex.Cocomplex + +/-! +# Homotopy on Koszul complex +-/ + +@[expose] public section + +universe u v + +open ExteriorAlgebra + +variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) + +section homology_annihilator + +lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) + (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by + sorry + +lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : + Ideal.ofList l ≤ Module.annihilator R ((koszulCocomplex.ofList R l).homology i) := by + intro r hr + have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] + rcases (Ideal.mem_span_range_iff_exists_fun (R := R) (x := r) (v := l.get)).1 hr' with ⟨c, hc⟩ + let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c + have hφ : φ l.get = r := by + simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] + exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i + +end homology_annihilator From 9e5e496ba51600ec690364c7b8cf57d0323eee9d Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 18:20:22 +0800 Subject: [PATCH 25/34] update file structure --- .../RingTheory/KoszulComplex/Cocomplex.lean | 30 ++++++++++++------- Mathlib/RingTheory/KoszulComplex/Complex.lean | 9 ++++++ .../RingTheory/KoszulComplex/Homotopy.lean | 27 +++++++++++++---- 3 files changed, 51 insertions(+), 15 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index ef36bb5d635d7a..65ec103347c587 100644 --- a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -58,8 +58,16 @@ noncomputable def koszulCocomplex (x : M) : CochainComplex (ModuleCat.{max u v} 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 + noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : koszulCocomplex R x ⟶ koszulCocomplex R y := CochainComplex.ofHom _ _ _ _ _ _ @@ -109,20 +117,15 @@ noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) : LinearEquiv.refl_toLinearMap] exact map_id_refl R y -noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder ι] (x : M) - (b : Basis ι R M) : (koszulCocomplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry +end functoriality -noncomputable abbrev ofList (l : List R) := - koszulCocomplex R l.get +section specialX -def topHomologyLinearEquiv (l : List R) : - (koszulCocomplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry +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) : - (koszulCocomplex.ofList R l).X l.length ≃ₗ[R] R := sorry - -instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulCocomplex R x).X i) := - inferInstanceAs <| Module.Free R (⋀[R]^i M) + (ofList R l).X l.length ≃ₗ[R] R := sorry 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) : @@ -152,4 +155,11 @@ lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : (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 + +-- def topHomologyLinearEquiv (l : List R) : +-- (koszulCocomplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + + + end koszulCocomplex diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index 94ee2aa227d423..351ff2a9a51a4a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -276,3 +276,12 @@ noncomputable def koszulComplex : ChainComplex (ModuleCat R) ℕ := (ModuleCat.of R M).exteriorPower (fun n ↦ ModuleCat.ofHom (koszulComplex_aux φ n)) (fun n ↦ by simp [← ModuleCat.ofHom_comp, koszulComplex_aux_comp_eq_zero]; rfl) + +namespace koszulComplex + +variable {N : Type v} [AddCommGroup N] [Module R N] + +noncomputable def map (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) : + koszulComplex φ ⟶ koszulComplex φ' := sorry + +end koszulComplex diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean index c5b4fca174156b..20d27cacebeb4f 100644 --- a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean +++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean @@ -19,15 +19,32 @@ universe u v open ExteriorAlgebra -variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) +variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] + (φ : M →ₗ[R] R) (x : M) + +#check Homotopy section homology_annihilator -lemma koszulComplex.mem_annihilator_homology (M : Type u) [AddCommGroup M] [Module R M] (x : M) - (φ : M →ₗ[R] R) (i : ℕ) : φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by +lemma koszulComplex.mem_annihilator_homology (i : ℕ) : + φ x ∈ Module.annihilator R ((koszulComplex φ).homology i) := by + sorry + +lemma koszulComplex.range_le_annihilator_homology (i : ℕ) : + φ.range ≤ Module.annihilator R ((koszulComplex φ).homology i) := by + rintro _ ⟨x, rfl⟩ + exact mem_annihilator_homology φ x i + +lemma koszulComplex.ofList_ideal_annihilator_homology (l : List R) (i : ℕ) : + Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList l).homology i) := by + convert range_le_annihilator_homology _ i + simp + +lemma koszulCocomplex.mem_annihilator_homology (i : ℕ) : + φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by sorry -lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : +lemma koszulCocomplex.ofList_ideal_le_mem_annihilator_homology (l : List R) (i : ℕ) : Ideal.ofList l ≤ Module.annihilator R ((koszulCocomplex.ofList R l).homology i) := by intro r hr have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l] @@ -35,6 +52,6 @@ lemma koszulComplex.mem_annihilator_homology_ofList (l : List R) (i : ℕ) : let φ : (Fin l.length → R) →ₗ[R] R := Fintype.linearCombination R c have hφ : φ l.get = r := by simp only [φ, ← hc, Fintype.linearCombination_apply, mul_comm (c _), smul_eq_mul] - exact hφ ▸ mem_annihilator_homology (R := R) (M := Fin l.length → R) (x := l.get) φ i + exact hφ ▸ mem_annihilator_homology φ l.get i end homology_annihilator From 38cfd154b2ac00bc022981142dda0c7743cd026e Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 19:02:45 +0800 Subject: [PATCH 26/34] move proofs --- .../LinearAlgebra/ExteriorPower/Basis.lean | 17 +++++++++++ .../RingTheory/KoszulComplex/Cocomplex.lean | 30 +++++-------------- Mathlib/RingTheory/KoszulComplex/Complex.lean | 10 +++++++ .../RingTheory/KoszulComplex/Homotopy.lean | 5 ++-- 4 files changed, 36 insertions(+), 26 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 34fae2c32af591..96c0b75d5b071f 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -81,3 +81,20 @@ instance Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R ( letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) exact Module.Free.of_basis (exteriorPower.basis (R := R) (M := M) (ι := ι) (Module.Free.chooseBasis R M) n) + +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 diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index 65ec103347c587..15d02d976305ef 100644 --- a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -125,28 +125,17 @@ noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder (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 := sorry + (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)) 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 - classical - 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 - have hSubsingleton : Subsingleton (⋀[R]^i M) := - (Submodule.subsingleton_iff R).mp <| (subsingleton_iff_bot_eq_top).mp hbotTop - have hIsZero : IsZero (ModuleCat.of R (⋀[R]^i M)) := - ModuleCat.isZero_of_iff_subsingleton.mpr hSubsingleton + 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) : @@ -157,9 +146,4 @@ lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : end specialX --- def topHomologyLinearEquiv (l : List R) : --- (koszulCocomplex.ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry - - - end koszulCocomplex diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index 351ff2a9a51a4a..db5bfe7051b37b 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -281,7 +281,17 @@ namespace koszulComplex variable {N : Type v} [AddCommGroup N] [Module R N] +noncomputable def ofList (l : List R) := koszulComplex (Fintype.linearCombination R l.get) + +section functoriality + noncomputable def map (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) : koszulComplex φ ⟶ koszulComplex φ' := sorry +end functoriality + +section specialX + +end specialX + end koszulComplex diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean index 20d27cacebeb4f..db8e66641c21e1 100644 --- a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean +++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean @@ -36,9 +36,8 @@ lemma koszulComplex.range_le_annihilator_homology (i : ℕ) : exact mem_annihilator_homology φ x i lemma koszulComplex.ofList_ideal_annihilator_homology (l : List R) (i : ℕ) : - Ideal.ofList l ≤ Module.annihilator R ((koszulComplex.ofList l).homology i) := by - convert range_le_annihilator_homology _ i - simp + Ideal.ofList l ≤ Module.annihilator R ((ofList l).homology i) := + le_of_eq_of_le (by simp) (range_le_annihilator_homology (Fintype.linearCombination R l.get) i) lemma koszulCocomplex.mem_annihilator_homology (i : ℕ) : φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by From eb56a4602b37a62976861434ab5e1efbf62e42e2 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 19:11:31 +0800 Subject: [PATCH 27/34] update file --- Mathlib/RingTheory/KoszulComplex/Complex.lean | 18 +++++++++++++++++- Mathlib/RingTheory/KoszulComplex/Homotopy.lean | 2 -- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index db5bfe7051b37b..7ea174daf43047 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -21,7 +21,7 @@ public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin universe u v -open ExteriorAlgebra +open CategoryTheory Category MonoidalCategory Limits Module ExteriorAlgebra variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) @@ -292,6 +292,22 @@ end functoriality section specialX +noncomputable def XZeroLinearEquivRing : (koszulComplex φ).X 0 ≃ₗ[R] R := + exteriorPower.zeroEquiv R M + +lemma X_isZero_of_card_generators_le {ι : Type*} [Finite ι] (g : ι → M) + (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) : + IsZero ((koszulComplex φ).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 [koszulComplex, ModuleCat.exteriorPower] using hIsZero + +lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : + IsZero ((ofList l).X i) := X_isZero_of_card_generators_le _ + (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 end koszulComplex diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean index db8e66641c21e1..5a4cdc94016837 100644 --- a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean +++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean @@ -22,8 +22,6 @@ open ExteriorAlgebra variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) (x : M) -#check Homotopy - section homology_annihilator lemma koszulComplex.mem_annihilator_homology (i : ℕ) : From b807f2e7beaa864a4f0121d74a01dd88079a927f Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 21:50:02 +0800 Subject: [PATCH 28/34] some more update(?) --- Mathlib/CategoryTheory/Abelian/Ext.lean | 8 +++++ Mathlib/RingTheory/KoszulComplex/Basic.lean | 10 ++++-- .../RingTheory/KoszulComplex/Cocomplex.lean | 2 +- Mathlib/RingTheory/KoszulComplex/Complex.lean | 6 +++- Mathlib/RingTheory/KoszulComplex/Dual.lean | 35 +++++++++++++++++++ 5 files changed, 56 insertions(+), 5 deletions(-) create mode 100644 Mathlib/RingTheory/KoszulComplex/Dual.lean diff --git a/Mathlib/CategoryTheory/Abelian/Ext.lean b/Mathlib/CategoryTheory/Abelian/Ext.lean index ed6e92f8d8d55d..8809a0ef9d017f 100644 --- a/Mathlib/CategoryTheory/Abelian/Ext.lean +++ b/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 diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean index f7d22ac5de2d72..fc20050c906756 100644 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ b/Mathlib/RingTheory/KoszulComplex/Basic.lean @@ -24,13 +24,17 @@ section change_generators variable [IsNoetherianRing R] [IsLocalRing R] +lemma nonempty_linearEquiv_of_minimal_generators (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) : + ∃ e : (Fin l.length → R) ≃ₗ[R] (Fin l'.length → R), e l.get = l'.get := sorry + theorem koszulCocomplex.nonempty_iso_of_minimal_generators {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 - refine ⟨isoOfEquiv R ?_ ?_⟩ - · sorry - · sorry + obtain ⟨e, h⟩ := nonempty_linearEquiv_of_minimal_generators R I l l' hl hl' hl_min hl'_min + exact ⟨isoOfEquiv R e h⟩ theorem koszulCocomplex.nonempty_iso_of_minimal_generators' {I : Ideal R} {l : List R} (eq : Ideal.ofList l = I) (min : l.length = I.spanFinrank) : diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index 15d02d976305ef..494151f9071f6b 100644 --- a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -13,7 +13,7 @@ public import Mathlib.LinearAlgebra.ExteriorPower.Basis public import Mathlib.RingTheory.Regular.RegularSequence /-! -# Definition of Koszul complex +# Definition of Koszul cocomplex -/ @[expose] public section diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index 7ea174daf43047..7498902049f33a 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -14,7 +14,7 @@ public import Mathlib.RingTheory.Regular.RegularSequence public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin /-! -# The dual of Koszul complex +# Definition of Koszul complex -/ @[expose] public section @@ -277,6 +277,10 @@ noncomputable def koszulComplex : ChainComplex (ModuleCat R) ℕ := (fun n ↦ ModuleCat.ofHom (koszulComplex_aux φ n)) (fun n ↦ by simp [← ModuleCat.ofHom_comp, koszulComplex_aux_comp_eq_zero]; rfl) +section DifferentialGradedAlgebra + +end DifferentialGradedAlgebra + namespace koszulComplex variable {N : Type v} [AddCommGroup N] [Module R N] diff --git a/Mathlib/RingTheory/KoszulComplex/Dual.lean b/Mathlib/RingTheory/KoszulComplex/Dual.lean new file mode 100644 index 00000000000000..8bd69d77468939 --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Dual.lean @@ -0,0 +1,35 @@ +/- +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.RingTheory.KoszulComplex.Complex +public import Mathlib.RingTheory.KoszulComplex.Cocomplex +public import Mathlib.Algebra.Homology.Embedding.Extend +public import Mathlib.CategoryTheory.Abelian.Ext + +/-! +# The dual relation of Koszul complex and cocomplex + +In this file, we prove the dual relation between Koszul complex and cocomplex. +-/ + +#check ComplexShape.Embedding.extendFunctor +set_option pp.universes true in +#check ChainComplex.linearYonedaObj +-- #loogle ComplexShape.Embedding + +@[expose] public section + +universe u v + +open CategoryTheory Functor + +/- `M`is set to be `Type u` to make universe problems easier. -/ +variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (x : M) + + + +-- #check (koszulCocomplex R x).linearYonedaObj R (ModuleCat.of R R) From 7dde300c27a6a8dd53ba6d7dcb4a7ad3013bcc81 Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Wed, 4 Feb 2026 22:32:34 +0800 Subject: [PATCH 29/34] update framework --- Mathlib/RingTheory/KoszulComplex/Basic.lean | 84 ------------------- .../RingTheory/KoszulComplex/Cocomplex.lean | 72 ++++++++++++++++ Mathlib/RingTheory/KoszulComplex/Complex.lean | 73 ++++++++++++++++ 3 files changed, 145 insertions(+), 84 deletions(-) delete mode 100644 Mathlib/RingTheory/KoszulComplex/Basic.lean diff --git a/Mathlib/RingTheory/KoszulComplex/Basic.lean b/Mathlib/RingTheory/KoszulComplex/Basic.lean deleted file mode 100644 index fc20050c906756..00000000000000 --- a/Mathlib/RingTheory/KoszulComplex/Basic.lean +++ /dev/null @@ -1,84 +0,0 @@ -/- -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.RingTheory.KoszulComplex.Complex -public import Mathlib.RingTheory.KoszulComplex.Cocomplex -public import Mathlib.Algebra.Module.SpanRank -public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings - -/-! -# Basic Properties of Koszul complex --/ - -@[expose] public section - -universe u v - -variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] - -section change_generators - -variable [IsNoetherianRing R] [IsLocalRing R] - -lemma nonempty_linearEquiv_of_minimal_generators (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) : - ∃ e : (Fin l.length → R) ≃ₗ[R] (Fin l'.length → R), e l.get = l'.get := sorry - -theorem koszulCocomplex.nonempty_iso_of_minimal_generators {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 - obtain ⟨e, h⟩ := nonempty_linearEquiv_of_minimal_generators R I l l' hl hl' hl_min hl'_min - exact ⟨isoOfEquiv R e h⟩ - -theorem koszulCocomplex.nonempty_iso_of_minimal_generators' {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', Algebra.algebraMap_self, - ModuleCat.hom_add, LinearMap.baseChange_add] - rfl - -open TensorProduct in -def koszulCocomplex.baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : - koszulCocomplex.ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex - (ComplexShape.up ℕ)).obj (koszulCocomplex.ofList R l) := by - refine HomologicalComplex.Hom.isoOfComponents - (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) - · sorry - · sorry - -end basechange - -section IsRegular - -open RingTheory.Sequence - -lemma koszulCocomplex.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 koszulCocomplex.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 IsRegular diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index 494151f9071f6b..a35e5813bdece0 100644 --- a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -7,7 +7,9 @@ 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 @@ -146,4 +148,74 @@ lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : 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 koszulCocomplex.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 koszulCocomplex.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', Algebra.algebraMap_self, + ModuleCat.hom_add, LinearMap.baseChange_add] + rfl + +open TensorProduct in +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 diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index 7498902049f33a..cd7af921e78dba 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -8,6 +8,8 @@ module public import Mathlib.Algebra.Category.ModuleCat.Abelian public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.LinearAlgebra.ExteriorPower.Basis public import Mathlib.RingTheory.Regular.RegularSequence @@ -292,6 +294,9 @@ section functoriality noncomputable def map (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) : koszulComplex φ ⟶ koszulComplex φ' := sorry +noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) : + koszulComplex φ ≅ koszulComplex φ' := sorry + end functoriality section specialX @@ -314,4 +319,72 @@ lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : end specialX +section H0 + +noncomputable def zeroHomologyLinearEquiv (l : List R) : + (ofList l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + +end H0 + +section regular + +open RingTheory.Sequence + +lemma exactAt_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i ≠ 0) : (ofList 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 l ≅ ofList l' := by + have hI : I ≤ Ring.jacobson R := sorry + obtain ⟨e, h⟩ := nonempty_linearEquiv_of_minimal_generators' I hI l l' hl hl' hl_min hl'_min + have h' : Fintype.linearCombination R l'.get ∘ₗ e = Fintype.linearCombination R l.get := by + sorry + exact ⟨isoOfEquiv _ 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 I.finite_generators_of_isNoetherian.toFinset.toList ≅ ofList l := by + refine nonempty_iso_of_minimal_generators ?_ 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', Algebra.algebraMap_self, + ModuleCat.hom_add, LinearMap.baseChange_add] + rfl + +open TensorProduct in +def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + ofList l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex _).obj (ofList l) := by + refine HomologicalComplex.Hom.isoOfComponents + (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) + · sorry + · sorry + +end basechange + end koszulComplex From fa096e29840cab5a2e3e1e06b323850024ce5133 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 5 Feb 2026 11:08:46 +0800 Subject: [PATCH 30/34] fix --- Mathlib/RingTheory/KoszulComplex/Complex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index cd7af921e78dba..fdf7f9b555868f 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -322,7 +322,7 @@ end specialX section H0 noncomputable def zeroHomologyLinearEquiv (l : List R) : - (ofList l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + (ofList l).homology 0 ≃ₗ[R] R ⧸ Ideal.ofList l := sorry end H0 From fa9ed70e1825517a04a74cab8c086384cba39028 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 24 Feb 2026 21:10:42 +0800 Subject: [PATCH 31/34] Delete Basis.lean remove file for correct merge --- .../LinearAlgebra/ExteriorPower/Basis.lean | 100 ------------------ 1 file changed, 100 deletions(-) delete mode 100644 Mathlib/LinearAlgebra/ExteriorPower/Basis.lean diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean deleted file mode 100644 index 96c0b75d5b071f..00000000000000 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ /dev/null @@ -1,100 +0,0 @@ -/- -Copyright (c) 2026 Jingting Wang. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jingting Wang --/ - -module - -public import Mathlib.LinearAlgebra.ExteriorPower.Basic -public import Mathlib.LinearAlgebra.ExteriorPower.Pairing -public import Mathlib.Data.Fin.Tuple.Sort - -/-! -# Basis of exterior power - -In this file we construct a basis of the exterior power `⋀[R]^n M` given a linearly ordered -basis of `M`, and deduce that exterior powers of free modules are free. - -Note: Joel Riou is PRing this at #18771 --/ - -@[expose] public 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 - -/-- 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 - -instance Module.Free.exteriorPower (n : ℕ) [Module.Free R M] : Module.Free R (⋀[R]^n M) := by - classical - let ι := Module.Free.ChooseBasisIndex R M - letI : LinearOrder ι := linearOrderOfSTO (WellOrderingRel (α := ι)) - exact Module.Free.of_basis - (exteriorPower.basis (R := R) (M := M) (ι := ι) (Module.Free.chooseBasis R M) n) - -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 From fb144faebceadead815d94dbae465dbac86ed129 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 24 Feb 2026 21:47:28 +0800 Subject: [PATCH 32/34] fix --- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean index 062d8edf67e13c..418598e599e72a 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean @@ -312,6 +312,7 @@ 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 _) := From 94b4cf1b6a85d0e8437f067ac9516e713e1eff92 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 24 Feb 2026 22:05:17 +0800 Subject: [PATCH 33/34] fix --- .../LinearAlgebra/ExteriorPower/Basis.lean | 77 +++++++++++++++++++ .../RingTheory/KoszulComplex/Cocomplex.lean | 13 +++- Mathlib/RingTheory/KoszulComplex/Complex.lean | 12 +-- 3 files changed, 93 insertions(+), 9 deletions(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 56c78dc9bd226a..5044bf67d05242 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -10,6 +10,7 @@ public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.Order.Extension.Well 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 @@ -185,3 +186,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 diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean index a35e5813bdece0..242dfaf5fd1d11 100644 --- a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -13,6 +13,7 @@ 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 @@ -42,6 +43,7 @@ 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 @@ -70,6 +72,7 @@ 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 _ _ _ _ _ _ @@ -99,6 +102,7 @@ lemma map_id (x y : M) (h : x = y) : 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 = @@ -132,6 +136,7 @@ noncomputable def topXLinearEquivOfBasisOfList (l : List R) : 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 @@ -159,11 +164,11 @@ section regular open RingTheory.Sequence -lemma koszulCocomplex.exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) +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 koszulCocomplex.exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) +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 @@ -204,12 +209,12 @@ 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', Algebra.algebraMap_self, + simp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map', ModuleCat.hom_add, LinearMap.baseChange_add] rfl open TensorProduct in -def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : +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 ↦ ?_) diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean index fdf7f9b555868f..2e02fe6450c0fd 100644 --- a/Mathlib/RingTheory/KoszulComplex/Complex.lean +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -27,6 +27,7 @@ open CategoryTheory Category MonoidalCategory Limits Module ExteriorAlgebra variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R) +set_option backward.isDefEq.respectTransparency false in noncomputable def koszulComplex_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M := exteriorPower.alternatingMapLinearEquiv { toFun x := ∑ i : Fin (n + 1), @@ -83,8 +84,7 @@ noncomputable def koszulComplex_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R have hupdate (z : M) : k.removeNth (Function.update m k z) = k.removeNth m := by ext i simp [Fin.removeNth, Function.update, Fin.succAbove_ne] - simp [term, hremove, LinearMap.map_smul, smul_smul, mul_comm, mul_left_comm, mul_assoc, - hupdate (c • x), hupdate x] + simp [term, hremove, smul_smul, mul_left_comm, hupdate (c • x), hupdate x] · rcases Fin.exists_succAbove_eq (x := p) (y := k) (by simpa [ne_comm] using hk') with ⟨j, rfl⟩ have hupdate (z : M) : @@ -96,7 +96,7 @@ noncomputable def koszulComplex_aux (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R · have hne : k.succAbove i ≠ k.succAbove j := by exact fun h => hi (Fin.succAbove_right_inj.mp h) simp [Fin.removeNth, Function.update, hi, hne] - simp [term, hremove, smul_smul, mul_comm, mul_left_comm, mul_assoc, hupdate (c • x), + simp [term, hremove, smul_smul, mul_comm, hupdate (c • x), hupdate x] have hcalc' : ∑ k, term (Function.update m p (c • x)) k = @@ -273,6 +273,7 @@ lemma koszulComplex_aux_comp_eq_zero (n : ℕ) : -- simpa [term, Finset.smul_sum] using hmain sorry +set_option backward.isDefEq.respectTransparency false in noncomputable def koszulComplex : ChainComplex (ModuleCat R) ℕ := ChainComplex.of (ModuleCat.of R M).exteriorPower @@ -304,6 +305,7 @@ section specialX noncomputable def XZeroLinearEquivRing : (koszulComplex φ).X 0 ≃ₗ[R] R := exteriorPower.zeroEquiv R M +set_option backward.isDefEq.respectTransparency false in lemma X_isZero_of_card_generators_le {ι : Type*} [Finite ι] (g : ι → M) (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) : IsZero ((koszulComplex φ).X i) := by @@ -373,12 +375,12 @@ 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', Algebra.algebraMap_self, + simp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map', ModuleCat.hom_add, LinearMap.baseChange_add] rfl open TensorProduct in -def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : +noncomputable def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : ofList l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex _).obj (ofList l) := by refine HomologicalComplex.Hom.isoOfComponents (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) From fdaaba10d8f338e3236c0db958c1959af62276de Mon Sep 17 00:00:00 2001 From: xyzw12345 Date: Thu, 23 Apr 2026 17:59:52 +0800 Subject: [PATCH 34/34] update Mathlib.lean --- Mathlib.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index b9c99a900a2c95..b219c7cda09739 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6454,9 +6454,9 @@ 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.Basic 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