Koszul Complex

Stream: mathlib4

[Nailin Guan]

As I mentioned in the Complete Intersection thread, @Wang Jingting is developing definition and basic properties of Koszul complex. We are following the definition in Eisenbud GTM 150 using exterior power. From this we get a cochain complex. We are also trying to build a chain complex version.
There are some questions here.
1: For the chain complex version, do we want a concrete version or giving the dual some concrete calculation tools are enough?
2: Which one should be named "KoszulComplex" chain/cochain? What should the other one be called?

[Nailin Guan]

Here are some suggestions for our previous attempt I found.
"For Koszul complexes, the better definition is probably using exterior powers, but it will also be important to give concrete formulas (case of a finitely generated free module, induction, etc) which will be useful in computations."

[Joël Riou]

The definitions could be named ChainComplex.koszulComplex and CochainComplex.koszulComplex, or ModuleCat.koszulComplex and ModuleCat.koszulCocomplex?