## Stream: new members

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

#### 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

#### Anne Baanen (Nov 20 2020 at 10:13):

Something like rw ← is_basis.total_repr IIRC?

#### 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

#mwe

#### Kenny Lau (Nov 20 2020 at 14:12):

(missing imports)

#### 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


#### Johan Commelin (Nov 21 2020 at 07:49):

I think we should also have def matrix.is_sym

#### Johan Commelin (Nov 21 2020 at 07:49):

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

#### Kenny Lau (Nov 21 2020 at 08:24):

bilin_form isn't defined to be a linear_map

#### Johan Commelin (Nov 21 2020 at 08:39):

Ooh, me needs to learn what docs#bilin_form is

#### 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