Timeline for answer to Precise meaning of "picking a basis"? by Jean Abou Samra
Current License: CC BY-SA 4.0
Post Revisions
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 3 at 19:04 | comment | added | Iosif Pinelis | @TimothyChow : In view of my latest comment in this thread, right above, I am wondering why you accepted this answer. | |
| Jan 29 at 19:49 | comment | added | Iosif Pinelis | Previous comment continued: So, I do not see how your answer addresses the posted question at all. I also do not see in your answer examples of potential use of "a function which assigns to each finite-dimensional vector space the trace operator on it". | |
| Jan 29 at 19:49 | comment | added | Iosif Pinelis | Previous comment continued: On the other hand, in your answer you wrote: 'rather we are defining a function which assigns to each finite-dimensional vector space the trace operator on it. This is so that when we are working with lots of vector spaces at the same time (say a vector bundle), we can write things like "the function mapping $x$ to the trace of the endomorphism $\ell(x)$ of $E(x)$."' In doing so, you are talking specifically about the trace operator and you are explicitly using the standard basis-based construction. | |
| Jan 29 at 19:48 | comment | added | Iosif Pinelis | Previous comment continued: Moreover, in the later comment by the OP my impression that the posted "question [...] was about a proof in general (even though [the] question was motivated by the particular blog post about the trace)" was apparently confirmed by the OP. The emphases in both quotes are mine -- I.P. | |
| Jan 29 at 19:48 | comment | added | Iosif Pinelis | @JeanAbouSamra : The OP wrote in a comment: 'My question is whether we can formally define "a definition/proof that doesn't mention bases at all."' | |
| Jan 29 at 14:26 | comment | added | Jean Abou Samra | @IosifPinelis The construction absolutely is the standard one; I haven't claimed it is special, only clarified that it doesn't need the axiom of choice but does need unique choice. | |
| Jan 24 at 10:23 | comment | added | Gro-Tsen | Re “unique choice”, it might be relevant to point out, as I like to do, that the axiom of choice over ZF is equivalent to the assertion that for any set $X$ and equivalence relation $\sim$, the obvious injective map $X^I/(\sim^I) \to (X/{\sim})^I$ is a bijection: so one shouldn't get the idea that “whenever there's no actual choice to be made, it's provable in ZF (let alone constructively)”. Whether this is related to the problem at hand isn't clear to me, however. | |
| Jan 20 at 17:07 | comment | added | Andrej Bauer | @TimothyChow: after some thinking (at 2am) I think I wrote up a construction that minimizes any "picking a basis" by relying on a characterization of trace. Finite dimensionality is only used in the proof that a certain set is a singleton, so inside a logical proposition, after the construction has been carried out. HoTT people will of course recognize the usual tricks involving truncation and contractibility, but my answer hides all that in a hole and covers it with a layer of leaves and branches. | |
| Jan 19 at 16:57 | comment | added | Iosif Pinelis | Previous comment continued: Also, modulo universally accepted unique choice, I don't see how your construction of the trace differs from the usual basis-based construction. | |
| Jan 19 at 16:57 | comment | added | Iosif Pinelis | @JeanAbouSamra : I guess now that you actually prove, not that "there exists a unique operator [...]", but that the set $A_{k,E}$ of all operators with this property is a singleton set, right? OK, but this distinction is zero modulo unique choice, which I think you said is universally accepted. Also, your proof explicitly uses bases $\mathscr B$. So, I do not understand how this proof(?)/construction(?) can be considered basis-free (if that was your intent). | |
| Jan 19 at 16:46 | comment | added | Jean Abou Samra | @IosifPinelis "Define $\operatorname{Tr}_{k, E}$ as the unique operator such that …" is an implicit application of unique choice. If you unravel this down to the level of axioms, you will find exactly what I said. | |
| Jan 19 at 16:35 | comment | added | Iosif Pinelis | @JeanAbouSamra : You already proved that for each $(k,E)$ there is a unique $\text{Tr}_{k,E}$ with this property. Why do you need then to form the singleton set $\{\text{Tr}_{k,E}\}$ and after all go back to $\text{Tr}_{k,E}$? | |
| Jan 19 at 16:28 | comment | added | Jean Abou Samra | @IosifPinelis The property of $\operatorname{Tr} : \operatorname{End}(E) \to k$ is: for all basis $\mathcal{B}$ and for all linear map $\ell \in \operatorname{End}(E)$, the scalar $\operatorname{Tr}(\ell)$ equals the sum of diagonal elements of the matrix of $\ell$ in the basis $\mathcal{B}$. | |
| Jan 19 at 16:03 | comment | added | Iosif Pinelis | @JeanAbouSamra : Thank you for your response. At this point, I have one further question, concerning "the set of operators with this property": What do you mean by "this property"? | |
| Jan 19 at 12:35 | comment | added | Jean Abou Samra | @IosifPinelis In the construction of the trace using unique choice, you first prove that for each field $k$ and for each finite-dimensional $k$-vector space $E$, there exists a unique operator $\operatorname{Tr} : \operatorname{End}(E) → k$ such that for all basis $ℬ$ of $E$ and for all linear map $ℓ ∈ \operatorname{End}(E)$, the scalar $\operatorname{Tr}(ℓ)$ equals the sum of diagonal elements of the matrix of $ℓ$ in the basis $ℬ$. Now let $A_{k, E}$ be the set of operators with this property, and apply unique choice to the (proper class sized) family of singletons $(A_{k, E})$. | |
| Jan 19 at 12:28 | comment | added | Jean Abou Samra | @IosifPinelis Here $x$ ranges over some set $X$, $E$ is some family of finite-dimensional $ℝ$-vector spaces indexed by the elements of $X$ (e.g., $X$ could be a differentiable manifold and $E(x)$ the tangent space of $X$ at $x ∈ X$), and each $ℓ(x)$ is some endomorphism of $E(x)$. The point is simply that it is not enough for all mathematical purposes to be able to work with the trace operator on a single vector space at a time. | |
| Jan 19 at 3:58 | comment | added | Iosif Pinelis | @JeanAbouSamra : When you say "$x$ to the trace of the endomorphism $ℓ(x)$ of $E(x)$", what do you mean here by $x$, $ℓ$, and $E$? Also, what are the singleton sets $A_i$ in this case (I guess $i=x$)? | |
| Jan 17 at 22:36 | comment | added | Andrej Bauer | The calculus of inductive constructions (used by Rocq and Lean) lacks unique choice. This was used advantageously by Yannick Forster in his thesis to develop synthetic computability with classical logic (because even though classical logic can show that the graph of the halting oracle exists, once needs unique choice to get the corresponding function). Anyhow Jean's answer gives me an idea but I have to think about it. | |
| Jan 17 at 21:57 | vote | accept | Timothy Chow | ||
| Jan 17 at 21:48 | comment | added | Jean Abou Samra | (So you can use a proof in a construction to discard impossible cases, to cast between equal types, and to do well-founded recursion.) It's a priori conceivable that the trace could be constructed with something like "define the trace of an endomorphism $A : E → E$ as … where the last case is impossible because $E$ is finite-dimensional". I'm pretty sure it's not possible, but it would take some work to actually prove it. (I do wonder if a parametricity argument would do the trick, but I'm in unknown territory there.) | |
| Jan 17 at 21:45 | comment | added | Jean Abou Samra | @TimothyChow Yes, I think that's reasonable. Obviously the answer will depend on what your exact logic is. If you don't have any other way of using proofs in constructions then obviously there's no way to make use of the hypothesis that the space is finite-dimensional. In Lean (and Rocq), what you do have is syntactic subsingleton elimination, of which the main cases are falsity, equality and accessibility. | |
| Jan 16 at 3:21 | comment | added | Timothy Chow | Very illuminating answer. Can I infer that if one could make precise sense of "mathematics without unique choice," then the question might be rephrased as, "can the trace on a finite-dimensional space be defined (or constructed?) in mathematics without unique choice?"? | |
| Jan 15 at 23:31 | history | answered | Jean Abou Samra | CC BY-SA 4.0 |