Zulip Chat Archive

Stream: new members

Topic: Splitting `[fintype n] (v: n → R)` into a sum of basis elems


view this post on Zulip Eric Wieser (Nov 20 2020 at 10:12):

I'm trying to prove

lemma is_sym_to_matrix {R : Type*} [comm_ring R] {n : Type*} [fintype n] [decidable_eq n]
  (B : bilin_form R (n  R)) : is_sym B  B.to_matrix = B.to_matrix.transpose :=
begin
  dunfold is_sym,
  split,
  { intro h,
    ext,
    rw bilin_form.to_matrix_apply,
    exact h _ _, },
  { intros h x y,
    dunfold bilin_form.to_matrix bilin_form.to_matrixₗ at h,
    simp at h,
    rw matrix.ext_iff at h,
    simp at h,
    sorry}
end
h:  (i j : n),
  B (λ (n_1 : n), ite (n_1 = i) 1 0) (λ (n_1 : n), ite (n_1 = j) 1 0) =
  B (λ (n_1 : n), ite (n_1 = j) 1 0) (λ (n_1 : n), ite (n_1 = i) 1 0)
 B x y = B y x

I'm aware that I may have unfolded too much here - but it looks like I should be able to proceed by expressing x and y as a sum of scaled basis elements, applying linearity of B in both arguments, and then applying h to each of my n^2 terms>

What I don't know how to do is the re-expressing of x and y

view this post on Zulip Anne Baanen (Nov 20 2020 at 10:13):

Something like rw ← is_basis.total_repr IIRC?

view this post on Zulip Eric Wieser (Nov 20 2020 at 10:18):

That looks like the lemma, and I guess now I need to find the lemma saying that is_basis R $ λ (i n_1 : n), ite (n_1 = i) (1 : R) 0- since surely that exists

view this post on Zulip Kenny Lau (Nov 20 2020 at 14:12):

#mwe

view this post on Zulip Kenny Lau (Nov 20 2020 at 14:12):

(missing imports)

view this post on Zulip Kenny Lau (Nov 21 2020 at 07:27):

import linear_algebra.bilinear_form

universes u v

namespace bilin_form

@[simps] def flip {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M]
  (b : bilin_form R M) : bilin_form R M :=
{ bilin := λ x y, b y x,
  bilin_add_left := λ x y z, add_right z x y,
  bilin_smul_left := λ a x y, smul_right a y x,
  bilin_add_right := λ x y z, add_left y z x,
  bilin_smul_right := λ a x y, smul_left a y x }

lemma to_matrix_flip {R : Type u} [comm_ring R] {n : Type v} [fintype n] [decidable_eq n]
  (b : bilin_form R (n  R)) : b.flip.to_matrix = b.to_matrix.transpose :=
rfl

end bilin_form

open bilin_form sym_bilin_form

lemma is_sym_to_matrix {R : Type*} [comm_ring R] {n : Type*} [fintype n] [decidable_eq n]
  (B : bilin_form R (n  R)) : is_sym B  B.to_matrix = B.to_matrix.transpose :=
begin
  dunfold is_sym,
  split,
  { intro h,
    ext,
    rw bilin_form.to_matrix_apply,
    exact h _ _, },
  { intros h x y,
    replace h := congr_arg matrix.to_bilin_form h,
    rw [ to_matrix_flip, to_matrix_to_bilin_form, to_matrix_to_bilin_form] at h,
    rw [ flip_bilin,  h] }
end

view this post on Zulip Johan Commelin (Nov 21 2020 at 07:49):

I think we should also have def matrix.is_sym

view this post on Zulip Johan Commelin (Nov 21 2020 at 07:49):

And don't we already have a linear_map.flip?

view this post on Zulip Kenny Lau (Nov 21 2020 at 08:24):

bilin_form isn't defined to be a linear_map

view this post on Zulip Johan Commelin (Nov 21 2020 at 08:39):

Ooh, me needs to learn what docs#bilin_form is

view this post on Zulip Eric Wieser (Nov 21 2020 at 09:33):

The rfl in to_matrix_flip surprises me slightly, as rfls often do. Thanks @Kenny Lau!


Last updated: May 13 2021 at 21:12 UTC