Trace of linear maps on EuclideanSpace

Stream: Is there code for X?

[Iván Renison]

Hi, do we have something like this?

import Mathlib.Analysis.InnerProductSpace.PiL2

variable {ι 𝕜 : Type*} [RCLike 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [Fintype ι]

lemma aux : ∃s : Finset (EuclideanSpace 𝕜 ι), Nonempty (Basis { x // x ∈ s } 𝕜 (EuclideanSpace 𝕜 ι)) :=
  sorry

I so there are some things about bases of the EuclideanSpace, but not proving that in particular.

The reason for witch I want this is to work with the trace of a linear mal of type EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι, because the definition of LinearMap.trace makes cases with that existential
In particular I'm working with ι = Fin 2 and I want to prove the traces of concrete linear maps, so if you have any suggestions for that they are welcome

[Aaron Liu]

import Mathlib.Analysis.InnerProductSpace.PiL2

noncomputable example {ι 𝕜 : Type*} [RCLike 𝕜] [Fintype ι] : Basis ι 𝕜 (EuclideanSpace 𝕜 ι) :=
  PiLp.basisFun 2 𝕜 ι

[Iván Renison]

And how would you prove the ∃ using that? I have not being able

[Eric Wieser]

Why do you need the exists?

[Eric Wieser]

(the answer is going to be something like Finset.univ.image theBasisAaronPosted as the witness)

[Iván Renison]

Here is a simplified version of what I'm, trying to prove:

import Mathlib

section outerProduct

variable (𝕜 : Type*) {E : Type*} [RCLike 𝕜]
variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]

/-- The outer product of two vectors -/
def outerProduct (x : E) (y : E) : E →ₗ[𝕜] E where
  toFun := fun z => (inner 𝕜 y z) • x
  map_add' z w := by
    rw [← Module.add_smul, inner_add_right y z w]
  map_smul' m z := by
    rw [RingHom.id_apply, inner_smul_right_eq_smul y z m]
    exact IsScalarTower.smul_assoc m (inner 𝕜 y z) x

end outerProduct

variable {𝕜 : Type*} [RCLike 𝕜]
local notation "𝕜²" => EuclideanSpace 𝕜 (Fin 2)

def ket0 : 𝕜² := !₂[1, 0]
def ketbra0 : 𝕜² →ₗ[𝕜] 𝕜² := outerProduct 𝕜 ket0 ket0

example : LinearMap.trace 𝕜 𝕜² ketbra0 = 1 :=
  sorry

So I what to somehow unfold thing, and the ∃ is in an if in LinearMap.trace

[Iván Renison]

I can use Finset.univ.image (PiLp.basisFun 2 𝕜 ι), but then I'm not able to prove that that set satisfies the ∃

[Eric Wieser]

You shouldn't care that the exists is in there

[Eric Wieser]

There should be a theorem that you can use instead

[Eric Wieser]

@loogle LinearMap.trace, Basis

[loogle]

:search: LinearMap.trace.eq_1, LinearMap.trace_eq_matrix_trace, and 3 more

[Eric Wieser]

It's the second one

[Iván Renison]

Ok, thanks