Zulip Chat Archive

Stream: maths

Topic: Using a basis of size one


view this post on Zulip 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}\{x\} is a basis for VV and yy is in VV then yy is equal to xx times the coefficient of xx in the representation of yy in terms of the basis {x}\{x\}. How is this sort of thing supposed to be proved?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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