Zulip Chat Archive

I take this opportunity to ask another question. Does anyone have an idea to define the trace of an endomorphism of a vector space of finite dimension. We can define the trace for an endomorphism of a vector space provided with a base and prove that this trace is independent of the base. But is there a way to forget the reference to the base ?

Kevin Buzzard (May 24 2020 at 19:14):

It's the unique linear map with some properties

Kevin Buzzard (May 24 2020 at 19:15):

It sends an idempotent to its rank and it's linear

orlando (May 24 2020 at 19:17):

oh i never see this caracterisation !!!

Kevin Buzzard (May 24 2020 at 19:17):

I'm not sure it helps you though :-)

Kevin Buzzard (May 24 2020 at 19:17):

It's also the sum of the eigenvalues!

Alex J. Best (May 24 2020 at 19:18):

One definition is via $Hom(V,V) \cong V\otimes V^* \to k$ , the last map is contraction, evaluating a dual vector at a vector

Kevin Buzzard (May 24 2020 at 19:21):

Wait

Kevin Buzzard (May 24 2020 at 19:21):

(got it)

Reid Barton (May 24 2020 at 19:22):

I think it's also the coefficient of $t$ in $\det (1 + tA)$

Kevin Buzzard (May 24 2020 at 19:23):

Right, but det also wants to be defined via choosing a basis

Reid Barton (May 24 2020 at 19:23):

ok but we already have det for an endomorphism I think :upside_down:

Reid Barton (May 24 2020 at 19:23):

Or at least, I heard we were going to

Kevin Buzzard (May 24 2020 at 19:24):

Alex's definition is one of these phenomena I've never understood properly. There's a natural map from $V\otimes V^*$ to $Hom(V,V)$ , which in the finite-dimensional case is an isomorphism (and which isn't an isomorphism otherwise). In the finite-dimensional case you can hence take its inverse.

orlando (May 24 2020 at 19:24):

hum @Reid Barton i don't see ( in lean) det for endomorphism !

Reid Barton (May 24 2020 at 19:24):

Yeah, maybe it was a false rumor.

Kevin Buzzard (May 24 2020 at 19:25):

In Langlands' paper on abelian local and global Langlands he pulls this trick off a couple of times. There is a map which is computable, and by a hard theorem it's a bijection, and then he merrily uses the inverse when doing calculations, but it's impossible to unravel them because the proof that it's a bijection is nonconstructive

Kevin Buzzard (May 24 2020 at 19:26):

If we're doing vector spaces over a field $k$ and we put the discrete norm on $k$ , then $V\otimes V^*$ corresponds to precisely the trace class endomorphisms in $Hom(V,V)$ , so the leap of faith is the assertion that every endomorphism is trace class

Reid Barton (May 24 2020 at 19:30):

Anyways the right way to give a direct definition like this (which we never do in mathlib AFAIK) is to prove the trace is independent of the choice of basis, then use unique choice to choose a value which is the trace of the matrix in some basis

Reid Barton (May 24 2020 at 19:31):

or equivalently, use unique choice to get a trunc ([basis for V]) and then use trunc.lift to get out the trace

Kevin Buzzard (May 24 2020 at 19:32):

Are you explaining how to make it computable or something? What do you mean by the "right" way?

Reid Barton (May 24 2020 at 19:33):

It won't be computable (ever?)

Reid Barton (May 24 2020 at 19:34):

this way it's obviously independent of the choice of basis, and theoretically a tactic could see this and prove that the trace of the corresponding endomorphism of an isomorphic vector space is equal

Reid Barton (May 24 2020 at 19:34):

It's also the right way in the sense that this is how mathematicians make definitions

Bryan Gin-ge Chen (May 24 2020 at 19:35):

Didn't we have to deal with something like this when we defined the dimension of a vector space?

Sebastien Gouezel (May 24 2020 at 19:35):

The right way is really to use the identification with $V \otimes V^*$ to define the trace of a finite-rank endomorphism, without assuming that the space is finite-dimensional.

Reid Barton (May 24 2020 at 19:36):

I think for the dimension of a vector space mathlib uses a more ad-hoc trick, like the minimum cardinality of a basis

Kevin Buzzard (May 24 2020 at 19:37):

The right way is to set up the theory of trace class endomorphisms of projective normed modules over normed rings, and then apply the theory in the case where the normed ring is a field with the discrete norm

Sebastien Gouezel (May 24 2020 at 19:37):

If $A$ is finite-rank and $B$ is anything, then you have the formula $Tr(AB)=Tr(BA)$ . Finite-dimensionality is not really relevant.

Kevin Buzzard (May 24 2020 at 19:37):

The right way is to show this for A compact and B anything

Sebastien Gouezel (May 24 2020 at 19:38):

Compact operators are not always trace-class...

Kevin Buzzard (May 24 2020 at 19:38):

Oh obviously I am assuming the norm is non-archimedean

Kevin Buzzard (May 24 2020 at 19:38):

because this is the right way to do it

Sebastien Gouezel (May 24 2020 at 19:38):

Yes, I was guessing the real case is too boring for you.

Kevin Buzzard (May 24 2020 at 19:39):

it is pathological

Sebastien Gouezel (May 24 2020 at 19:39):

Definitely. But still interesting.

Kevin Buzzard (May 24 2020 at 19:39):

You have some phenomenon about the limit of $a_n$ is zero but $\sum a_n$ doesn't converge, right?

Kevin Buzzard (May 24 2020 at 19:40):

Doing analysis over such fields must be a nightmare

Sebastien Gouezel (May 24 2020 at 19:40):

That's what we tell undergraduates, yes. But then we forget happily about it.

Sebastien Gouezel (May 24 2020 at 19:40):

That's why it's called real analysis, as opposed to trivial analysis.

Kevin Buzzard (May 24 2020 at 19:42):

I'm just looking at my paper on this and apparently I need my base ring to be Noetherian too

Kevin Buzzard (May 24 2020 at 19:43):

It's hard to tell for sure because I can't click on the lemma name and see all hypotheses which are in place at this point, and I wrote the paper 15 years ago so have forgotten the details

orlando (May 24 2020 at 19:46):

I think it's not difficult to show the independance of the basis, we have the lemma :

lemma trace_mul_comm {S : Type v} [comm_ring S] (A : matrix m n S) (B : matrix n m S) :
  trace n S S (B ⬝ A) = trace m S S (A ⬝ B)

So if i understand @Reid Barton idea. We make a function trace (f : V \to V) (B : basis of V) and we show that this function is constant and use trunc.lift to make trace (f : V \to V)

Mario Carneiro (May 24 2020 at 21:15):

Reid Barton said:

I think for the dimension of a vector space mathlib uses a more ad-hoc trick, like the minimum cardinality of a basis

That wasn't supposed to be an ad hoc trick, it was intended to apply to modules as well

Mario Carneiro (May 24 2020 at 21:23):

although the git history says it has only ever been on vector spaces

Mario Carneiro (May 24 2020 at 21:24):

but I distinctly remember researching notions of dimension on modules (and not finding anything very definitive)

Oliver Nash (May 24 2020 at 21:38):

I actually have defining traces of finite-dimensional vector space endomorphisms on a list of things to PR at some point. I actually started this with https://github.com/leanprover-community/mathlib/pull/1973 a few months ago and then got distracted, but I have been intending to come back to it. That PR at least introduces the map $V^* \otimes W \to Hom(V, W)$ so a possible next step is to prove that it is a bijection when W is a finite-dimensional vector space, prove formulae about dimensions of tensor products and homs and use linear_map.injective_iff_surjective (or else skip the dimension stuff and just prove the map is injective over a field).

orlando (May 25 2020 at 05:18):

For the map $V^* \otimes W \to \text{Hom}(V,W)$ i suppose the definition is : (the map associated) to $(\phi, w) \mapsto \left[ v \mapsto \phi (v) \bullet w \right]$ .

I don't see other map so :grinning_face_with_smiling_eyes:

David Wärn (May 25 2020 at 07:34):

For what it's worth: Given a finite basis $w_1, \ldots, w_n$ for W with dual basis $\phi_1, \ldots, \phi_n$ , the other map is just $f \mapsto \sum_{i=1}^n f^*\phi_i \otimes w_i$ . But in the absence of a basis, there is no better name than "the inverse of the natural map".

I think this is why @Kevin Buzzard called this a trick. I guess this trick is also at the heart of classical logic: there is a natural map bool -> Prop. Some people assert that this is a bijection, and merrily use the inverse map in their calculations. Then they prove things like $(\neg \forall x, \neg P x) \to \exists x, P x$ , and you ask them why it's true. But because their inverse map is noncomputable, they have no way to unravel their calculations! (The vector space situation seems different though, since the inverse map is actually computable if you interpret "W is finite-dimensional" constructively.)

Kevin Buzzard (May 25 2020 at 08:53):

Right. We have a map one way with a "formula", and it's not bijective in general, but if V is finite-dimensional then it's an injective map between two vector spaces of the same dimension hence it must be bijective and so an inverse exists, and the inverse must exist, although might not have a "formula". We can get a formula but only if we pick a basis. My claim about Langlands is that this phenomenon shows up in other places eg in the definition of the local and global Langlands correspondences. I still don't understand what's going on on a conceptual level here. Is it something to do with this blog post or is it a different thing?

David Wärn (May 25 2020 at 11:23):

Ah, your blog post definitely seems related. Maybe the source of confusion is that you have a constructive idea of what a function is (it's something you can write down with a formula) but a non-constructive idea of what a "proof of a proposition" is (it just says that something is true, but not why it's true)? This is how Lean without classical.choice works.

bumby bumby (Apr 09 2021 at 14:38):

what libraries of mathlib can i use to prove that some set is a vector space? for example real numbers

Kevin Buzzard (Apr 09 2021 at 14:45):

That's not how things work formally. You need more than a set (in fact Lean works with type theory, not set theory, and you need more than a type). Given a random "thing" (e.g. a set or a type) you literally can't prove that it's a vector space, because being a vector space is not a theorem, it's a definition. What is your mathematical background?

bumby bumby (Apr 09 2021 at 15:01):

but here says Lean allow work with abstract structures like rings, fields or vector spaces imagen.png

Eric Wieser (Apr 09 2021 at 15:03):

There's already a discussion about this in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/vector.20spaces/near/233829510, right?

Last updated: Dec 20 2023 at 11:08 UTC