Zulip Chat Archive

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}\{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?

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: Dec 20 2023 at 11:08 UTC