leanprover-community/lean-liquid

Tensor product of condensed modules

jcommelin opened this issue ยท 0 comments

If ๐’œ is a concrete monoidal abelian category, show that sheaves with values in ๐’œ also form a monoidal abelian category. Prove the tensor-hom adjunction.

In fact, we only need to be able to tensor a condensed abelian group with an ordinary abelian group. This is easier: it can be done componentwise.