update mathlib + finish DualKoszulComplex + update blueprint names

Author: pink10000

LeanCommAlg/Koszul.lean

@@ -106,84 +106,31 @@ def KoszulComplex (a : M) [Module R M] : CochainComplex (ModuleCat R) ℕ := {
   d_comp_d' := by
     intro i _ _ hij hjk
     simp at hij hjk; subst hij hjk; simp
-    have conv (j : ℕ) (a : ⋀[R]^j M →ₗ[R] ⋀[R]^(j + 1) M) (b : ⋀[R]^(j + 1) M →ₗ[R] ⋀[R]^(j + 2) M) :
-        ofHom a ≫ ofHom b = ofHom (b ∘ₗ a) := rfl
-    rw [conv]
-    have : i + 1 + 1 = i + 2 := rfl; rw [this]; clear this
+    rw [← @ofHom_comp]
+    have : i + 1 + 1 = i + 2 := rfl; rw [this];
     rw [koszul_d_squared_zero i a]
     rfl
 }
 
 -- Self-duality of the Koszul Complex
 variable {E : Type*} [AddCommGroup E] [Module R E] [Module.Free R E] [Module.Finite R E]
+variable [ CommMonoid (ExteriorAlgebra R E)]
 
-noncomputable def rank_E : ℕ := (Module.rank R E).toNat
-def aux_KoszulComplex (e : E) : CochainComplex (ModuleCat R) ℕ := KoszulComplex e
-
--- im not sure how to "take the dual"
--- i know you have to do `Hom(-, R)` but i dont know how to do that in lean
--- hence, the definition is not complete
 #check Module.Dual R (⋀[R]^2 E)
-
 #check (Module.Free R E)
-
--- Aluffi Lemma 8.4.3
-lemma rank_free_wedge :
-    (Module.rank R (⋀[R]^ℓ E)).toNat = Nat.choose ((Module.rank R E).toNat) ℓ := by
-  sorry
-
-
-noncomputable def dual_is_rank_minus_power (i : ℕ) :
-    (⋀[R]^i E) ≃ₗ[R] Module.Dual R (⋀[R]^((Module.rank R E).toNat - i) E)  := by
-  generalize rankh : (Module.rank R E).toNat = r
-  have E_basis := Module.Free.chooseBasis R E
-  -- need to get some a ∈ ⋀[R]^i E
-  -- need to get some b ∈ ⋀[R]^(r - i) E
-  -- multiply them together
-  -- show the result is in ⋀[R]^r E ≃ R
-  -- so a ^ b = r
-  unfold Module.Dual
-
-
-  apply LinearEquiv.ofBijective
-  . case hf =>
-
-    sorry
-  . case f =>
-    apply LinearMap.mk
-    . case _ =>
-      intro m x
-
-
-    sorry
-
-
-
-
-noncomputable def dual_ext_comm (j : ℕ) :
-    Module.Dual R (⋀[R]^j E) ≃ₗ[R] ⋀[R]^j (Module.Dual R E) := by
-  sorry
-
-def dual_rank_comm (i : ℕ) :
-    (⋀[R]^i E) → ⋀[R]^((Module.rank R E).toNat - i) (Module.Dual R E) := by
-  sorry
-
+#check exteriorPower.zeroEquiv
+#check exteriorPower.oneEquiv
 
 def DualKoszulComplex (e : E) : ChainComplex (ModuleCat R) ℕ := {
-  X := (fun i => of R (⋀[R]^i M)),
-  d := fun i j => if i == j + 1 then ofHom (diff_map i j e) else 0,
-  shape := fun i j h => by
-    simp_all
-    sorry
-  ,
+  X := fun i => of R (Module.Dual R (⋀[R]^i E)),
+  d := fun i j => if j + 1 == i then @ofHom R _ _ _ _ _ _ _ (LinearMap.dualMap (diff_map j i e)) else 0,
+  shape := fun i j h => by simp_all,
   d_comp_d' := by
-    intro i _ _ hij hjk
+    intro _ _ k hij hjk
     simp at hij hjk; subst hij hjk; simp
-    have conv (j : ℕ) (a : ⋀[R]^j M →ₗ[R] ⋀[R]^(j + 1) M) (b : ⋀[R]^(j + 1) M →ₗ[R] ⋀[R]^(j + 2) M) :
-        ofHom a ≫ ofHom b = ofHom (b ∘ₗ a) := rfl
-    -- rw [conv]
-    sorry
-    -- have : i + 1 + 1 = i + 2 := rfl; rw [this]; clear this
-    -- rw [koszul_d_squared_zero i a]
-    -- rfl
+    rw [← @ofHom_comp]
+    have : k + 1 + 1 = k + 2 := rfl; rw [this]; clear this
+    rw [LinearMap.dualMap_comp_dualMap, koszul_d_squared_zero k e]
+    rw [LinearMap.dualMap_eq_lcomp, LinearMap.lcomp, LinearMap.comp_zero]
+    rfl
 }

blueprint/src/koszul.tex

@@ -21,8 +21,8 @@ \subsection{Koszul complex}
 \end{proposition}
 
 
-\begin{definition}[koszul_complex]
-	\label{def:koszul_complex}
+\begin{definition}[KoszulComplex]
+	\label{def:KoszulComplex}
 	\leanok
 	\uses{def:ExteriorAlgebra}
 	Let $R$ be a (Noetherian?) ring, $M$ be an (finitely generated?) $R$-module and $a \in M$.
@@ -36,8 +36,9 @@ \subsection{Koszul complex}
 \end{definition}
 
 \begin{definition}[Dual Koszul complex]
-	\label{def:koszul_complex_dual}
-	\uses{def:koszul_complex}
+	\label{def:DualKoszulComplex}
+	% \leanok
+	\uses{def:KoszulComplex}
 	If $M \cong R^m$ is a free $R$-module, then applying the contravariant functor $\operatorname{Hom}_R(\ , R)$ gives us an isomorphic chain complex 
 	$$K_{\bullet}(a) :\begin{tikzcd}
 	\bigwedge^{i+1}_R R^m \arrow[r, "d_{i+1}"] & \bigwedge^i_R R^m \arrow[r, "d_i"] & \bigwedge^{i-1}_R R^m \arrow[r] & \dots R^m \arrow[r, "d_1"] & R \arrow[r] & 0
@@ -53,7 +54,7 @@ \subsection{Koszul complex}
 
 \begin{lemma}
 	\label{lem:koszul_of_length_2}
-	\uses{def:koszul_complex_dual}
+	\uses{def:DualKoszulComplex}
 	$K(x)$ is exact exept for the rightmost side iff $x$ is regular.
 \end{lemma}
 
@@ -127,13 +128,13 @@ \subsection{Koszul complex}
 \end{corollary}
 
 \begin{lemma}
-	\label{thm:koszul_complex_res_quotient_ring}
+	\label{thm:KoszulComplex_res_quotient_ring}
 	\uses{def:free_resl}
 \end{lemma}
 
 \begin{lemma}
 	\label{lem:tor_measures_koszul_homology}
-	\uses{thm:koszul_complex_res_quotient_ring}
+	\uses{thm:KoszulComplex_res_quotient_ring}
 	$$H_i(K(a) \otimes M) \cong \tor_i^R (R/(a), M)$$
 \end{lemma}
 
@@ -165,7 +166,7 @@ \subsection{Koszul complex}
 
 \begin{lemma}
 	\label{lem:koszul_homotopy}
-	\uses{def:koszul_complex_dual}
+	\uses{def:DualKoszulComplex}
 \end{lemma}
 
 \begin{proposition}

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b00f62e9c1e9a582666b555d055d890c4a56149",
+   "rev": "8d0660f3c507e19b8e729894cd0be53c2b1c73f5",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -55,10 +55,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
+   "rev": "322a050322e97b0a701588d9b1efbe2bee7f8527",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.52-pre",
+   "inputRev": "v0.0.52-pre2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "309e155d9f70a477768c434ce015ad784deb094f",
+   "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",