tensor product of a complex by module

Stream: Is there code for X?

[Sarah El Boustany]

Is there code for the tensor product of a complex by module?

[Kevin Buzzard]

Can you be more precise? Is the complex a complex of modules for the same ring? Is the ring commutative? (i.e. is the tensor product also a complex of modules or a complex of abelian groups)? I am only asking these questions because I don't know the answer to your question in any of these situations :-/ but formalization will care.

[Sarah El Boustany]

Specifically, I am looking at $k$ a commutative ring, $A$ a $k$-algebra, $M$ an $A$-bimodule (equivalently a right module over the enveloping algebra of $A$), and I want to tensor the bar resolution of $A$ by $M$ over the enveloping algebra of $A$. So it's a complex for the same ring, but the ring is not necessarily commutative (as far as I understand - I am still pretty new to this field)

[Matthew Ballard]

By enveloping in this context you mean $A^{\operatorname{op}} \otimes_k A$, is that right?

[Sarah El Boustany]

Yes

[Matthew Ballard]

@Joël Riou will know best but docs#HomologicalComplex.coinvariantsTensorObj is a good place to start poking around

[Sarah El Boustany]

Thank you very much!

[Joël Riou]

We have the alternating (co)face map complex of a (co)simplicial object https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.html but I do not think we have the simplicial object which sends n to the (n +1) tensor power of the k-algebra A.

[Sarah El Boustany]

Thank you, I will look into this tomorrow!