# Zulip Chat Archive

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

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

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