## Stream: maths

### Topic: Using a basis of size one

#### Patrick Lutz (Aug 08 2020 at 17:47):

Embarrassingly, I cannot figure out how to do the following using Lean's linear algebra library

import linear_algebra.basis

example (K V : Type*) [field K] [add_comm_group V] [vector_space K V]
(x : V) (hx : is_basis K (coe : ({x} : set V) → V)) (y : V) :
y = (is_basis.repr hx y ⟨x, set.mem_singleton x⟩) • x := sorry


I believe this is basically saying that if $\{x\}$ is a basis for $V$ and $y$ is in $V$ then $y$ is equal to $x$ times the coefficient of $x$ in the representation of $y$ in terms of the basis $\{x\}$. How is this sort of thing supposed to be proved?

#### Floris van Doorn (Aug 09 2020 at 04:26):

Assuming I can slightly change the problem (into - what I think is - a more convenient way of stating the example), then here is a way to do this:

import linear_algebra.basis

example (K V : Type*) [field K] [add_comm_group V] [vector_space K V]
(x : V) (hx : is_basis K (λ _ : unit, x)) (y : V) :
hx.repr y () • x = y :=
begin
convert hx.total_repr y, rw [finsupp.total_apply, finsupp.sum_fintype],
{ simp only [fintype.univ_punit, finset.sum_singleton] },
{ simp only [forall_const, zero_smul] }
end


I'm not fluent in the linear algebra library, so there might be an easier way.

#### Floris van Doorn (Aug 09 2020 at 04:29):

I found both arguments to simp only by using squeeze_simp.
For the first line I had to search a little bit, but I could use the first lemma under the relevant definition (incidentally the first lemma made progress in each of the cases).

#### Kenny Lau (Aug 09 2020 at 06:17):

import linear_algebra.basis

open finsupp

theorem repr_smul_of_unique {R M ι : Type*} [ring R] [add_comm_group M] [module R M]
[unique ι] (f : ι → M) (hx : is_basis R f) (y : M) :
hx.repr y (default ι) • f (default ι) = y :=
by conv_rhs { rw [← hx.total_repr y, total_apply, unique_single (hx.repr y), sum_single_index],
skip, rw zero_smul }

theorem repr_smul_of_singleton {R M : Type*} [ring R] [add_comm_group M] [module R M]
(x : M) (hx : is_basis R (coe : ({x} : set M) → M)) (y : M) :
hx.repr y ⟨x, set.mem_singleton x⟩ • x = y :=
repr_smul_of_unique _ hx y


Last updated: May 12 2021 at 07:17 UTC