You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
James Gilles (Dec 12 2024 at 17:51):Pardon me, this is probably a naive question.
One of the archetypal examples of a natural isomorphism is that of a finite-dimensional vector space to its double dual. I'd never actually sat down and thought about this until recently. The natural map in one direction is obvious, . But I couldn't think of how to construct an inverse.
M.O. says you don't construct the inverse. You just prove injectivity, and that the two spaces are the same dimension, therefore the spaces are isomorphic. This makes perfect sense to me on a set-theoretic level. But I still don't see how to actually construct the inverse, to show that the map is an isomorphism in a category-theoretic sense.
Is there just some linear algebra algorithm I'm forgetting about? Any algorithm seems like it would require a basis...
Is there some categorical property of f.d.Vec we're using here? Some sort of dependently-typed map (f: V -> W, injective(f), same_dimension(src(f), tgt(f))) -> (f^{-1}: W -> V)? Or should we consider the double dual isomorphism an "axiom" of f.d.Vec, a fundamental property?
Or, do these questions depend on fiddly foundational details?
Nathan Corbyn (Dec 12 2024 at 17:58):Remember that ‘finite dimensional vector space’ means vector space for which there exists a natural number and a linear isomorphism with (where is your base field). This is equivalent to the existence of a finite basis. Armed with a basis, it should be ok to write down the inverse.
James Gilles (Dec 12 2024 at 17:59):Ahh, that's it. Makes sense, thanks.
James Gilles (Dec 12 2024 at 18:01):I guess I was confused because I was thinking of "the category of finite-dimensional-vector spaces equipped with bases" as distinct from "the category of finite-dimensional vector spaces that CAN be equipped with bases". You have to invoke choice to get from the second to the first, right?
Mike Shulman (Dec 12 2024 at 18:02):You have to invoke choice to get a functor from the second to the first. But when proving that some map you already have is an isomorphism, you don't need choice to choose one thing that you know exists.
James Gilles (Dec 12 2024 at 18:32):Ah, I see, this is just the elimination rule for the existential quantifier in a proof assistant. The type of the result doesn't depend on the basis, so we can apply Exists.elim -- and in this case, there's only one choice for the result, so it doesn't depend on the basis at all. Thanks!