<commit_before>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.matrix.basis
import linear_algebra.basis
import linear_algebra.pi

/-!
# The standard basis

This file defines the standard basis `pi.basis (s : ∀ j, basis (ι j) R (M j))`,
which is the `Σ j, ι j`-indexed basis of Π j, M j`. The basis vectors are given by
`pi.basis s ⟨j, i⟩ j' = linear_map.std_basis R M j' (s j) i = if j = j' then s i else 0`.

The standard basis on `R^η`, i.e. `η → R` is called `pi.basis_fun`.

To give a concrete example, `linear_map.std_basis R (λ (i : fin 3), R) i 1`
gives the `i`th unit basis vector in `R³`, and `pi.basis_fun R (fin 3)` proves
this is a basis over `fin 3 → R`.

## Main definitions

 - `linear_map.std_basis R M`: if `x` is a basis vector of `M i`, then
   `linear_map.std_basis R M i x` is the `i`th standard basis vector of `Π i, M i`.
 - `pi.basis s`: given a basis `s i` for each `M i`, the standard basis on `Π i, M i`
 - `pi.basis_fun R η`: the standard basis on `R^η`, i.e. `η → R`, given by
   `pi.basis_fun R η i j = if i = j then 1 else 0`.
 - `matrix.std_basis R n m`: the standard basis on `matrix n m R`, given by
   `matrix.std_basis R n m (i, j) i' j' = if (i, j) = (i', j') then 1 else 0`.

-/

open function submodule
open_locale big_operators
open_locale big_operators

namespace linear_map

variables (R : Type*) {ι : Type*} [semiring R] (φ : ι → Type*)
  [Π i, add_comm_monoid (φ i)] [Π i, module R (φ i)] [decidable_eq ι]

/-- The standard basis of the product of `φ`. -/
def std_basis : Π (i : ι), φ i →ₗ[R] (Πi, φ i) := single

lemma std_basis_apply (i : ι) (b : φ i) : std_basis R φ i b = update 0 i b :=
rfl

lemma coe_std_basis (i : ι) : ⇑(std_basis R φ i) = pi.single i :=
rfl

@[simp] lemma std_basis_same (i : ι) (b : φ i) : std_basis R φ i b i = b :=
by rw [std_basis_apply, update_same]

lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis R φ i b j = 0 :=
by rw [std_basis_apply, update_noteq h]; refl

lemma std_basis_eq_pi_diag (i : ι) : std_basis R φ i = pi (diag i) :=
begin
  ext x j,
  convert (update_apply 0 x i j _).symm,
  refl,
end

lemma ker_std_basis (i : ι) : ker (std_basis R φ i) = ⊥ :=
ker_eq_bot_of_injective $ assume f g hfg,
  have std_basis R φ i f i = std_basis R φ i g i := hfg ▸ rfl,
  by simpa only [std_basis_same]

lemma proj_comp_std_basis (i j : ι) : (proj i).comp (std_basis R φ j) = diag j i :=
by rw [std_basis_eq_pi_diag, proj_pi]

lemma proj_std_basis_same (i : ι) : (proj i).comp (std_basis R φ i) = id :=
by ext b; simp

lemma proj_std_basis_ne (i j : ι) (h : i ≠ j) : (proj i).comp (std_basis R φ j) = 0 :=
by ext b; simp [std_basis_ne R φ _ _ h]

lemma supr_range_std_basis_le_infi_ker_proj (I J : set ι) (h : disjoint I J) :
  (⨆i∈I, range (std_basis R φ i)) ≤ (⨅i∈J, ker (proj i)) :=
begin
  refine (supr_le $ λ i, supr_le $ λ hi, range_le_iff_comap.2 _),
  simp only [(ker_comp _ _).symm, eq_top_iff, set_like.le_def, mem_ker, comap_infi, mem_infi],
  rintro b - j hj,
  rw [proj_std_basis_ne R φ j i, zero_apply],
  rintro rfl,
  exact h ⟨hi, hj⟩
end

lemma infi_ker_proj_le_supr_range_std_basis {I : finset ι} {J : set ι} (hu : set.univ ⊆ ↑I ∪ J) :
  (⨅ i∈J, ker (proj i)) ≤ (⨆i∈I, range (std_basis R φ i)) :=
set_like.le_def.2
begin
  assume b hb,
  simp only [mem_infi, mem_ker, proj_apply] at hb,
  rw ← show ∑ i in I, std_basis R φ i (b i) = b,
  { ext i,
    rw [finset.sum_apply, ← std_basis_same R φ i (b i)],
    refine finset.sum_eq_single i (assume j hjI ne, std_basis_ne _ _ _ _ ne.symm _) _,
    assume hiI,
    rw [std_basis_same],
    exact hb _ ((hu trivial).resolve_left hiI) },
  exact sum_mem (assume i hiI, mem_supr_of_mem i $ mem_supr_of_mem hiI $
    (std_basis R φ i).mem_range_self (b i))
end

lemma supr_range_std_basis_eq_infi_ker_proj {I J : set ι}
  (hd : disjoint I J) (hu : set.univ ⊆ I ∪ J) (hI : set.finite I) :
  (⨆i∈I, range (std_basis R φ i)) = (⨅i∈J, ker (proj i)) :=
begin
  refine le_antisymm (supr_range_std_basis_le_infi_ker_proj _ _ _ _ hd) _,
  have : set.univ ⊆ ↑hI.to_finset ∪ J, { rwa [hI.coe_to_finset] },<commit_msg>chore(linear_algebra/std_basis): minor golfs (#14552)<commit_after>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.matrix.basis
import linear_algebra.basis
import linear_algebra.pi

/-!
# The standard basis

This file defines the standard basis `pi.basis (s : ∀ j, basis (ι j) R (M j))`,
which is the `Σ j, ι j`-indexed basis of Π j, M j`. The basis vectors are given by
`pi.basis s ⟨j, i⟩ j' = linear_map.std_basis R M j' (s j) i = if j = j' then s i else 0`.

The standard basis on `R^η`, i.e. `η → R` is called `pi.basis_fun`.

To give a concrete example, `linear_map.std_basis R (λ (i : fin 3), R) i 1`
gives the `i`th unit basis vector in `R³`, and `pi.basis_fun R (fin 3)` proves
this is a basis over `fin 3 → R`.

## Main definitions

 - `linear_map.std_basis R M`: if `x` is a basis vector of `M i`, then
   `linear_map.std_basis R M i x` is the `i`th standard basis vector of `Π i, M i`.
 - `pi.basis s`: given a basis `s i` for each `M i`, the standard basis on `Π i, M i`
 - `pi.basis_fun R η`: the standard basis on `R^η`, i.e. `η → R`, given by
   `pi.basis_fun R η i j = if i = j then 1 else 0`.
 - `matrix.std_basis R n m`: the standard basis on `matrix n m R`, given by
   `matrix.std_basis R n m (i, j) i' j' = if (i, j) = (i', j') then 1 else 0`.

-/

open function submodule
open_locale big_operators
open_locale big_operators

namespace linear_map

variables (R : Type*) {ι : Type*} [semiring R] (φ : ι → Type*)
  [Π i, add_comm_monoid (φ i)] [Π i, module R (φ i)] [decidable_eq ι]

/-- The standard basis of the product of `φ`. -/
def std_basis : Π (i : ι), φ i →ₗ[R] (Πi, φ i) := single

lemma std_basis_apply (i : ι) (b : φ i) : std_basis R φ i b = update 0 i b :=
rfl

lemma coe_std_basis (i : ι) : ⇑(std_basis R φ i) = pi.single i :=
rfl

@[simp] lemma std_basis_same (i : ι) (b : φ i) : std_basis R φ i b i = b :=
pi.single_eq_same i b

lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis R φ i b j = 0 :=
pi.single_eq_of_ne h b

lemma std_basis_eq_pi_diag (i : ι) : std_basis R φ i = pi (diag i) :=
begin
  ext x j,
  convert (update_apply 0 x i j _).symm,
  refl,
end

lemma ker_std_basis (i : ι) : ker (std_basis R φ i) = ⊥ :=
ker_eq_bot_of_injective $ pi.single_injective _ _

lemma proj_comp_std_basis (i j : ι) : (proj i).comp (std_basis R φ j) = diag j i :=
by rw [std_basis_eq_pi_diag, proj_pi]

lemma proj_std_basis_same (i : ι) : (proj i).comp (std_basis R φ i) = id :=
linear_map.ext $ std_basis_same R φ i

lemma proj_std_basis_ne (i j : ι) (h : i ≠ j) : (proj i).comp (std_basis R φ j) = 0 :=
linear_map.ext $ std_basis_ne R φ _ _ h

lemma supr_range_std_basis_le_infi_ker_proj (I J : set ι) (h : disjoint I J) :
  (⨆i∈I, range (std_basis R φ i)) ≤ (⨅i∈J, ker (proj i)) :=
begin
  refine (supr_le $ λ i, supr_le $ λ hi, range_le_iff_comap.2 _),
  simp only [(ker_comp _ _).symm, eq_top_iff, set_like.le_def, mem_ker, comap_infi, mem_infi],
  rintro b - j hj,
  rw [proj_std_basis_ne R φ j i, zero_apply],
  rintro rfl,
  exact h ⟨hi, hj⟩
end

lemma infi_ker_proj_le_supr_range_std_basis {I : finset ι} {J : set ι} (hu : set.univ ⊆ ↑I ∪ J) :
  (⨅ i∈J, ker (proj i)) ≤ (⨆i∈I, range (std_basis R φ i)) :=
set_like.le_def.2
begin
  assume b hb,
  simp only [mem_infi, mem_ker, proj_apply] at hb,
  rw ← show ∑ i in I, std_basis R φ i (b i) = b,
  { ext i,
    rw [finset.sum_apply, ← std_basis_same R φ i (b i)],
    refine finset.sum_eq_single i (assume j hjI ne, std_basis_ne _ _ _ _ ne.symm _) _,
    assume hiI,
    rw [std_basis_same],
    exact hb _ ((hu trivial).resolve_left hiI) },
  exact sum_mem_bsupr (λ i hi, (std_basis R φ i).mem_range_self (b i))
end

lemma supr_range_std_basis_eq_infi_ker_proj {I J : set ι}
  (hd : disjoint I J) (hu : set.univ ⊆ I ∪ J) (hI : set.finite I) :
  (⨆i∈I, range (std_basis R φ i)) = (⨅i∈J, ker (proj i)) :=
begin
  refine le_antisymm (supr_range_std_basis_le_infi_ker_proj _ _ _ _ hd) _,
  have : set.univ ⊆ ↑hI.to_finset ∪ J, { rwa [hI.coe_to_finset] },
{'fraction_non_alphanumeric': 0.13418647166361974, 'fraction_numerical': 0.005728214503351615, 'mean_word_length': 3.303093864708967, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2211362', 'n_tokens_mistral': 3863, 'n_tokens_neox': 3594, 'n_words': 1326}