Zulip Chat Archive

Stream: maths

Topic: basis.tensor_product


Jakob von Raumer (Aug 25 2021 at 11:45):

What does basis.tensor_product do in linear_algebra.finsupp_vector_space? It's neither about modules which are necessarily vector spaces, nor about finiteness...

Anne Baanen (Aug 25 2021 at 11:49):

IIRC, the definitions in finsupp_vector_space.lean are finsupp-specific results that can't go in finsupp.lean because they depend on basis.lean, which depends on finsupp.lean.

Anne Baanen (Aug 25 2021 at 11:50):

In this case, looks like docs#finsupp.basis.tensor_product depends on docs#finsupp.basis_single_one, which is a basis for finsupp.

Jakob von Raumer (Aug 25 2021 at 11:55):

But basis.tensor_product itself isn't about finsupp at all, so why not put it in linear_algebra.tensor_product?

Anne Baanen (Aug 25 2021 at 12:06):

I don't know, and I think moving the definition should be a good idea, if the imports allow it. Looks like #3147 introduced basis.tensor_product, and there was no discussion on where to put it.

Jakob von Raumer (Aug 25 2021 at 12:09):

In a similar vein, finite_dimensional is lacking some instances, for products and, derived from that, for tensor products, right? Or am I just missing them?

Anne Baanen (Aug 25 2021 at 12:12):

I can't find them, no :/

Anne Baanen (Aug 25 2021 at 12:14):

I would like a big cleanup of some of those files in linear_algebra anyway, since I'm always having a lot of trouble finding things.

Jakob von Raumer (Aug 30 2021 at 11:00):

Might also be good to rename basis.ext, since it's not extensionality of bases but of linear maps..


Last updated: Dec 20 2023 at 11:08 UTC