Here’s a basic problem with infinite bases. Suppose f:R→Rω duplicates its argument ω times. And suppose g:Rω→R sums all ω entries. Now g∘f is not a sensible function.
So you really need to have some restriction. Like for example, maybe we interpret Rω as requiring all but a finite number of entries to be zero. That would at least rule out f. Now Rω is not a “true infinite product” in the category-theory sense. But we would still have Rω≅R⊕Rω (“first” and “rest” of infinite list). Which might enable induction. I’m not sure.
Alternatively we could have Rω be unrestricted, but then g can’t be defined. Either way there’s an issue with allowing functions to or from Rω to be represented by arbitrary infinite matrices.
EDIT: another framing of this is that “infinite product” (Rω unrestricted) and “infinite coproduct” (Rω restricted to all but finite being zero) come apart in Vect. So there isn’t strictly an infinite biproduct.
Here’s a basic problem with infinite bases. Suppose f:R→Rω duplicates its argument ω times. And suppose g:Rω→R sums all ω entries. Now g∘f is not a sensible function.
So you really need to have some restriction. Like for example, maybe we interpret Rω as requiring all but a finite number of entries to be zero. That would at least rule out f. Now Rω is not a “true infinite product” in the category-theory sense. But we would still have Rω≅R⊕Rω (“first” and “rest” of infinite list). Which might enable induction. I’m not sure.
Alternatively we could have Rω be unrestricted, but then g can’t be defined. Either way there’s an issue with allowing functions to or from Rω to be represented by arbitrary infinite matrices.
EDIT: another framing of this is that “infinite product” (Rω unrestricted) and “infinite coproduct” (Rω restricted to all but finite being zero) come apart in Vect. So there isn’t strictly an infinite biproduct.