<commit_before>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>
-/
import linear_algebra.matrix.reindex
import linear_algebra.matrix.to_lin

/-!
# Bases and matrices

This file defines the map `basis.to_matrix` that sends a family of vectors to
the matrix of their coordinates with respect to some basis.

## Main definitions

 * `basis.to_matrix e v` is the matrix whose `i, j`th entry is `e.repr (v j) i`
 * `basis.to_matrix_equiv` is `basis.to_matrix` bundled as a linear equiv

## Main results

 * `linear_map.to_matrix_id_eq_basis_to_matrix`: `linear_map.to_matrix b c id`
   is equal to `basis.to_matrix b c`
 * `basis.to_matrix_mul_to_matrix`: multiplying `basis.to_matrix` with another
   `basis.to_matrix` gives a `basis.to_matrix`

## Tags

matrix, basis
-/

noncomputable theory

open linear_map matrix set submodule
open_locale big_operators
open_locale matrix

section basis_to_matrix

variables {ι ι' κ κ' : Type*}
variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

open function matrix

/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
are the vectors `v i` written in the basis `e`. -/
def basis.to_matrix (e : basis ι R M) (v : ι' → M) : matrix ι ι' R :=
λ i j, e.repr (v j) i

variables (e : basis ι R M) (v : ι' → M) (i : ι) (j : ι')

namespace basis

lemma to_matrix_apply : e.to_matrix v i j = e.repr (v j) i :=
rfl

lemma to_matrix_transpose_apply : (e.to_matrix v)ᵀ j = e.repr (v j) :=
funext $ (λ _, rfl)

lemma to_matrix_eq_to_matrix_constr [fintype ι] [decidable_eq ι] (v : ι → M) :
  e.to_matrix v = linear_map.to_matrix e e (e.constr ℕ v) :=
by { ext, rw [basis.to_matrix_apply, linear_map.to_matrix_apply, basis.constr_basis] }

-- TODO (maybe) Adjust the definition of `basis.to_matrix` to eliminate the transpose.
lemma coe_pi_basis_fun.to_matrix_eq_transpose [fintype ι] :
  ((pi.basis_fun R ι).to_matrix : matrix ι ι R → matrix ι ι R) = matrix.transpose :=
by { ext M i j, refl, }

@[simp] lemma to_matrix_self [decidable_eq ι] : e.to_matrix e = 1 :=
begin
  rw basis.to_matrix,
  ext i j,
  simp [basis.equiv_fun, matrix.one_apply, finsupp.single, eq_comm]
end

lemma to_matrix_update [decidable_eq ι'] (x : M) :
  e.to_matrix (function.update v j x) = matrix.update_column (e.to_matrix v) j (e.repr x) :=
begin
  ext i' k,
  rw [basis.to_matrix, matrix.update_column_apply, e.to_matrix_apply],
  split_ifs,
  { rw [h, update_same j x v] },
  { rw update_noteq h },
end

@[simp] lemma sum_to_matrix_smul_self [fintype ι] : ∑ (i : ι), e.to_matrix v i j • e i = v j :=
by simp_rw [e.to_matrix_apply, e.sum_repr]

@[simp] lemma to_lin_to_matrix [fintype ι] [fintype ι'] [decidable_eq ι'] (v : basis ι' R M) :
  matrix.to_lin v e (e.to_matrix v) = id :=
v.ext (λ i, by rw [to_lin_self, id_apply, e.sum_to_matrix_smul_self])

/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,<commit_msg>feat(linear_algebra/matrix/basis): `to_matrix_units_smul` and `to_matrix_is_unit_smul` (#11191)<commit_after>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>
-/
import linear_algebra.matrix.reindex
import linear_algebra.matrix.to_lin

/-!
# Bases and matrices

This file defines the map `basis.to_matrix` that sends a family of vectors to
the matrix of their coordinates with respect to some basis.

## Main definitions

 * `basis.to_matrix e v` is the matrix whose `i, j`th entry is `e.repr (v j) i`
 * `basis.to_matrix_equiv` is `basis.to_matrix` bundled as a linear equiv

## Main results

 * `linear_map.to_matrix_id_eq_basis_to_matrix`: `linear_map.to_matrix b c id`
   is equal to `basis.to_matrix b c`
 * `basis.to_matrix_mul_to_matrix`: multiplying `basis.to_matrix` with another
   `basis.to_matrix` gives a `basis.to_matrix`

## Tags

matrix, basis
-/

noncomputable theory

open linear_map matrix set submodule
open_locale big_operators
open_locale matrix

section basis_to_matrix

variables {ι ι' κ κ' : Type*}
variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

open function matrix

/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
are the vectors `v i` written in the basis `e`. -/
def basis.to_matrix (e : basis ι R M) (v : ι' → M) : matrix ι ι' R :=
λ i j, e.repr (v j) i

variables (e : basis ι R M) (v : ι' → M) (i : ι) (j : ι')

namespace basis

lemma to_matrix_apply : e.to_matrix v i j = e.repr (v j) i :=
rfl

lemma to_matrix_transpose_apply : (e.to_matrix v)ᵀ j = e.repr (v j) :=
funext $ (λ _, rfl)

lemma to_matrix_eq_to_matrix_constr [fintype ι] [decidable_eq ι] (v : ι → M) :
  e.to_matrix v = linear_map.to_matrix e e (e.constr ℕ v) :=
by { ext, rw [basis.to_matrix_apply, linear_map.to_matrix_apply, basis.constr_basis] }

-- TODO (maybe) Adjust the definition of `basis.to_matrix` to eliminate the transpose.
lemma coe_pi_basis_fun.to_matrix_eq_transpose [fintype ι] :
  ((pi.basis_fun R ι).to_matrix : matrix ι ι R → matrix ι ι R) = matrix.transpose :=
by { ext M i j, refl, }

@[simp] lemma to_matrix_self [decidable_eq ι] : e.to_matrix e = 1 :=
begin
  rw basis.to_matrix,
  ext i j,
  simp [basis.equiv_fun, matrix.one_apply, finsupp.single, eq_comm]
end

lemma to_matrix_update [decidable_eq ι'] (x : M) :
  e.to_matrix (function.update v j x) = matrix.update_column (e.to_matrix v) j (e.repr x) :=
begin
  ext i' k,
  rw [basis.to_matrix, matrix.update_column_apply, e.to_matrix_apply],
  split_ifs,
  { rw [h, update_same j x v] },
  { rw update_noteq h },
end

/-- The basis constructed by `units_smul` has vectors given by a diagonal matrix. -/
@[simp] lemma to_matrix_units_smul [decidable_eq ι] (w : ι → units R) :
  e.to_matrix (e.units_smul w) = diagonal (coe ∘ w) :=
begin
  ext i j,
  by_cases h : i = j,
  { simp [h, to_matrix_apply, units_smul_apply, units.smul_def] },
  { simp [h, to_matrix_apply, units_smul_apply, units.smul_def, ne.symm h] }
end

/-- The basis constructed by `is_unit_smul` has vectors given by a diagonal matrix. -/
@[simp] lemma to_matrix_is_unit_smul [decidable_eq ι] {w : ι → R} (hw : ∀ i, is_unit (w i)) :
  e.to_matrix (e.is_unit_smul hw) = diagonal w :=
e.to_matrix_units_smul _

@[simp] lemma sum_to_matrix_smul_self [fintype ι] : ∑ (i : ι), e.to_matrix v i j • e i = v j :=
by simp_rw [e.to_matrix_apply, e.sum_repr]

@[simp] lemma to_lin_to_matrix [fintype ι] [fintype ι'] [decidable_eq ι'] (v : basis ι' R M) :
  matrix.to_lin v e (e.to_matrix v) = id :=
v.ext (λ i, by rw [to_lin_self, id_apply, e.sum_to_matrix_smul_self])

/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
{'fraction_non_alphanumeric': 0.12106111681078705, 'fraction_numerical': 0.002784698812838927, 'mean_word_length': 3.9737609329446064, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3852218', 'n_tokens_mistral': 2817, 'n_tokens_neox': 2692, 'n_words': 906}