chore(linear_algebra): move is_basis_std_basis to std_basis.lean (#…

…6054)

This is a follow-up to #6020 which moved `std_basis` to a new file: now move results from `basis.lean` to that same file.

CC @eric-wieser 



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/linear_algebra/basis.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
 import linear_algebra.linear_independent
 import linear_algebra.projection
-import linear_algebra.std_basis
 import data.fintype.card
 
 /-!
@@ -511,98 +510,3 @@ theorem vector_space.card_fintype [fintype K] [fintype V] :
 exists.elim (exists_is_basis K V) $ λ b hb, ⟨card b, module.card_fintype hb⟩
 
 end vector_space
-
-namespace pi
-open set linear_map
-
-section module
-variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
-variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)]
-
-lemma linear_independent_std_basis [decidable_eq η]
-  (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
-  linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
-begin
-  have hs' : ∀j : η, linear_independent R (λ i : ιs j, std_basis R Ms j (v j i)),
-  { intro j,
-    exact (hs j).map' _ (ker_std_basis _ _ _) },
-  apply linear_independent_Union_finite hs',
-  { assume j J _ hiJ,
-    simp [(set.Union.equations._eqn_1 _).symm, submodule.span_image, submodule.span_Union],
-    have h₀ : ∀ j, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
-        ≤ range (std_basis R Ms j),
-    { intro j,
-      rw [span_le, linear_map.range_coe],
-      apply range_comp_subset_range },
-    have h₁ : span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
-        ≤ ⨆ i ∈ {j}, range (std_basis R Ms i),
-    { rw @supr_singleton _ _ _ (λ i, linear_map.range (std_basis R (λ (j : η), Ms j) i)),
-      apply h₀ },
-    have h₂ : (⨆ j ∈ J, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))) ≤
-               ⨆ j ∈ J, range (std_basis R (λ (j : η), Ms j) j) :=
-      supr_le_supr (λ i, supr_le_supr (λ H, h₀ i)),
-    have h₃ : disjoint (λ (i : η), i ∈ {j}) J,
-    { convert set.disjoint_singleton_left.2 hiJ using 0 },
-    exact (disjoint_std_basis_std_basis _ _ _ _ h₃).mono h₁ h₂ }
-end
-
-variable [fintype η]
-
-lemma is_basis_std_basis [decidable_eq η] (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
-  is_basis R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (s ji.1 ji.2)) :=
-begin
-  split,
-  { apply linear_independent_std_basis _ (assume i, (hs i).1) },
-  have h₁ : Union (λ j, set.range (std_basis R Ms j ∘ s j))
-    ⊆ range (λ (ji : Σ (j : η), ιs j), (std_basis R Ms (ji.fst)) (s (ji.fst) (ji.snd))),
-  { apply Union_subset, intro i,
-    apply range_comp_subset_range (λ x : ιs i, (⟨i, x⟩ : Σ (j : η), ιs j))
-        (λ (ji : Σ (j : η), ιs j), std_basis R Ms (ji.fst) (s (ji.fst) (ji.snd))) },
-  have h₂ : ∀ i, span R (range (std_basis R Ms i ∘ s i)) = range (std_basis R Ms i),
-  { intro i,
-    rw [set.range_comp, submodule.span_image, (assume i, (hs i).2), submodule.map_top] },
-  apply eq_top_mono,
-  apply span_mono h₁,
-  rw span_Union,
-  simp only [h₂],
-  apply supr_range_std_basis
-end
-
-section
-variables (R η)
-
-lemma is_basis_fun₀ [decidable_eq η] : is_basis R
-    (λ (ji : Σ (j : η), unit),
-       (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
-@is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ _ (λ _ _, (1 : R))
-  (assume i, @is_basis_singleton_one _ _ _ _)
-
-lemma is_basis_fun [decidable_eq η] : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
-begin
-  apply (is_basis_fun₀ R η).comp (λ i, ⟨i, punit.star⟩),
-  apply bijective_iff_has_inverse.2,
-  use sigma.fst,
-  simp [function.left_inverse, function.right_inverse]
-end
-
-@[simp] lemma is_basis_fun_repr [decidable_eq η] (x : η → R) (i : η) :
-  (pi.is_basis_fun R η).repr x i = x i :=
-begin
-  conv_rhs { rw ← (pi.is_basis_fun R η).total_repr x },
-  rw [finsupp.total_apply, finsupp.sum_fintype],
-  show (pi.is_basis_fun R η).repr x i =
-    (∑ j, λ i, (pi.is_basis_fun R η).repr x j • std_basis R (λ _, R) j 1 i) i,
-  rw [finset.sum_apply, finset.sum_eq_single i],
-  { simp only [pi.smul_apply, smul_eq_mul, std_basis_same, mul_one] },
-  { rintros b - hb, simp only [std_basis_ne _ _ _ _ hb.symm, smul_zero] },
-  { intro,
-    have := finset.mem_univ i,
-    contradiction },
-  { intros, apply zero_smul },
-end
-
-end
-
-end module
-
-end pi

src/linear_algebra/dimension.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro, Johannes Hölzl, Sander Dahmen
 -/
 import linear_algebra.basis
+import linear_algebra.std_basis
 import set_theory.cardinal_ordinal
 
 /-!

src/linear_algebra/std_basis.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import linear_algebra.basic
+import linear_algebra.basis
 
 /-!
 # The standard basis
@@ -13,11 +14,25 @@ elsewhere.
 
 To give a concrete example, `std_basis R (λ (i : fin 3), R) i 1` gives the `i`th unit basis vector
 in `R³`, and `pi.is_basis_fun` proves this is a basis over `fin 3 → R`.
+
+## Main definitions
+
+ - `linear_map.std_basis R ϕ i b`: the `i`'th standard `R`-basis vector on `Π i, ϕ i`,
+   scaled by `b`.
+
+## Main results
+
+ - `pi.is_basis_std_basis`: `std_basis` turns a component-wise basis into a basis on the product
+   type.
+ - `pi.is_basis_fun`: `std_basis R (λ _, R) i 1` is a basis for `n → R`.
+
 -/
 
-namespace linear_map
 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, semimodule R (φ i)] [decidable_eq ι]
@@ -123,3 +138,101 @@ begin
 end
 
 end linear_map
+
+namespace pi
+open linear_map
+open set
+
+variables {R : Type*}
+
+section module
+variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
+variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)]
+
+lemma linear_independent_std_basis [decidable_eq η]
+  (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
+  linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
+begin
+  have hs' : ∀j : η, linear_independent R (λ i : ιs j, std_basis R Ms j (v j i)),
+  { intro j,
+    exact (hs j).map' _ (ker_std_basis _ _ _) },
+  apply linear_independent_Union_finite hs',
+  { assume j J _ hiJ,
+    simp [(set.Union.equations._eqn_1 _).symm, submodule.span_image, submodule.span_Union],
+    have h₀ : ∀ j, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
+        ≤ range (std_basis R Ms j),
+    { intro j,
+      rw [span_le, linear_map.range_coe],
+      apply range_comp_subset_range },
+    have h₁ : span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
+        ≤ ⨆ i ∈ {j}, range (std_basis R Ms i),
+    { rw @supr_singleton _ _ _ (λ i, linear_map.range (std_basis R (λ (j : η), Ms j) i)),
+      apply h₀ },
+    have h₂ : (⨆ j ∈ J, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))) ≤
+               ⨆ j ∈ J, range (std_basis R (λ (j : η), Ms j) j) :=
+      supr_le_supr (λ i, supr_le_supr (λ H, h₀ i)),
+    have h₃ : disjoint (λ (i : η), i ∈ {j}) J,
+    { convert set.disjoint_singleton_left.2 hiJ using 0 },
+    exact (disjoint_std_basis_std_basis _ _ _ _ h₃).mono h₁ h₂ }
+end
+
+variable [fintype η]
+
+lemma is_basis_std_basis [decidable_eq η] (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
+  is_basis R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (s ji.1 ji.2)) :=
+begin
+  split,
+  { apply linear_independent_std_basis _ (assume i, (hs i).1) },
+  have h₁ : Union (λ j, set.range (std_basis R Ms j ∘ s j))
+    ⊆ range (λ (ji : Σ (j : η), ιs j), (std_basis R Ms (ji.fst)) (s (ji.fst) (ji.snd))),
+  { apply Union_subset, intro i,
+    apply range_comp_subset_range (λ x : ιs i, (⟨i, x⟩ : Σ (j : η), ιs j))
+        (λ (ji : Σ (j : η), ιs j), std_basis R Ms (ji.fst) (s (ji.fst) (ji.snd))) },
+  have h₂ : ∀ i, span R (range (std_basis R Ms i ∘ s i)) = range (std_basis R Ms i),
+  { intro i,
+    rw [set.range_comp, submodule.span_image, (assume i, (hs i).2), submodule.map_top] },
+  apply eq_top_mono,
+  apply span_mono h₁,
+  rw span_Union,
+  simp only [h₂],
+  apply supr_range_std_basis
+end
+
+section
+variables (R η)
+
+lemma is_basis_fun₀ [decidable_eq η] : is_basis R
+    (λ (ji : Σ (j : η), unit),
+       (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
+@is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ _ (λ _ _, (1 : R))
+  (assume i, @is_basis_singleton_one _ _ _ _)
+
+lemma is_basis_fun [decidable_eq η] : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
+begin
+  apply (is_basis_fun₀ R η).comp (λ i, ⟨i, punit.star⟩),
+  apply bijective_iff_has_inverse.2,
+  use sigma.fst,
+  simp [function.left_inverse, function.right_inverse]
+end
+
+@[simp] lemma is_basis_fun_repr [decidable_eq η] (x : η → R) (i : η) :
+  (pi.is_basis_fun R η).repr x i = x i :=
+begin
+  conv_rhs { rw ← (pi.is_basis_fun R η).total_repr x },
+  rw [finsupp.total_apply, finsupp.sum_fintype],
+  show (pi.is_basis_fun R η).repr x i =
+    (∑ j, λ i, (pi.is_basis_fun R η).repr x j • std_basis R (λ _, R) j 1 i) i,
+  rw [finset.sum_apply, finset.sum_eq_single i],
+  { simp only [pi.smul_apply, smul_eq_mul, std_basis_same, mul_one] },
+  { rintros b - hb, simp only [std_basis_ne _ _ _ _ hb.symm, smul_zero] },
+  { intro,
+    have := finset.mem_univ i,
+    contradiction },
+  { intros, apply zero_smul },
+end
+
+end
+
+end module
+
+end pi

src/ring_theory/power_series/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau
 -/
 import data.mv_polynomial
+import linear_algebra.std_basis
 import ring_theory.ideal.operations
 import ring_theory.multiplicity
 import ring_theory.algebra_tower