Timeline for Precise meaning of "picking a basis"?
Current License: CC BY-SA 4.0
Post Revisions
34 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 26 at 19:14 | answer | added | D.R. | timeline score: 4 | |
| Jan 19 at 16:37 | comment | added | Timothy Chow | @IosifPinelis Your first impression was correct. | |
| Jan 19 at 16:13 | comment | added | Iosif Pinelis | Previous comment continued: So, if my latter impression is right, my question now is this: A proof of what specific statement (concerning the trace or otherwise) did you have in mind? | |
| Jan 19 at 16:13 | comment | added | Iosif Pinelis | @TimothyChow : At first I thought that your question "Is it possible to formalize what it means for a proof to pick a basis?" was about a proof in general (even though your question was motivated by the particular blog post about the trace). But then, having looked at your comment, it seems to me that you meant a proof concerning the trace. | |
| Jan 18 at 1:35 | answer | added | Andrej Bauer | timeline score: 12 | |
| Jan 17 at 22:59 | comment | added | Andrej Bauer | @ToddTrimble: I suspect it wouldn't be entirely out of line to explain to the present party the differnce between applying choice and applying existential elimination. | |
| Jan 17 at 22:47 | answer | added | Simon Henry | timeline score: 2 | |
| Jan 17 at 22:38 | comment | added | Todd Trimble | @BenjaminSteinberg In my answer below, you don't need to consider chosen presentations of arbitrary modules $Q$ appearing in transformations of type $P^\ast \otimes_R Q \to \hom_R(P, Q)$. OTOH, projectivity of $P$ is at bottom an existential condition, and there is a trivial sense where any witness to such existence is (in the absence of unique existence) a "choice" of witness, but this is a truism about existential conditions generally; it has nothing to do with "serious choice" qua AC. (If "avoiding choice" means avoiding all existential conditions in proofs, that could be a big ask.) | |
| Jan 17 at 21:57 | vote | accept | Timothy Chow | ||
| Jan 17 at 21:47 | comment | added | Timothy Chow | @AndrejBauer It occurs to me that I took a similar "there's no way to formalize this" attitude toward another MO question. While I still think that's true, it was your own work that came closest. So maybe that will give you some idea of what I'm hoping for here. | |
| Jan 17 at 21:14 | answer | added | Todd Trimble | timeline score: 16 | |
| Jan 17 at 17:35 | comment | added | Benjamin Steinberg | @ToddTrimble, doesn’t the proof of Eilenberg-Watts first prove the natural map is an iso on free modules and then use the 5 lemma writing a free presentation of an arbitrary module. Doesn’t the free presentation involve choice? | |
| Jan 16 at 20:09 | comment | added | Todd Trimble | @JakobWerner Re your first comment: not that I can see. Over a general (let's say commutative) ring $R$, there are abstract reasons for the natural isomorphism $P^\ast \otimes_R - \to \hom_R(P, -)$ when $P$ is finitely generated projective, mainly boiling to down checking that the functor on the right preserves small colimits. There is no choosing a basis at any part of the argument; at least I don't see it, and as I say, f.g. projective modules $P$ generally don't have bases. | |
| Jan 16 at 14:15 | comment | added | Timothy Chow | @AndrejBauer Right, that's why I was hoping for something along the lines of, setting up axioms that capture most of linear algebra, but where "finite-dimensional" vector spaces don't necessarily have a basis. Could be too much to hope for, though. | |
| Jan 16 at 13:18 | comment | added | Andrej Bauer | @TimothyChow: I wish I knew how to formally express "a proof/construction doesn't pick a basis, even temporarily" or even just "this proof does not mention the number 42". Sure, if a proof is construed as a string of symbols, then we can do so, but that's not a mathematically satisfactory notion of proof. | |
| Jan 16 at 9:53 | comment | added | Naïm Camille Favier | I think we can boil down the question further: is it possible to define the product of an unordered pair of elements (of a commutative monoid, say) without "choosing" a first element? I don't see this having a non-philosophical answer. | |
| Jan 16 at 9:48 | comment | added | Naïm Camille Favier | The construction of the sign homomorphism in the Symmetry book uses a similar idea and does not refer to an enumeration (at least not obviously, but since I don't know how to formalise the question it might be that it secretly does in an unavoidable sense). | |
| Jan 16 at 9:13 | comment | added | Lazzaro Campeotti | @JakobWerner: I think that issue was discussed here. | |
| Jan 16 at 5:52 | comment | added | Jakob Werner | Stuff like this happens already much earlier: Instead of asking how to construct a trace operator $\mathrm{End}(V) \to k$ on a finite-dimensional vector space without using an isomorphism $V \cong k^n$ one could e.g. ask how to define a signum homomorphism $\mathrm{Sym}(X) \to \{\pm1\}$ on the symmetric group of a finite set without using an isomorphism $X \cong \{1, \dots, n\}$ at some point. | |
| Jan 16 at 5:41 | comment | added | Jakob Werner | @ToddTrimble In order to show that your map is an ismomorphism, don't you have to choose bases too (similarly and more generally as in the vector space case)? Either a basis of a finitely generated free module of which $P$ is a direct summand, or local bases on a covering of Spec(R) over which $P$ is a trivial vector bundle? | |
| Jan 16 at 3:23 | history | edited | Timothy Chow | CC BY-SA 4.0 |
Clarified my comment about Dedekind-finiteness
|
| Jan 16 at 3:18 | comment | added | Timothy Chow | The question isn't whether the result is basis-invariant, but whether this basis-invariant result admits a definition/proof that doesn't mention bases at all. My question is whether we can formally define "a definition/proof that doesn't mention bases at all." | |
| Jan 16 at 3:06 | comment | added | Timothy Chow | @AndrejBauer Peter LeFanu Lumsdaine put his finger on the matter. More generally, often in mathematics we have a result that is "independent of the choice of X" and yet one of the standard proofs proceeds by picking an X. For example, to define singular homology, we pick an orientation, but the homology group is independent of the choice of orientation. The question naturally arises, if the choice of X doesn't matter, then why are we choosing X in the proof (or definition)? Can we prove/define what we want without referring to X at all? | |
| Jan 16 at 3:04 | comment | added | Todd Trimble | Working over a general commutative ring $R$, one can define the notion of trace for any finitely generated projective module $P$, because the canonical map $P^\ast \otimes_R P \to \hom_R(P, P)$ is an isomorphism: compose its inverse with the evaluation $P^\ast \otimes_R P \to R$. And yet one doesn't "pick a basis" to define the trace there, because finitely generated projective modules do not generally have bases. Also, since fields are von Neumann regular, one can prove that finitely presented modules are projective without picking a basis, so finite presentability could be a good proxy. | |
| Jan 16 at 2:07 | history | became hot network question | |||
| Jan 16 at 0:45 | comment | added | Peter LeFanu Lumsdaine | @AndrejBauer: I read this as exactly trying to pick apart the distinction between ”not dependent on the choice of basis” and ”not needing to pick a basis, even temporarily”. It’s quite a fine distinction, and I don’t know if there’s any space to get a knife-point in there — but if there is, I’d be quite interested to hear it. | |
| Jan 15 at 23:31 | answer | added | Jean Abou Samra | timeline score: 31 | |
| Jan 15 at 23:25 | comment | added | Andrej Bauer | Sorry in the previous comment the condition should have been $\alpha : V \cong \mathbb{R}^n$. Anyhow, assuming a good enough notion of propositions (classical logic will give one), such a pair $(V, t)$ is equivalent to having $V$ satisfying $\exists n .\, V \cong \mathbb{R}^\alpha$. So it really seems to be just "ZF-theorem", provided we use a good enough definition of finite-dimensional. | |
| Jan 15 at 23:17 | comment | added | Andrej Bauer | @Timothy Chow: what's wrong with Kevin's suggestion? I.e., it's a ZF theorem about all pairs $(V, t)$ where $V$ is a vector space and $t$ is an element of the truncation of $\{ (n, \alpha) \mid V \cong \mathbb{R}^n\}$. I thought that was quite reasonable. | |
| Jan 15 at 23:14 | comment | added | Andrej Bauer | It's interesting how Kevin manages to resist the singing of the sirens of constructivism. | |
| Jan 15 at 22:43 | answer | added | Carlo Beenakker | timeline score: 11 | |
| Jan 15 at 19:34 | comment | added | Neil Strickland | I started to write an answer, but then realised that everything that I was going to say was already in Kevin's blog post, which is admirably complete. I suspect that it will be difficult to find anything useful to say that he has not already said. | |
| Jan 15 at 19:17 | answer | added | Iosif Pinelis | timeline score: 9 | |
| Jan 15 at 18:06 | history | asked | Timothy Chow | CC BY-SA 4.0 |