Projection maps

Stream: Is there code for X?

[Antoine Labelle]

Hi,
Do we have basic results about projection maps in linear algebra (i.e. linear maps T such that T^2 = T), such as equivalences between different definitions (every element in the range being fixed, being diagonalisable with 0-1 eigenvalues)?
Specifically I need the result that the trace of a projection is the dimension of the range, which I couldn't find but would follow easily from these equivalences.

[Heather Macbeth]

@Antoine Labelle I think this mostly doesn't exist yet (but would be good to have!). The closest I can find is docs#submodule.is_compl_equiv_proj, proving that projection maps are in natural correspondence with internal direct sum decompositions of a vector space. If you can't be bothered building up a full theory, you could probably get the fact you need from this directly :)

[Antoine Labelle]

How much do we have about direct sums of linear maps? In particular do we have that the matrix corresponding to a direct sum of linear maps is block-diagonal, and do we have a good dictionnary between internal and external direct sums?

[Eric Wieser]

Are you talking about a linear map of direct sums formed by a separate linear map for each piece?

[Eric Wieser]

(If so, that's sort of docs#direct_sum.to_module, but you have to post-compose with docs#direct_sum.lof yourself)

[Eric Wieser]

and do we have a good dictionnary between internal and external direct sums?

Currently the approach we've been taking is "an internal direct sum is just an external direct sum of submodules"

[Eric Wieser]

We have almost no API for internal direct sums of modules beyond docs#direct_sum.submodule_is_internal and the things near it

[Eric Wieser]

Nevermind, it seems @Heather Macbeth added a bunch of useful API :tada:

[Antoine Labelle]

Thanks, I'll look that up. And do you know if we have translations with block-diagonal matrices, which I think would be needed to show that the trace is additive under direct sum.

[Eric Wieser]

Not sure what you mean by translation, but you probably want docs#matrix.block_diagonal' since the unprimed version will only work with a direct sum of copies of the same module

[Heather Macbeth]

@Antoine Labelle Are you sure you want to work with matrices? Linear algebra is often easier if you don't :)

[Antoine Labelle]

I'd prefer not to but trace is currently defined in terms of matrices, so I guess I don't really have the choice

[Antoine Labelle]

Unless we have a basis-free definition of trace that I'm not aware of?

[Heather Macbeth]

We have docs#linear_map.trace, but is what you're saying that the only way to prove something about the trace is to go to a basis?

[Heather Macbeth]

Working back from your question yesterday about projection maps, I think perhaps what you need here is that trace of docs#linear_map.prod_map of two endomorphisms is the sum of their traces?

[Heather Macbeth]

And while you're at it, the same result for docs#dfinsupp.map_range.linear_map

[Antoine Labelle]

Heather Macbeth said:

We have docs#linear_map.trace, but is what you're saying that the only way to prove something about the trace is to go to a basis?

It looks to me like we don't really have the choice, since the definition of docs#linear_map.trace is by picking a basis and taking the trace of the corresponding matrix. And we seem to have very few lemmas about the trace of a linear map, so I feel like the matrix definition is pretty much unavoidable. That being said it would be very cool to have a true basis-free definition of trace using the isomorphism Hom(V,W)=V*⊗ W and evaluation map.

[Antoine Labelle]

Heather Macbeth said:

Working back from your question yesterday about projection maps, I think perhaps what you need here is that trace of docs#linear_map.prod_map of two endomorphisms is the sum of their traces?

Right, that's exactly what I'd need for the trace of projection maps (or actually I guess an internal version of that)

[Oliver Nash]

I think the thing to do here is to fill this sorry so that nobody else has to drop down to matrices again unless they want to:

import linear_algebra.contraction
import linear_algebra.trace

open_locale tensor_product

variables (R M : Type*) [field R] [add_comm_group M] [module R M]

lemma trace_eq_contract [finite_dimensional R M] :
  (linear_map.trace R M) ∘ₗ (dual_tensor_hom R M M) = contract_left R M :=
begin
  sorry,
end

[Oliver Nash]

(And also prove that dual_tensor_hom R M M is an equiv subject to the relevant hypothesis and thus get a formula for trace in terms of its inverse and contraction.)

[Antoine Labelle]

I'll try to tackle that!

[Antoine Labelle]

Is there a lemma for linear maps agreeing iff they agree on a basis?

[Heather Macbeth]

Yup, docs#basis.ext

[Antoine Labelle]

Oliver Nash said:

I think the thing to do here is to fill this sorry so that nobody else has to drop down to matrices again unless they want to:

import linear_algebra.contraction
import linear_algebra.trace

open_locale tensor_product

variables (R M : Type*) [field R] [add_comm_group M] [module R M]

lemma trace_eq_contract [finite_dimensional R M] :
  (linear_map.trace R M) ∘ₗ (dual_tensor_hom R M M) = contract_left R M :=
begin
  sorry,
end

PR'd! #10372

[Oliver Nash]

Antoine Labelle said:

PR'd! #10372

This looks great. I just left some review remarks but overall this is really great.

[Eric Wieser]

Seems to fill a nice number of lemma holes elsewhere too