mathlib documentation

linear_algebra.basis

Bases #

This file defines bases in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

Main definitions #

All definitions are given for families of vectors, i.e. v : ι → M where M is the module or vector space and ι : Type* is an arbitrary indexing type.

basis ι R M is the type of ι-indexed R-bases for a module M, represented by a linear equiv M ≃ₗ[R] ι →₀ R.
the basis vectors of a basis b : basis ι R M are available as b i, where i : ι
basis.repr is the isomorphism sending x : M to its coordinates basis.repr x : ι →₀ R. The converse, turning this isomorphism into a basis, is called basis.of_repr.
If ι is finite, there is a variant of repr called basis.equiv_fun b : M ≃ₗ[R] ι → R (saving you from having to work with finsupp). The converse, turning this isomorphism into a basis, is called basis.of_equiv_fun.
basis.constr hv f constructs a linear map M₁ →ₗ[R] M₂ given the values f : ι → M₂ at the basis elements ⇑b : ι → M₁.
basis.reindex uses an equiv to map a basis to a different indexing set.
basis.map uses a linear equiv to map a basis to a different module.

Main statements #

basis.mk: a linear independent set of vectors spanning the whole module determines a basis
basis.ext states that two linear maps are equal if they coincide on a basis. Similar results are available for linear equivs (if they coincide on the basis vectors), elements (if their coordinates coincide) and the functions b.repr and ⇑b.
basis.of_vector_space states that every vector space has a basis.

Implementation notes #

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent. For bases, this is useful as well because we can easily derive ordered bases by using an ordered index type ι.

Tags #

basis, bases

structure basis (ι : Type u_1) (R : Type u_3) (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] :

Type (max u_1 u_3 u_5)

repr : M ≃ₗ[R] ι →₀ R

A basis ι R M for a module M is the type of ι-indexed R-bases of M.

The basis vectors are available as coe_fn (b : basis ι R M) : ι → M. To turn a linear independent family of vectors spanning M into a basis, use basis.mk. They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R), available as basis.repr.

Instances for basis

@[protected, instance]

noncomputable def basis.inhabited {ι : Type u_1} {R : Type u_3} [semiring R] :

inhabited (basis ι R (ι →₀ R))

Equations

basis.inhabited = {default := {repr := linear_equiv.refl R (ι →₀ R) (finsupp.module ι R)}}

@[protected, instance]

noncomputable def basis.has_coe_to_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :

has_coe_to_fun (basis ι R M) (λ (_x : basis ι R M), ι → M)

b i is the ith basis vector.

Equations

basis.has_coe_to_fun = {coe := λ (b : basis ι R M) (i : ι), ⇑(b.repr.symm) (finsupp.single i 1)}

@[simp]

theorem basis.coe_of_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (e : M ≃ₗ[R] ι →₀ R) :

⇑{repr := e} = λ (i : ι), ⇑(e.symm) (finsupp.single i 1)

@[protected]

theorem basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial R] :

function.injective ⇑b

theorem basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

⇑(b.repr.symm) (finsupp.single i 1) = ⇑b i

theorem basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (c : R) :

⇑(b.repr.symm) (finsupp.single i c) = c • ⇑b i

@[simp]

theorem basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

⇑(b.repr) (⇑b i) = finsupp.single i 1

theorem basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i j : ι) [decidable (i = j)] :

⇑(⇑(b.repr) (⇑b i)) j = ite (i = j) 1 0

@[simp]

theorem basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (v : ι →₀ R) :

⇑(b.repr.symm) v = ⇑(finsupp.total ι M R ⇑b) v

@[simp]

theorem basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

↑(b.repr.symm) = finsupp.total ι M R ⇑b

@[simp]

theorem basis.repr_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (v : ι →₀ R) :

⇑(b.repr) (⇑(finsupp.total ι M R ⇑b) v) = v

@[simp]

theorem basis.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) :

⇑(finsupp.total ι M R ⇑b) (⇑(b.repr) x) = x

theorem basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

linear_map.range ↑(b.repr) = finsupp.supported R R set.univ

theorem basis.mem_span_repr_support {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (b : basis ι R M) (m : M) :

m ∈ submodule.span R (⇑b '' ↑((⇑(b.repr) m).support))

theorem basis.repr_support_subset_of_mem_span {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (b : basis ι R M) (s : set ι) {m : M} (hm : m ∈ submodule.span R (⇑b '' s)) :

↑((⇑(b.repr) m).support) ⊆ s

@[simp]

theorem basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (ᾰ : M) :

⇑(b.coord i) ᾰ = ⇑(⇑(b.repr) ᾰ) i

noncomputable def basis.coord {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

b.coord i is the linear function giving the i'th coordinate of a vector with respect to the basis b.

b.coord i is an element of the dual space. In particular, for finite-dimensional spaces it is the ιth basis vector of the dual space.

Equations

b.coord i = (finsupp.lapply i).comp ↑(b.repr)

theorem basis.forall_coord_eq_zero_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x : M} :

(∀ (i : ι), ⇑(b.coord i) x = 0) ↔ x = 0

noncomputable def basis.sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

The sum of the coordinates of an element m : M with respect to a basis.

Equations

b.sum_coords = (⇑(finsupp.lsum ℕ) (λ (i : ι), linear_map.id)).comp ↑(b.repr)

@[simp]

theorem basis.coe_sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

⇑(b.sum_coords) = λ (m : M), (⇑(b.repr) m).sum (λ (i : ι), id)

theorem basis.coe_sum_coords_eq_finsum {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

⇑(b.sum_coords) = λ (m : M), finsum (λ (i : ι), ⇑(b.coord i) m)

@[simp]

theorem basis.coe_sum_coords_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] :

⇑(b.sum_coords) = finset.univ.sum (λ (i : ι), ⇑(b.coord i))

@[simp]

theorem basis.sum_coords_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

⇑(b.sum_coords) (⇑b i) = 1

theorem basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {M₁ : Type u_10} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ (i : ι), ⇑f₁ (⇑b i) = ⇑f₂ (⇑b i)) :

f₁ = f₂

Two linear maps are equal if they are equal on basis vectors.

theorem basis.ext' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M₁ : Type u_10} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ (i : ι), ⇑f₁ (⇑b i) = ⇑f₂ (⇑b i)) :

f₁ = f₂

Two linear equivs are equal if they are equal on basis vectors.

theorem basis.ext_elem {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {x y : M} (h : ∀ (i : ι), ⇑(⇑(b.repr) x) i = ⇑(⇑(b.repr) y) i) :

x = y

Two elements are equal if their coordinates are equal.

theorem basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {f : M →ₗ[R] ι →₀ R} :

↑(b.repr) = f ↔ ∀ (i : ι), ⇑f (⇑b i) = finsupp.single i 1

theorem basis.repr_eq_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {f : M ≃ₗ[R] ι →₀ R} :

b.repr = f ↔ ∀ (i : ι), ⇑f (⇑b i) = finsupp.single i 1

theorem basis.apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b : basis ι R M} {x : M} {i : ι} :

⇑b i = x ↔ ⇑(b.repr) x = finsupp.single i 1

theorem basis.repr_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (f : M → ι → R) (hadd : ∀ (x y : M), f (x + y) = f x + f y) (hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x) (f_eq : ∀ (i : ι), f (⇑b i) = ⇑(finsupp.single i 1)) (x : M) (i : ι) :

⇑(⇑(b.repr) x) i = f x i

An unbundled version of repr_eq_iff

theorem basis.eq_of_repr_eq_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b₁ b₂ : basis ι R M} (h : ∀ (x : M) (i : ι), ⇑(⇑(b₁.repr) x) i = ⇑(⇑(b₂.repr) x) i) :

b₁ = b₂

Two bases are equal if they assign the same coordinates.

@[ext]

theorem basis.eq_of_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {b₁ b₂ : basis ι R M} (h : ∀ (i : ι), ⇑b₁ i = ⇑b₂ i) :

b₁ = b₂

Two bases are equal if their basis vectors are the same.

@[protected]

noncomputable def basis.map {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') :

basis ι R M'

Apply the linear equivalence f to the basis vectors.

Equations

b.map f = {repr := f.symm.trans b.repr}

@[simp]

theorem basis.map_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') :

(b.map f).repr = f.symm.trans b.repr

@[simp]

theorem basis.map_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (f : M ≃ₗ[R] M') (i : ι) :

⇑(b.map f) i = ⇑f (⇑b i)

@[simp]

theorem basis.map_coeffs_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), ⇑f c • x = c • x) :

(b.map_coeffs f h).repr = (linear_equiv.restrict_scalars R' b.repr).trans (finsupp.map_range.linear_equiv (module.comp_hom.to_linear_equiv f.symm).symm)

noncomputable def basis.map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), ⇑f c • x = c • x) :

basis ι R' M

If R and R' are isomorphic rings that act identically on a module M, then a basis for M as R-module is also a basis for M as R'-module.

See also basis.algebra_map_coeffs for the case where f is equal to algebra_map.

Equations

b.map_coeffs f h = let _inst : module R' R := module.comp_hom R ↑(f.symm) in {repr := (linear_equiv.restrict_scalars R' b.repr).trans (finsupp.map_range.linear_equiv (module.comp_hom.to_linear_equiv f.symm).symm)}

theorem basis.map_coeffs_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), ⇑f c • x = c • x) (i : ι) :

⇑(b.map_coeffs f h) i = ⇑b i

@[simp]

theorem basis.coe_map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), ⇑f c • x = c • x) :

⇑(b.map_coeffs f h) = ⇑b

noncomputable def basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ≃ ι') :

basis ι' R M

b.reindex (e : ι ≃ ι') is a basis indexed by ι'

Equations

b.reindex e = {repr := b.repr.trans (finsupp.dom_lcongr e)}

theorem basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ≃ ι') (i' : ι') :

⇑(b.reindex e) i' = ⇑b (⇑(e.symm) i')

@[simp]

theorem basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ≃ ι') :

⇑(b.reindex e) = ⇑b ∘ ⇑(e.symm)

@[simp]

theorem basis.coe_reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (e : ι ≃ ι') :

⇑(⇑((b.reindex e).repr) x) = ⇑(⇑(b.repr) x) ∘ ⇑(e.symm)

@[simp]

theorem basis.reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (e : ι ≃ ι') (i' : ι') :

⇑(⇑((b.reindex e).repr) x) i' = ⇑(⇑(b.repr) x) (⇑(e.symm) i')

@[simp]

theorem basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

b.reindex (equiv.refl ι) = b

@[simp]

theorem basis.range_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ≃ ι') :

set.range (⇑b ∘ ⇑(e.symm)) = set.range ⇑b

simp normal form version of range_reindex

theorem basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (e : ι ≃ ι') :

set.range ⇑(b.reindex e) = set.range ⇑b

noncomputable def basis.reindex_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

basis ↥(set.range ⇑b) R M

b.reindex_range is a basis indexed by range b, the basis vectors themselves.

Equations

b.reindex_range = dite (nontrivial R) (λ (h : nontrivial R), let _inst : nontrivial R := h in b.reindex (equiv.of_injective ⇑b _)) (λ (h : ¬nontrivial R), let _inst : subsingleton R := _ in {repr := module.subsingleton_equiv R M ↥(set.range ⇑b) _inst_3})

theorem basis.finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] {f : α → β} (hf : function.injective f) (x z : α) (y : γ) :

⇑(finsupp.single (f x) y) (f z) = ⇑(finsupp.single x y) z

theorem basis.reindex_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) (h : ⇑b i ∈ set.range (λ (i : ι), ⇑b i) := _) :

⇑(b.reindex_range) ⟨⇑b i, h⟩ = ⇑b i

theorem basis.reindex_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (i : ι) :

⇑(b.reindex_range.repr) (⇑b i) = finsupp.single ⟨⇑b i, _⟩ 1

@[simp]

theorem basis.reindex_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : ↥(set.range ⇑b)) :

⇑(b.reindex_range) x = ↑x

theorem basis.reindex_range_repr' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) {bi : M} {i : ι} (h : ⇑b i = bi) :

⇑(⇑(b.reindex_range.repr) x) ⟨bi, _⟩ = ⇑(⇑(b.repr) x) i

@[simp]

theorem basis.reindex_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) (i : ι) (h : ⇑b i ∈ set.range (λ (i : ι), ⇑b i) := _) :

⇑(⇑(b.reindex_range.repr) x) ⟨⇑b i, h⟩ = ⇑(⇑(b.repr) x) i

noncomputable def basis.reindex_finset_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] :

basis ↥(finset.image ⇑b finset.univ) R M

b.reindex_finset_range is a basis indexed by finset.univ.image b, the finite set of basis vectors themselves.

Equations

b.reindex_finset_range = b.reindex_range.reindex ((equiv.refl M).subtype_equiv _)

theorem basis.reindex_finset_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (i : ι) (h : ⇑b i ∈ finset.image ⇑b finset.univ := _) :

⇑(b.reindex_finset_range) ⟨⇑b i, h⟩ = ⇑b i

@[simp]

theorem basis.reindex_finset_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (x : ↥(finset.image ⇑b finset.univ)) :

⇑(b.reindex_finset_range) x = ↑x

theorem basis.reindex_finset_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (i : ι) :

⇑(b.reindex_finset_range.repr) (⇑b i) = finsupp.single ⟨⇑b i, _⟩ 1

@[simp]

theorem basis.reindex_finset_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [fintype ι] (x : M) (i : ι) (h : ⇑b i ∈ finset.image ⇑b finset.univ := _) :

⇑(⇑(b.reindex_finset_range.repr) x) ⟨⇑b i, h⟩ = ⇑(⇑(b.repr) x) i

@[protected]

theorem basis.linear_independent {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

linear_independent R ⇑b

@[protected]

theorem basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial R] (i : ι) :

⇑b i ≠ 0

@[protected]

theorem basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) (x : M) :

x ∈ submodule.span R (set.range ⇑b)

@[protected]

theorem basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

submodule.span R (set.range ⇑b) = ⊤

theorem basis.index_nonempty {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) [nontrivial M] :

noncomputable def basis.constr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] :

(ι → M') ≃ₗ[S] M →ₗ[R] M'

Construct a linear map given the value at the basis.

This definition is parameterized over an extra semiring S, such that smul_comm_class R S M' holds. If R is commutative, you can set S := R; if R is not commutative, you can recover an add_equiv by setting S := ℕ. See library note [bundled maps over different rings].

Equations

b.constr S = {to_fun := λ (f : ι → M'), (finsupp.total M' M' R id).comp ((finsupp.lmap_domain R R f).comp ↑(b.repr)), map_add' := _, map_smul' := _, inv_fun := λ (f : M →ₗ[R] M') (i : ι), ⇑f (⇑b i), left_inv := _, right_inv := _}

theorem basis.constr_def {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') :

⇑(b.constr S) f = (finsupp.total M' M' R id).comp ((finsupp.lmap_domain R R f).comp ↑(b.repr))

theorem basis.constr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (x : M) :

⇑(⇑(b.constr S) f) x = (⇑(b.repr) x).sum (λ (b : ι) (a : R), a • f b)

@[simp]

theorem basis.constr_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (i : ι) :

⇑(⇑(b.constr S) f) (⇑b i) = f i

theorem basis.constr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ (i : ι), g i = ⇑f (⇑b i)) :

⇑(b.constr S) g = f

theorem basis.constr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : M →ₗ[R] M') :

⇑(b.constr S) (λ (i : ι), ⇑f (⇑b i)) = f

theorem basis.constr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] [nonempty ι] {f : ι → M'} :

linear_map.range (⇑(b.constr S) f) = submodule.span R (set.range f)

@[simp]

theorem basis.constr_comp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : M' →ₗ[R] M') (v : ι → M') :

⇑(b.constr S) (⇑f ∘ v) = f.comp (⇑(b.constr S) v)

@[protected]

noncomputable def basis.equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ≃ ι') :

If b is a basis for M and b' a basis for M', and the index types are equivalent, b.equiv b' e is a linear equivalence M ≃ₗ[R] M', mapping b i to b' (e i).

Equations

b.equiv b' e = b.repr.trans (b'.reindex e.symm).repr.symm

@[simp]

theorem basis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (i : ι) (b' : basis ι' R M') (e : ι ≃ ι') :

⇑(b.equiv b' e) (⇑b i) = ⇑b' (⇑e i)

@[simp]

theorem basis.equiv_refl {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) :

b.equiv b (equiv.refl ι) = linear_equiv.refl R M

@[simp]

theorem basis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ≃ ι') :

(b.equiv b' e).symm = b'.equiv b e.symm

@[simp]

theorem basis.equiv_trans {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {M'' : Type u_7} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') [add_comm_monoid M''] [module R M''] {ι'' : Type u_4} (b'' : basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :

(b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e')

@[simp]

theorem basis.map_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (e : ι ≃ ι') :

b.map (b.equiv b' e) = b'.reindex e.symm

@[protected]

noncomputable def basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') :

basis (ι ⊕ ι') R (M × M')

basis.prod maps a ι-indexed basis for M and a ι'-indexed basis for M' to a ι ⊕ ι'-index basis for M × M'. For the specific case of R × R, see also basis.fin_two_prod.

Equations

b.prod b' = {repr := (b.repr.prod b'.repr).trans (finsupp.sum_finsupp_lequiv_prod_finsupp R).symm}

@[simp]

theorem basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (x : M × M') (i : ι) :

⇑(⇑((b.prod b').repr) x) (sum.inl i) = ⇑(⇑(b.repr) x.fst) i

@[simp]

theorem basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (x : M × M') (i : ι') :

⇑(⇑((b.prod b').repr) x) (sum.inr i) = ⇑(⇑(b'.repr) x.snd) i

theorem basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι) :

(⇑(b.prod b') (sum.inl i)).fst = ⇑b i

theorem basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι') :

(⇑(b.prod b') (sum.inr i)).fst = 0

theorem basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι) :

(⇑(b.prod b') (sum.inl i)).snd = 0

theorem basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι') :

(⇑(b.prod b') (sum.inr i)).snd = ⇑b' i

@[simp]

theorem basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (i : ι ⊕ ι') :

⇑(b.prod b') i = sum.elim (⇑(linear_map.inl R M M') ∘ ⇑b) (⇑(linear_map.inr R M M') ∘ ⇑b') i

@[protected]

theorem basis.no_zero_smul_divisors {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) :

no_zero_smul_divisors R M

@[protected]

theorem basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) {c : R} {x : M} :

c • x = 0 ↔ c = 0 ∨ x = 0

theorem eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] (b : basis ι R M) (N : submodule R M) (rank_eq : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m = 0) :

@[protected]

noncomputable def basis.singleton (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] :

basis ι R R

basis.singleton ι R is the basis sending the unique element of ι to 1 : R.

Equations

basis.singleton ι R = {repr := {to_fun := λ (x : R), finsupp.single inhabited.default x, map_add' := _, map_smul' := _, inv_fun := λ (f : ι →₀ R), ⇑f inhabited.default, left_inv := _, right_inv := _}}

@[simp]

theorem basis.singleton_apply (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (i : ι) :

⇑(basis.singleton ι R) i = 1

@[simp]

theorem basis.singleton_repr (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (x : R) (i : ι) :

⇑(⇑((basis.singleton ι R).repr) x) i = x

theorem basis.basis_singleton_iff {R : Type u_1} {M : Type u_2} [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (ι : Type u_3) [unique ι] :

nonempty (basis ι R M) ↔ ∃ (x : M) (H : x ≠ 0), ∀ (y : M), ∃ (r : R), r • x = y

@[protected]

noncomputable def basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] [is_empty ι] :

basis ι R M

If M is a subsingleton and ι is empty, this is the unique ι-indexed basis for M.

Equations

basis.empty M = {repr := 0}

@[protected, instance]

noncomputable def basis.empty_unique {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] [is_empty ι] :

unique (basis ι R M)

Equations

basis.empty_unique M = {to_inhabited := {default := basis.empty M _inst_7}, uniq := _}

noncomputable def basis.equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) :

M ≃ₗ[R] ι → R

A module over R with a finite basis is linearly equivalent to functions from its basis to R.

Equations

b.equiv_fun = b.repr.trans {to_fun := coe_fn finsupp.has_coe_to_fun, map_add' := _, map_smul' := _, inv_fun := finsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}

noncomputable def module.fintype_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) [fintype R] :

A module over a finite ring that admits a finite basis is finite.

Equations

module.fintype_of_fintype b = fintype.of_equiv (ι → R) b.equiv_fun.to_equiv.symm

theorem module.card_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) [fintype R] [fintype M] :

fintype.card M = fintype.card R ^ fintype.card ι

@[simp]

theorem basis.equiv_fun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (x : ι → R) :

⇑(b.equiv_fun.symm) x = finset.univ.sum (λ (i : ι), x i • ⇑b i)

Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps a function x : ι → R to the linear combination ∑_i x i • v i.

@[simp]

theorem basis.equiv_fun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :

⇑(b.equiv_fun) u = ⇑(⇑(b.repr) u)

@[simp]

theorem basis.map_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] [fintype ι] (b : basis ι R M) (f : M ≃ₗ[R] M') :

(b.map f).equiv_fun = f.symm.trans b.equiv_fun

theorem basis.sum_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :

finset.univ.sum (λ (i : ι), ⇑(b.equiv_fun) u i • ⇑b i) = u

theorem basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (u : M) :

finset.univ.sum (λ (i : ι), ⇑(⇑(b.repr) u) i • ⇑b i) = u

@[simp]

theorem basis.equiv_fun_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (b : basis ι R M) (i j : ι) :

⇑(b.equiv_fun) (⇑b i) j = ite (i = j) 1 0

noncomputable def basis.of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) :

basis ι R M

Define a basis by mapping each vector x : M to its coordinates e x : ι → R, as long as ι is finite.

Equations

basis.of_equiv_fun e = {repr := e.trans (finsupp.linear_equiv_fun_on_fintype R R ι).symm}

@[simp]

theorem basis.of_equiv_fun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) :

⇑(⇑((basis.of_equiv_fun e).repr) x) i = ⇑e x i

@[simp]

theorem basis.coe_of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (e : M ≃ₗ[R] ι → R) :

⇑(basis.of_equiv_fun e) = λ (i : ι), ⇑(e.symm) (function.update 0 i 1)

@[simp]

theorem basis.of_equiv_fun_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (v : basis ι R M) :

basis.of_equiv_fun v.equiv_fun = v

@[simp]

theorem basis.constr_apply_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] [fintype ι] (b : basis ι R M) (S : Type u_9) [semiring S] [module S M'] [smul_comm_class R S M'] (f : ι → M') (x : M) :

⇑(⇑(b.constr S) f) x = finset.univ.sum (λ (i : ι), ⇑(b.equiv_fun) x i • f i)

noncomputable def basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (⇑b i) ∈ set.range ⇑b') (hg : ∀ (i : ι'), g (⇑b' i) ∈ set.range ⇑b) (hgf : ∀ (i : ι), g (f (⇑b i)) = ⇑b i) (hfg : ∀ (i : ι'), f (g (⇑b' i)) = ⇑b' i) :

If b is a basis for M and b' a basis for M', and f, g form a bijection between the basis vectors, b.equiv' b' f g hf hg hgf hfg is a linear equivalence M ≃ₗ[R] M', mapping b i to f (b i).

Equations

b.equiv' b' f g hf hg hgf hfg = {to_fun := (⇑(b.constr R) (f ∘ ⇑b)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(⇑(b'.constr R) (g ∘ ⇑b')), left_inv := _, right_inv := _}

@[simp]

theorem basis.equiv'_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (⇑b i) ∈ set.range ⇑b') (hg : ∀ (i : ι'), g (⇑b' i) ∈ set.range ⇑b) (hgf : ∀ (i : ι), g (f (⇑b i)) = ⇑b i) (hfg : ∀ (i : ι'), f (g (⇑b' i)) = ⇑b' i) (i : ι) :

⇑(b.equiv' b' f g hf hg hgf hfg) (⇑b i) = f (⇑b i)

@[simp]

theorem basis.equiv'_symm_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M'] [module R M'] (b : basis ι R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (⇑b i) ∈ set.range ⇑b') (hg : ∀ (i : ι'), g (⇑b' i) ∈ set.range ⇑b) (hgf : ∀ (i : ι), g (f (⇑b i)) = ⇑b i) (hfg : ∀ (i : ι'), f (g (⇑b' i)) = ⇑b' i) (i : ι') :

⇑((b.equiv' b' f g hf hg hgf hfg).symm) (⇑b' i) = g (⇑b' i)

theorem basis.sum_repr_mul_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] (b : basis ι R M) {ι' : Type u_2} [fintype ι'] (b' : basis ι' R M) (x : M) (i : ι) :

finset.univ.sum (λ (j : ι'), ⇑(⇑(b.repr) (⇑b' j)) i * ⇑(⇑(b'.repr) x) j) = ⇑(⇑(b.repr) x) i

theorem basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] (b : basis ι R M) :

Any basis is a maximal linear independent set.

@[protected]

noncomputable def basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : ⊤ ≤ submodule.span R (set.range v)) :

basis ι R M

A linear independent family of vectors spanning the whole module is a basis.

Equations

basis.mk hli hsp = {repr := {to_fun := (hli.repr.comp (linear_map.cod_restrict (submodule.span R (set.range v)) linear_map.id _)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(finsupp.total ι M R v), left_inv := _, right_inv := _}}

@[simp]

theorem basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {x : M} (hli : linear_independent R v) (hsp : ⊤ ≤ submodule.span R (set.range v)) :

⇑((basis.mk hli hsp).repr) x = ⇑(hli.repr) ⟨x, _⟩

theorem basis.mk_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : ⊤ ≤ submodule.span R (set.range v)) (i : ι) :

⇑(basis.mk hli hsp) i = v i

@[simp]

theorem basis.coe_mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (hsp : ⊤ ≤ submodule.span R (set.range v)) :

⇑(basis.mk hli hsp) = v

theorem basis.mk_coord_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {hli : linear_independent R v} {hsp : ⊤ ≤ submodule.span R (set.range v)} (i : ι) :

⇑((basis.mk hli hsp).coord i) (v i) = 1

Given a basis, the ith element of the dual basis evaluates to 1 on the ith element of the basis.

theorem basis.mk_coord_apply_ne {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {hli : linear_independent R v} {hsp : ⊤ ≤ submodule.span R (set.range v)} {i j : ι} (h : j ≠ i) :

⇑((basis.mk hli hsp).coord i) (v j) = 0

Given a basis, the ith element of the dual basis evaluates to 0 on the jth element of the basis if j ≠ i.

theorem basis.mk_coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {hli : linear_independent R v} {hsp : ⊤ ≤ submodule.span R (set.range v)} {i j : ι} :

⇑((basis.mk hli hsp).coord i) (v j) = ite (j = i) 1 0

Given a basis, the ith element of the dual basis evaluates to the Kronecker delta on the jth element of the basis.

@[protected]

noncomputable def basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) :

basis ι R ↥(submodule.span R (set.range v))

A linear independent family of vectors is a basis for their span.

Equations

basis.span hli = basis.mk _ basis.span._proof_3

@[protected]

theorem basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hli : linear_independent R v) (i : ι) :

↑(⇑(basis.span hli) i) = v i

theorem basis.group_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] {v : ι → M} (hv : submodule.span R (set.range v) = ⊤) {w : ι → G} :

submodule.span R (set.range (w • v)) = ⊤

noncomputable def basis.group_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] [smul_comm_class G R M] (v : basis ι R M) (w : ι → G) :

basis ι R M

Given a basis v and a map w such that for all i, w i are elements of a group, group_smul provides the basis corresponding to w • v.

Equations

v.group_smul w = basis.mk _ _

theorem basis.group_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] [smul_comm_class G R M] {v : basis ι R M} {w : ι → G} (i : ι) :

⇑(v.group_smul w) i = (w • ⇑v) i

theorem basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : ι → M} (hv : submodule.span R (set.range v) = ⊤) {w : ι → Rˣ} :

submodule.span R (set.range (w • v)) = ⊤

noncomputable def basis.units_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] (v : basis ι R M) (w : ι → Rˣ) :

basis ι R M

Given a basis v and a map w such that for all i, w i is a unit, smul_of_is_unit provides the basis corresponding to w • v.

Equations

v.units_smul w = basis.mk _ _

theorem basis.units_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : basis ι R M} {w : ι → Rˣ} (i : ι) :

⇑(v.units_smul w) i = w i • ⇑v i

noncomputable def basis.is_unit_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] (v : basis ι R M) {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) :

basis ι R M

A version of smul_of_units that uses is_unit.

Equations

v.is_unit_smul hw = v.units_smul (λ (i : ι), _.unit)

theorem basis.is_unit_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : basis ι R M} {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) (i : ι) :

⇑(v.is_unit_smul hw) i = w i • ⇑v i

noncomputable def basis.mk_fin_cons {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {n : ℕ} {N : submodule R M} (y : M) (b : basis (fin n) R ↥N) (hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) :

basis (fin (n + 1)) R M

Let b be a basis for a submodule N of M. If y : M is linear independent of N and y and N together span the whole of M, then there is a basis for M whose basis vectors are given by fin.cons y b.

Equations

basis.mk_fin_cons y b hli hsp = have span_b : submodule.span R (set.range (⇑(N.subtype) ∘ ⇑b)) = N, from _, basis.mk _ _

@[simp]

theorem basis.coe_mk_fin_cons {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {n : ℕ} {N : submodule R M} (y : M) (b : basis (fin n) R ↥N) (hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) :

⇑(basis.mk_fin_cons y b hli hsp) = fin.cons y (coe ∘ ⇑b)

noncomputable def basis.mk_fin_cons_of_le {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {n : ℕ} {N O : submodule R M} (y : M) (yO : y ∈ O) (b : basis (fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0) (hsp : ∀ (z : M), z ∈ O → (∃ (c : R), z + c • y ∈ N)) :

basis (fin (n + 1)) R ↥O

Let b be a basis for a submodule N ≤ O. If y ∈ O is linear independent of N and y and N together span the whole of O, then there is a basis for O whose basis vectors are given by fin.cons y b.

Equations

basis.mk_fin_cons_of_le y yO b hNO hli hsp = basis.mk_fin_cons ⟨y, yO⟩ (b.map (submodule.comap_subtype_equiv_of_le hNO).symm) _ _

@[simp]

theorem basis.coe_mk_fin_cons_of_le {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {n : ℕ} {N O : submodule R M} (y : M) (yO : y ∈ O) (b : basis (fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0) (hsp : ∀ (z : M), z ∈ O → (∃ (c : R), z + c • y ∈ N)) :

⇑(basis.mk_fin_cons_of_le y yO b hNO hli hsp) = fin.cons ⟨y, yO⟩ (⇑(submodule.of_le hNO) ∘ ⇑b)

@[protected]

noncomputable def basis.fin_two_prod (R : Type u_1) [semiring R] :

basis (fin 2) R (R × R)

The basis of R × R given by the two vectors (1, 0) and (0, 1).

Equations

basis.fin_two_prod R = basis.of_equiv_fun (linear_equiv.fin_two_arrow R R).symm

@[simp]

theorem basis.fin_two_prod_zero (R : Type u_1) [semiring R] :

⇑(basis.fin_two_prod R) 0 = (1, 0)

@[simp]

theorem basis.fin_two_prod_one (R : Type u_1) [semiring R] :

⇑(basis.fin_two_prod R) 1 = (0, 1)

@[simp]

theorem basis.coe_fin_two_prod_repr {R : Type u_1} [semiring R] (x : R × R) :

⇑(⇑((basis.fin_two_prod R).repr) x) = ![x.fst, x.snd]

def submodule.induction_on_rank_aux {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [is_domain R] [add_comm_group M] [module R M] (b : basis ι R M) (P : submodule R M → Sort u_2) (ih : Π (N : submodule R M), (Π (N' : submodule R M), N' ≤ N → Π (x : M), x ∈ N → (∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0) → P N') → P N) (n : ℕ) (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n) :

P N

If N is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

Equations

submodule.induction_on_rank_aux b P ih n N rank_le = nat.rec (λ (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ 0), _.mpr (ih ⊥ (λ (N : submodule R M) (N_le : N ≤ ⊥) (x : M) (x_mem : x ∈ ⊥) (x_ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0), false.rec (P N) _))) (λ (n : ℕ) (rank_ih : Π (N : submodule R M), (∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n) → P N) (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n.succ), ih N (λ (N' : submodule R M) (N'_le : N' ≤ N) (x : M) (x_mem : x ∈ N) (x_ortho : ∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0), rank_ih N' _)) n N rank_le

noncomputable def basis.extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :

basis ↥(hs.extend _) K V

If s is a linear independent set of vectors, we can extend it to a basis.

Equations

basis.extend hs = basis.mk _ _

theorem basis.extend_apply_self {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) (x : ↥(hs.extend _)) :

⇑(basis.extend hs) x = ↑x

@[simp]

theorem basis.coe_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :

⇑(basis.extend hs) = coe

theorem basis.range_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :

set.range ⇑(basis.extend hs) = hs.extend _

noncomputable def basis.sum_extend {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : ι → V} (hs : linear_independent K v) :

basis (ι ⊕ ↥(_.extend basis.sum_extend._proof_2 \ set.range v)) K V

If v is a linear independent family of vectors, extend it to a basis indexed by a sum type.

Equations

basis.sum_extend hs = let s : set V := set.range v, e : ι ≃ ↥s := equiv.of_injective v _, b : set V := _.extend basis.sum_extend._proof_5 in (basis.extend _).reindex ((e.sum_congr (equiv.refl ↥(b \ s))).trans (equiv.set.sum_diff_subset _ (λ (a : V), classical.prop_decidable ((λ (_x : V), _x ∈ s) a)))).symm

theorem basis.subset_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} (hs : linear_independent K coe) :

s ⊆ hs.extend _

def basis.of_vector_space_index (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

A set used to index basis.of_vector_space.

Equations

basis.of_vector_space_index K V = _.extend _

Instances for ↥basis.of_vector_space_index

noncomputable def basis.of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

basis ↥(basis.of_vector_space_index K V) K V

Each vector space has a basis.

Equations

basis.of_vector_space K V = basis.extend _

theorem basis.of_vector_space_apply_self (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] (x : ↥(basis.of_vector_space_index K V)) :

⇑(basis.of_vector_space K V) x = ↑x

@[simp]

theorem basis.coe_of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

⇑(basis.of_vector_space K V) = coe

theorem basis.of_vector_space_index.linear_independent (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

linear_independent K coe

theorem basis.range_of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

set.range ⇑(basis.of_vector_space K V) = basis.of_vector_space_index K V

theorem basis.exists_basis (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] :

∃ (s : set V), nonempty (basis ↥s K V)

theorem vector_space.card_fintype (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V] [fintype K] [fintype V] :

∃ (n : ℕ), fintype.card V = fintype.card K ^ n

theorem nonzero_span_atom {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (v : V) (hv : v ≠ 0) :

is_atom (submodule.span K {v})

For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.

theorem atom_iff_nonzero_span {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] (W : submodule K V) :

is_atom W ↔ ∃ (v : V) (hv : v ≠ 0), W = submodule.span K {v}

The atoms of the lattice of submodules of a module over a division ring are the submodules equal to the span of a nonzero element of the module.

@[protected, instance]

def submodule.is_atomistic {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] :

is_atomistic (submodule K V)

The lattice of submodules of a module over a division ring is atomistic.

theorem linear_map.exists_left_inverse_of_injective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_inj : linear_map.ker f = ⊥) :

∃ (g : V' →ₗ[K] V), g.comp f = linear_map.id

theorem submodule.exists_is_compl {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) :

∃ (q : submodule K V), is_compl p q

@[protected, instance]

def module.submodule.complemented_lattice {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] :

complemented_lattice (submodule K V)

theorem linear_map.exists_right_inverse_of_surjective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] (f : V →ₗ[K] V') (hf_surj : linear_map.range f = ⊤) :

∃ (g : V' →ₗ[K] V), f.comp g = linear_map.id

theorem linear_map.exists_extend {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V'] {p : submodule K V} (f : ↥p →ₗ[K] V') :

∃ (g : V →ₗ[K] V'), g.comp p.subtype = f

Any linear map f : p →ₗ[K] V' defined on a subspace p can be extended to the whole space.

theorem submodule.exists_le_ker_of_lt_top {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) (hp : p < ⊤) :

∃ (f : V →ₗ[K] K) (H : f ≠ 0), p ≤ linear_map.ker f

If p < ⊤ is a subspace of a vector space V, then there exists a nonzero linear map f : V →ₗ[K] K such that p ≤ ker f.

theorem quotient_prod_linear_equiv {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [module K V] (p : submodule K V) :

nonempty (((V ⧸ p) × ↥p) ≃ₗ[K] V)