Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(linear_algebra): move is_basis_std_basis to std_basis.lean #6054

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(linear_algebra): move is_basis_std_basis to std_basis.lean #6054

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
56229e9
chore(linear_algebra): move `is_basis_std_basis` to `std_basis.lean`
Vierkantor Feb 5, 2021
365d954
Apply suggestions from code review
Vierkantor Feb 5, 2021
81f25cd
Spelling and style in docs
Vierkantor Feb 5, 2021
3fc1848
Even more spelling and style :P
Vierkantor Feb 5, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
96 changes: 0 additions & 96 deletions src/linear_algebra/basis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down Expand Up @@ -508,98 +507,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
1 change: 1 addition & 0 deletions src/linear_algebra/dimension.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
113 changes: 112 additions & 1 deletion src/linear_algebra/std_basis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -13,11 +14,23 @@ 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

- `std_basis R ϕ i b`: the `i`'th standard `R`-basis vector on `Π i, ϕ i`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps add "scaled by b"?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not exactly scaled since φ is just a semimodule. I'll use that for now unless someone has a nice alternative.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I see your point - the semimodule may not have a 1.

Vierkantor marked this conversation as resolved.
Show resolved Hide resolved

## Main results

- `is_basis_std_basis`: `std_basis` turns a componentwise basis into a basis on the product type
Vierkantor marked this conversation as resolved.
Show resolved Hide resolved
- `is_basis_fun`: `std_basis R (λ _, R) i 1` is a basis for `n → R`
Vierkantor marked this conversation as resolved.
Show resolved Hide resolved

-/

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 ι]
Expand Down Expand Up @@ -123,3 +136,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
1 change: 1 addition & 0 deletions src/ring_theory/power_series/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down