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

Stream: new members

[Eric Wieser]

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

[Anne Baanen]

Something like rw ← is_basis.total_repr IIRC?

[Eric Wieser]

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

[Kenny Lau]

#mwe

[Kenny Lau]

(missing imports)

[Kenny Lau]

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

[Johan Commelin]

I think we should also have def matrix.is_sym

[Johan Commelin]

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

[Kenny Lau]

bilin_form isn't defined to be a linear_map

[Johan Commelin]

Ooh, me needs to learn what docs#bilin_form is

[Eric Wieser]

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