diff --git a/Mathlib.lean b/Mathlib.lean index 1374639b55c706..78bc2da011a195 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6474,6 +6474,10 @@ public import Mathlib.RingTheory.Kaehler.Basic public import Mathlib.RingTheory.Kaehler.JacobiZariski public import Mathlib.RingTheory.Kaehler.Polynomial public import Mathlib.RingTheory.Kaehler.TensorProduct +public import Mathlib.RingTheory.KoszulComplex.Cocomplex +public import Mathlib.RingTheory.KoszulComplex.Complex +public import Mathlib.RingTheory.KoszulComplex.Dual +public import Mathlib.RingTheory.KoszulComplex.Homotopy public import Mathlib.RingTheory.KrullDimension.Basic public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.LocalRing diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 5b736544464f5a..4c7555efa22e2e 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -238,6 +238,9 @@ lemma FG.finite_generators {p : Submodule R M} (hp : p.FG) : rw [← Cardinal.lt_aleph0_iff_set_finite, Submodule.generators_card] exact spanRank_finite_iff_fg.mpr hp +instance finite_generators_of_isNoetherian [IsNoetherian R M] (p : Submodule R M) : + p.generators.Finite := FG.finite_generators FG.of_finite + /-- The span of the generators equals the submodule. -/ lemma span_generators (p : Submodule R M) : span R (generators p) = p := (Classical.choose_spec (exists_span_set_card_eq_spanRank p)).2 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/LinearAlgebra/ExteriorPower/Basic.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean index beb5809e99aa93..ce9b43e67a3a42 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean @@ -297,6 +297,15 @@ theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] N') : map n (g ∘ₗ f) = map n g ∘ₗ map n f := by aesop +set_option backward.isDefEq.respectTransparency false in +theorem subtype_comp_map_eq (f : M →ₗ[R] N) : + (Submodule.subtype _) ∘ₗ (map n f) = + (ExteriorAlgebra.map f).toLinearMap ∘ₗ (Submodule.subtype _) := + linearMap_ext <| AlternatingMap.ext fun m ↦ (by simp) + +@[simp] +theorem coe_map (f : M →ₗ[R] N) (x : ⋀[R]^n M) : + map n f x = ExteriorAlgebra.map f x.1 := congr($(subtype_comp_map_eq f) x) /-! Exactness properties of the exterior power functor. -/ /-- If a linear map has a retraction, then the map it induces on exterior powers is injective. -/ diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean index 22abdd2f5ebe9a..1c612884cdb882 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean @@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.ExteriorPower.Basic public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.RingTheory.Finiteness.Subalgebra public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition +public import Mathlib.Data.Fin.Tuple.Sort /-! # Constructs a basis for exterior powers @@ -183,3 +184,79 @@ lemma ιMulti_family_linearIndependent_field {I : Type*} [LinearOrder I] {v : I rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply] end exteriorPower + +section + +universe u v + +variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] + +namespace exteriorPower + +lemma span_ιMulti_orderEmbedding_of_span_eq_top {ι : Type*} [LinearOrder ι] {g : ι → M} + (hg : Submodule.span R (Set.range g) = ⊤) (n : ℕ) : + Submodule.span R (Set.range (fun (x : Fin n ↪o ι) ↦ ιMulti R _ (g ∘ x))) = ⊤ := sorry + +set_option backward.isDefEq.respectTransparency false in +/-- Given a linearly ordered basis `b : Module.Basis ι R M`, the `n`th exterior power `⋀[R]^n M` +has a basis indexed by order embeddings `Fin n ↪o ι`. -/ +noncomputable def basis {ι : Type*} [LinearOrder ι] (b : Module.Basis ι R M) (n : ℕ) : + Module.Basis (Fin n ↪o ι) R (⋀[R]^n M) := by + let e : (Fin n ↪o ι) → ⋀[R]^n M := fun a ↦ ιMulti R n (fun i ↦ b (a i)) + refine Module.Basis.mk (v := e) ?_ ?_ + · refine (linearIndependent_iff).2 fun l hl ↦ Finsupp.ext fun a0 ↦ ?_ + have h₁ (i : ι) : b.coord i (b i) = (1 : R) := by simp [Module.Basis.coord] + have h₀ (i j : ι) (hij : i ≠ j) : b.coord i (b j) = (0 : R) := by simp [Module.Basis.coord, hij] + let φ : ⋀[R]^n M →ₗ[R] R := pairingDual R M n (ιMulti R n (fun i ↦ b.coord (a0 i))) + have hx : φ ((Finsupp.linearCombination R e) l) = 0 := by simpa using congr(φ $hl) + have hx' : φ ((Finsupp.linearCombination R e) l) = l a0 := by + simp only [Finsupp.linearCombination_apply, map_finsuppSum, map_smul] + refine (Finsupp.sum_eq_single a0 ?_ fun ha0 ↦ by simp).trans ?_ + · intro a ha hne + have : φ (e a) = 0 := pairingDual_apply_apply_eq_one_zero b b.coord h₀ n a0 a hne.symm + simp [this] + · have : φ (e a0) = 1 := pairingDual_apply_apply_eq_one b b.coord h₁ h₀ n a0 + simp [this, smul_eq_mul] + exact hx'.symm.trans hx + · let S : Submodule R (⋀[R]^n M) := Submodule.span R (Set.range e) + have mem_S_of_injective (v : Fin n → ι) (hv : Function.Injective v) : + ιMulti R n (b ∘ v) ∈ S := by + let σ : Equiv.Perm (Fin n) := Tuple.sort v + have hmono : Monotone (v ∘ σ) := Tuple.monotone_sort v + have hinj : Function.Injective (v ∘ σ) := hv.comp σ.injective + let a : Fin n ↪o ι := OrderEmbedding.ofStrictMono (v ∘ σ) (hmono.strictMono_of_injective hinj) + have hperm : ιMulti R n (b ∘ v) = Equiv.Perm.sign σ • ιMulti R n (b ∘ a) := by + rw [← Equiv.Perm.sign_inv] + convert AlternatingMap.map_perm (ιMulti R n) (b ∘ a) σ⁻¹ + simp [a, Function.comp_assoc] + rw [hperm] + exact S.smul_mem _ (Submodule.subset_span ⟨a, rfl⟩) + let ψ : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M ⧸ S) := S.mkQ.compAlternatingMap (ιMulti R n) + have hψ : ψ = 0 := by + refine Module.Basis.ext_alternating b fun v hv ↦ ?_ + simpa [ψ] using (Submodule.Quotient.mk_eq_zero S).2 (mem_S_of_injective v hv) + have hrange : Set.range (ιMulti R n (M := M)) ⊆ S := by + rintro _ ⟨m, rfl⟩ + exact (Submodule.Quotient.mk_eq_zero S).1 (show ψ m = 0 from by simp [hψ]) + simpa [S, ιMulti_span R n M] using Submodule.span_le.mpr hrange + +end exteriorPower + +lemma subsingleton_of_card_generators_le {ι : Type*} [Finite ι] (g : ι → M) + (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) : + Subsingleton (⋀[R]^i M) := by + letI : Fintype ι := Fintype.ofFinite ι + letI : LinearOrder ι := LinearOrder.lift' (Fintype.equivFin ι) (Fintype.equivFin ι).injective + have hcard : Fintype.card ι < i := by simpa [Nat.card_eq_fintype_card] using hi + have hempty : IsEmpty (Fin i ↪o ι) := by + refine ⟨fun f ↦ ?_⟩ + absurd f.injective + contrapose hcard + simpa using Fintype.card_le_of_injective f ‹_› + have hbotTop : (⊥ : Submodule R (⋀[R]^i M)) = ⊤ := by + rw [← exteriorPower.span_ιMulti_orderEmbedding_of_span_eq_top (R := R) (M := M) hg i] + convert Submodule.span_empty.symm + exact Set.range_eq_empty_iff.mpr hempty + exact (Submodule.subsingleton_iff R).mp <| (subsingleton_iff_bot_eq_top).mp hbotTop + +end diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean new file mode 100644 index 00000000000000..242dfaf5fd1d11 --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean @@ -0,0 +1,226 @@ +/- +Copyright (c) 2026 Jingting Wang, Nailin Guan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jingting Wang, Nailin Guan +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex +public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading +public import Mathlib.LinearAlgebra.ExteriorPower.Basis +public import Mathlib.RingTheory.Regular.RegularSequence +public import Mathlib.Data.Fin.Tuple.Sort + +/-! +# Definition of Koszul cocomplex +-/ + +@[expose] public section + +universe u v w w' + +open CategoryTheory Category MonoidalCategory Limits Module + +section GradedAlgebra + +variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι] + [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] + {i j k : ι} + +def GradedAlgebra.linearGMul (h : k = i + j) : 𝒜 i →ₗ[R] (𝒜 j →ₗ[R] 𝒜 k) := sorry + +@[simp] +lemma GradedAlgebra.linearGMul_eq_mul (h : k = i + j) (x : 𝒜 i) (y : 𝒜 j) : + (GradedAlgebra.linearGMul 𝒜 h) x y = x.1 * y.1 := sorry + +end GradedAlgebra + +section + +variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] + +set_option backward.isDefEq.respectTransparency false in +variable {M} in +noncomputable def koszulCocomplex (x : M) : CochainComplex (ModuleCat.{max u v} R) ℕ := + CochainComplex.of + (ModuleCat.of R M).exteriorPower + (fun n ↦ ModuleCat.ofHom (GradedAlgebra.linearGMul (fun i : ℕ ↦ ⋀[R]^i M) (add_comm n 1) + ((exteriorPower.oneEquiv R M).symm x))) + (fun n ↦ by + simp only [← ModuleCat.ofHom_comp] + congr + refine LinearMap.ext fun x ↦ Subtype.ext ?_ + simp only [exteriorPower.oneEquiv_symm_apply, LinearMap.coe_comp, Function.comp_apply, + GradedAlgebra.linearGMul_eq_mul, exteriorPower.ιMulti_apply_coe, + ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.ιMulti_zero_apply, mul_one, ← mul_assoc, + CliffordAlgebra.ι_sq_scalar, QuadraticMap.zero_apply, map_zero, zero_mul] + rfl) + +namespace koszulCocomplex + +noncomputable abbrev ofList (l : List R) := + koszulCocomplex R l.get + +instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulCocomplex R x).X i) := + inferInstanceAs <| Module.Free R (⋀[R]^i M) + +variable {M} {N : Type v} [AddCommGroup N] [Module R N] + +section functoriality + +set_option backward.isDefEq.respectTransparency false in +noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) : + koszulCocomplex R x ⟶ koszulCocomplex R y := + CochainComplex.ofHom _ _ _ _ _ _ + (fun i ↦ (ModuleCat.exteriorPower.functor R i).map (ModuleCat.ofHom f)) + (fun i ↦ by + refine ModuleCat.hom_ext <| LinearMap.ext fun z ↦ Subtype.ext ?_ + simp only [ModuleCat.exteriorPower, ModuleCat.exteriorPower.functor_map, + ModuleCat.exteriorPower.map, ModuleCat.hom_ofHom, ModuleCat.hom_comp, LinearMap.coe_comp, + Function.comp_apply, GradedAlgebra.linearGMul_eq_mul, exteriorPower.coe_map, + exteriorPower.oneEquiv_symm_apply, map_mul, exteriorPower.ιMulti_apply_coe, + ExteriorAlgebra.map_apply_ιMulti] + congr + exact funext fun _ ↦ h.symm) + +lemma map_hom (f : M →ₗ[R] N) (x : M) (y : N) (h : f x = y) (i : ℕ) : + (map R f h).f i = (ModuleCat.exteriorPower.functor R i).map (ModuleCat.ofHom f) := rfl + +lemma map_id_refl (x : M) : koszulCocomplex.map R (M := M) .id (Eq.refl x) = 𝟙 _ := by + ext i x + simp only [map_hom, ModuleCat.ofHom_id, ModuleCat.exteriorPower.functor_map, + ModuleCat.exteriorPower.map, ModuleCat.hom_id, exteriorPower.map_id, HomologicalComplex.id_f, + LinearMap.id_coe, id_eq] + rfl + +lemma map_id (x y : M) (h : x = y) : + koszulCocomplex.map R (M := M) .id h = eqToHom (by rw [h]) := by + subst h + exact map_id_refl R x + +set_option backward.isDefEq.respectTransparency false in +lemma map_comp {P : Type v} [AddCommGroup P] [Module R P] + (f : M →ₗ[R] N) (g : N →ₗ[R] P) {x : M} {y : N} {z : P} (hxy : f x = y) (hyz : g y = z) : + koszulCocomplex.map R f hxy ≫ koszulCocomplex.map R g hyz = + koszulCocomplex.map R (g ∘ₗ f) (hxy ▸ hyz : g (f x) = z) := by + refine HomologicalComplex.hom_ext _ _ fun i ↦ ?_ + simp only [HomologicalComplex.comp_f, map_hom, ModuleCat.ofHom_comp, Functor.map_comp] + +noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) : + koszulCocomplex R x ≅ koszulCocomplex R y where + hom := koszulCocomplex.map R f h + inv := koszulCocomplex.map R f.symm (f.injective (by simpa using h.symm)) + hom_inv_id := by + simp only [map_comp, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm, + LinearEquiv.refl_toLinearMap] + exact map_id_refl R x + inv_hom_id := by + simp only [map_comp, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, + LinearEquiv.refl_toLinearMap] + exact map_id_refl R y + +end functoriality + +section specialX + +noncomputable def topXLinearEquivOfBasis {ι : Type*} [Finite ι] [LinearOrder ι] (x : M) + (b : Basis ι R M) : (koszulCocomplex R x).X (Nat.card ι) ≃ₗ[R] R := by sorry + +noncomputable def topXLinearEquivOfBasisOfList (l : List R) : + (ofList R l).X l.length ≃ₗ[R] R := by + have : l.length = Nat.card (Fin l.length) := by simp + rw [this] + exact topXLinearEquivOfBasis R l.get (Pi.basisFun R (Fin l.length)) + +set_option backward.isDefEq.respectTransparency false in +lemma X_isZero_of_card_generators_le (x : M) {ι : Type*} [Finite ι] (g : ι → M) + (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) : + IsZero ((koszulCocomplex R x).X i) := by + have hIsZero : IsZero (ModuleCat.of R (⋀[R]^i M)) := by + apply ModuleCat.isZero_of_iff_subsingleton.mpr + exact subsingleton_of_card_generators_le R M g hg i hi + simpa [koszulCocomplex, ModuleCat.exteriorPower] using hIsZero + +lemma ofList_X_isZero_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) : + IsZero ((koszulCocomplex.ofList R l).X i) := + X_isZero_of_card_generators_le R l.get + (Pi.basisFun R (Fin l.length)) (Pi.basisFun R (Fin l.length)).span_eq i + (by simpa [Nat.card_eq_fintype_card] using hi) + +end specialX + +section Htop + +noncomputable def topHomologyLinearEquiv (l : List R) : + (ofList R l).homology l.length ≃ₗ[R] R ⧸ Ideal.ofList l := sorry + +end Htop + +section regular + +open RingTheory.Sequence + +lemma exactAt_of_lt_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i < rs.length) : (koszulCocomplex.ofList R rs).ExactAt i := by + sorry + +theorem exactAt_of_ne_length_of_isRegular (rs : List R) (reg : IsRegular R rs) + (i : ℕ) (lt : i ≠ rs.length) : (koszulCocomplex.ofList R rs).ExactAt i := by + sorry + +end regular + +section change_generators + +lemma nonempty_linearEquiv_of_minimal_generators (I : Ideal R) (hI : I ≤ Ring.jacobson R) + (l l' : List R) (hl : Ideal.ofList l = I) (hl' : Ideal.ofList l' = I) + (hl_min : l.length = I.spanFinrank) (hl'_min : l'.length = I.spanFinrank) : + ∃ e : (Fin l.length → R) ≃ₗ[R] (Fin l'.length → R), e l.get = l'.get := sorry + +theorem nonempty_iso_of_minimal_generators [IsLocalRing R] + {I : Ideal R} {l l' : List R} + (hl : Ideal.ofList l = I) (hl' : Ideal.ofList l' = I) + (hl_min : l.length = I.spanFinrank) (hl'_min : l'.length = I.spanFinrank) : + Nonempty <| ofList R l ≅ ofList R l' := by + have hI : I ≤ Ring.jacobson R := sorry + obtain ⟨e, h⟩ := nonempty_linearEquiv_of_minimal_generators R I hI l l' hl hl' hl_min hl'_min + exact ⟨isoOfEquiv R e h⟩ + +theorem nonempty_iso_of_minimal_generators' + [IsNoetherianRing R] [IsLocalRing R] {I : Ideal R} {l : List R} + (eq : Ideal.ofList l = I) (min : l.length = I.spanFinrank) : + Nonempty <| ofList R I.finite_generators_of_isNoetherian.toFinset.toList ≅ ofList R l := by + refine nonempty_iso_of_minimal_generators R ?_ eq ?_ min + · simp only [Ideal.ofList, Finset.mem_toList, Set.Finite.mem_toFinset, Set.setOf_mem_eq] + exact I.span_generators + · simp only [Finset.length_toList, ← Set.ncard_eq_toFinset_card _ _] + exact Submodule.FG.generators_ncard Submodule.FG.of_finite + +end change_generators + +section basechange + +variable (S : Type (max u v)) [CommRing S] (f : R →+* S) + +instance (T : Type v) [CommRing T] (g : R →+* T) : + (ModuleCat.extendScalars.{u, v, u} g).Additive where + map_add {X Y a b} := by + simp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map', + ModuleCat.hom_add, LinearMap.baseChange_add] + rfl + +open TensorProduct in +noncomputable def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + ofList S l' ≅ ((ModuleCat.extendScalars f).mapHomologicalComplex _).obj (ofList R l) := by + refine HomologicalComplex.Hom.isoOfComponents + (fun i ↦ LinearEquiv.toModuleIso ?_) (fun i j ↦ ?_) + · sorry + · sorry + +end basechange + +end koszulCocomplex diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean new file mode 100644 index 00000000000000..2e02fe6450c0fd --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean @@ -0,0 +1,392 @@ +/- +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.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 +public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin + +/-! +# Definition of Koszul complex +-/ + +@[expose] public section + +universe u v + +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), + ((-1) ^ i.1 * (φ (x i))) • exteriorPower.ιMulti R n (x ∘ i.succAbove) + 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, 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) : + 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, 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 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 + +set_option backward.isDefEq.respectTransparency false in +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 DifferentialGradedAlgebra + +end DifferentialGradedAlgebra + +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 + +noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) : + koszulComplex φ ≅ koszulComplex φ' := sorry + +end functoriality + +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 + 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 + +section H0 + +noncomputable def zeroHomologyLinearEquiv (l : List R) : + (ofList l).homology 0 ≃ₗ[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', + ModuleCat.hom_add, LinearMap.baseChange_add] + rfl + +open TensorProduct in +noncomputable def baseChange_iso (l : List R) (l' : List S) (eqmap : l.map f = l') : + ofList 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 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) diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean new file mode 100644 index 00000000000000..5a4cdc94016837 --- /dev/null +++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean @@ -0,0 +1,54 @@ +/- +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) (x : M) + +section homology_annihilator + +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 ((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 + sorry + +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] + 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 φ l.get i + +end homology_annihilator