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.ofRepr.

• If ι is finite, there is a variant of repr called Basis.equivFun b : M ≃ₗ[R] ι → R (saving you from having to work with Finsupp). The converse, turning this isomorphism into a basis, is called Basis.ofEquivFun.

• 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.

• Basis.constr: given b : Basis ι R M and f : ι → M, construct a linear map g so that g (b i) = f i.

• Basis.coord: b.coord i x is the i-th coordinate of a vector x with respect to the basis b.

Main results

• 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.

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 Module.Basis (ι : Type u_1) (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max (max u_1 u_3) u_4)

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

The basis vectors are available as DFunLike.coe (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.

• ofRepr :: (
• repr : M ≃ₗ[R] ι →₀ R

  repr is the linear equivalence sending a vector x to its coordinates: the cs such that x = ∑ i, c i.

• )

@[instance_reducible]

noncomputable instance Module.Basis.instInhabitedFinsupp {ι : Type u_1} {R : Type u_3} [Semiring R] : Inhabited (Basis ι R (ι →₀ R))

Equations

• Module.Basis.instInhabitedFinsupp = { default := { repr := LinearEquiv.refl R (ι →₀ R) } }

theorem Module.Basis.repr_injective {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : Function.Injective repr

@[instance_reducible]

noncomputable instance Module.Basis.instFunLike {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : FunLike (Basis ι R M) ι M

b i is the ith basis vector.

Equations

• Module.Basis.instFunLike = { coe := fun (b : Module.Basis ι R M) (i : ι) => b.repr.symm (Finsupp.single i 1), coe_injective := ⋯ }

@[simp]

theorem Module.Basis.coe_ofRepr {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] ι →₀ R) : ⇑{ repr := e } = fun (i : ι) => e.symm (Finsupp.single i 1)

theorem Module.Basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] : Function.Injective ⇑b

theorem Module.Basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : b.repr.symm (Finsupp.single i 1) = b i

theorem Module.Basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (c : R) : b.repr.symm (Finsupp.single i c) = c • b i

@[simp]

theorem Module.Basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : b.repr (b i) = Finsupp.single i 1

theorem Module.Basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i j : ι) [Decidable (i = j)] : (b.repr (b i)) j = if i = j then 1 else 0

@[simp]

theorem Module.Basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) : b.repr.symm v = (Finsupp.linearCombination R ⇑b) v

@[simp]

theorem Module.Basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : ↑b.repr.symm = Finsupp.linearCombination R ⇑b

@[simp]

theorem Module.Basis.repr_linearCombination {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) : b.repr ((Finsupp.linearCombination R ⇑b) v) = v

@[simp]

theorem Module.Basis.linearCombination_repr {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) : (Finsupp.linearCombination R ⇑b) (b.repr x) = x

noncomputable def Module.Basis.map {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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 ≪≫ₗ b.repr }

@[simp]

theorem Module.Basis.map_repr {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).repr = f.symm ≪≫ₗ b.repr

@[simp]

theorem Module.Basis.map_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') (i : ι) : (b.map f) i = f (b i)

theorem Module.Basis.coe_map {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : ⇑(b.map f) = ⇑f ∘ ⇑b

noncomputable def Module.Basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid 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 ≪≫ₗ Finsupp.domLCongr e }

theorem Module.Basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') (i' : ι') : (b.reindex e) i' = b (e.symm i')

@[simp]

theorem Module.Basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') : ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm

theorem Module.Basis.repr_reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid 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 Module.Basis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (e : ι ≃ ι') : (b.reindex e).repr x = Finsupp.equivMapDomain e (b.repr x)

@[simp]

theorem Module.Basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : b.reindex (Equiv.refl ι) = b

theorem Module.Basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') : Set.range ⇑(b.reindex e) = Set.range ⇑b

simp can prove this as Basis.coe_reindex + EquivLike.range_comp

noncomputable def Module.Basis.equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (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.equivFun = b.repr ≪≫ₗ let __src := Finsupp.equivFunOnFinite; { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

noncomputable def Module.fintypeOfFintype {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) [Fintype R] : Fintype M

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

Equations

• Module.fintypeOfFintype b = Fintype.ofEquiv (ι → R) b.equivFun.toEquiv.symm

@[simp]

theorem Module.Basis.equivFun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (x : ι → R) : b.equivFun.symm x = ∑ 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 Module.Basis.equivFun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (u : M) : b.equivFun u = ⇑(b.repr u)

@[simp]

theorem Module.Basis.map_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Finite ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).equivFun = f.symm ≪≫ₗ b.equivFun

theorem Module.Basis.sum_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) : ∑ i : ι, b.equivFun u i • b i = u

@[simp]

theorem Module.Basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) : ∑ i : ι, (b.repr u) i • b i = u

@[simp]

theorem Module.Basis.equivFun_self {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [DecidableEq ι] (b : Basis ι R M) (i j : ι) : b.equivFun (b i) j = if i = j then 1 else 0

theorem Module.Basis.repr_sum_self {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (c : ι → R) : ⇑(b.repr (∑ i : ι, c i • b i)) = c

noncomputable def Module.Basis.ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (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

• Module.Basis.ofEquivFun e = { repr := e ≪≫ₗ (Finsupp.linearEquivFunOnFinite R R ι).symm }

@[simp]

theorem Module.Basis.ofEquivFun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) : ((ofEquivFun e).repr x) i = e x i

@[simp]

theorem Module.Basis.coe_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) : ⇑(ofEquivFun e) = fun (i : ι) => e.symm (Pi.single i 1)

@[simp]

theorem Module.Basis.ofEquivFun_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (v : Basis ι R M) : ofEquivFun v.equivFun = v

@[simp]

theorem Module.Basis.equivFun_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ι → R) : (ofEquivFun e).equivFun = e

theorem Module.Basis.ext {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_10} [Semiring R₁] {σ : R →+* R₁} {M₁ : Type u_11} [AddCommMonoid 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 Module.Basis.ext' {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_10} [Semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M₁ : Type u_11} [AddCommMonoid 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 Module.Basis.ext_elem_iff {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x y : M} : x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i

Two elements are equal iff their coordinates are equal.

theorem Module.Basis.ext_elem {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x y : M} : (∀ (i : ι), (b.repr x) i = (b.repr y) i) → x = y

Alias of the reverse direction of Module.Basis.ext_elem_iff.

---

Two elements are equal iff their coordinates are equal.

theorem Module.Basis.repr_eq_iff {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {f : M →ₗ[R] ι →₀ R} : ↑b.repr = f ↔ ∀ (i : ι), f (b i) = Finsupp.single i 1

theorem Module.Basis.repr_eq_iff' {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {f : M ≃ₗ[R] ι →₀ R} : b.repr = f ↔ ∀ (i : ι), f (b i) = Finsupp.single i 1

theorem Module.Basis.apply_eq_iff {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {x : M} {i : ι} : b i = x ↔ b.repr x = Finsupp.single i 1

theorem Module.Basis.repr_apply_eq {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid 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 Module.Basis.eq_ofRepr_eq_repr {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid 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.

theorem Module.Basis.eq_of_apply_eq {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ : Basis ι R M} : (∀ (i : ι), b₁ i = b₂ i) → b₁ = b₂

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

theorem Module.Basis.eq_of_apply_eq_iff {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ : Basis ι R M} : b₁ = b₂ ↔ ∀ (i : ι), b₁ i = b₂ i

noncomputable def Module.Basis.mapCoeffs {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_10} [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.algebraMapCoeffs for the case where f is equal to algebraMap.

Equations

• b.mapCoeffs f h = { repr := LinearEquiv.restrictScalars R' b.repr ≪≫ₗ Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm }

@[simp]

theorem Module.Basis.mapCoeffs_repr {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_10} [Semiring R'] [Module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c • x = c • x) : (b.mapCoeffs f h).repr = LinearEquiv.restrictScalars R' b.repr ≪≫ₗ Finsupp.mapRange.linearEquiv (compHom.toLinearEquiv f.symm).symm

theorem Module.Basis.mapCoeffs_apply {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_10} [Semiring R'] [Module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c • x = c • x) (i : ι) : (b.mapCoeffs f h) i = b i

@[simp]

theorem Module.Basis.coe_mapCoeffs {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_10} [Semiring R'] [Module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c • x = c • x) : ⇑(b.mapCoeffs f h) = ⇑b

noncomputable def Module.Basis.reindexRange {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Basis (↑(Set.range ⇑b)) R M

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

Equations

• b.reindexRange = if h : Nontrivial R then b.reindex (Equiv.ofInjective ⇑b ⋯) else { repr := Module.subsingletonEquiv R M ↑(Set.range ⇑b) }

theorem Module.Basis.reindexRange_self {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (h : b i ∈ Set.range ⇑b := ⋯) : b.reindexRange ⟨b i, h⟩ = b i

theorem Module.Basis.reindexRange_repr_self {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : b.reindexRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1

@[simp]

theorem Module.Basis.reindexRange_apply {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : ↑(Set.range ⇑b)) : b.reindexRange x = ↑x

theorem Module.Basis.reindexRange_repr' {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi) : (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

@[simp]

theorem Module.Basis.reindexRange_repr {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (i : ι) (h : b i ∈ Set.range ⇑b := ⋯) : (b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i

noncomputable def Module.Basis.reindexFinsetRange {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] : Basis (↥(Finset.image (⇑b) Finset.univ)) R M

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

Equations

• b.reindexFinsetRange = b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)

theorem Module.Basis.reindexFinsetRange_self {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) (h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯) : b.reindexFinsetRange ⟨b i, h⟩ = b i

@[simp]

theorem Module.Basis.reindexFinsetRange_apply {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : ↥(Finset.image (⇑b) Finset.univ)) : b.reindexFinsetRange x = ↑x

theorem Module.Basis.reindexFinsetRange_repr_self {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) : b.reindexFinsetRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1

@[simp]

theorem Module.Basis.reindexFinsetRange_repr {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : M) (i : ι) (h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯) : (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i

noncomputable def Module.Basis.constr {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] : (ι → M') ≃ₗ[S] M →ₗ[R] M'

Construct a linear map given the value at the basis, called Basis.constr b S f where b is a basis, f is the value of the linear map over the elements of the basis, and S is an extra semiring (typically S = R or S = ℕ).

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

Equations

• One or more equations did not get rendered due to their size.

theorem Module.Basis.constr_def {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') : (b.constr S) f = Finsupp.linearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr

theorem Module.Basis.constr_apply {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') (x : M) : ((b.constr S) f) x = (b.repr x).sum fun (b : ι) (a : R) => a • f b

@[simp]

theorem Module.Basis.constr_symm_apply {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M →ₗ[R] M') (i : ι) : (b.constr S).symm f i = f (b i)

@[simp]

theorem Module.Basis.constr_basis {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') (i : ι) : ((b.constr S) f) (b i) = f i

theorem Module.Basis.constr_eq {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ (i : ι), g i = f (b i)) : (b.constr S) g = f

theorem Module.Basis.constr_self {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M →ₗ[R] M') : ((b.constr S) fun (i : ι) => f (b i)) = f

theorem Module.Basis.constr_range {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] {f : ι → M'} : ((b.constr S) f).range = Submodule.span R (Set.range f)

@[simp]

theorem Module.Basis.constr_comp {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M' →ₗ[R] M') (v : ι → M') : (b.constr S) (⇑f ∘ v) = f ∘ₗ (b.constr S) v

@[simp]

theorem Module.Basis.constr_apply_fintype {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Module R M'] (S : Type u_11) [Semiring S] [Module S M'] [SMulCommClass R S M'] [Fintype ι] (b : Basis ι R M) (f : ι → M') (x : M) : ((b.constr S) f) x = ∑ i : ι, b.equivFun x i • f i

noncomputable def Module.Basis.equiv {ι' : Type u_2} {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (b' : Basis ι' R M') (e : ι ≃ ι') : M ≃ₗ[R] M'

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 ≪≫ₗ (b'.reindex e.symm).repr.symm

@[simp]

theorem Module.Basis.equiv_apply {ι' : Type u_2} {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (i : ι) (b' : Basis ι' R M') (e : ι ≃ ι') : (b.equiv b' e) (b i) = b' (e i)

@[simp]

theorem Module.Basis.equiv_refl {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M

@[simp]

theorem Module.Basis.equiv_symm {ι' : Type u_2} {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (b' : Basis ι' R M') (e : ι ≃ ι') : (b.equiv b' e).symm = b'.equiv b e.symm

@[simp]

theorem Module.Basis.equiv_trans {ι' : Type u_2} {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] {M'' : Type u_10} (b' : Basis ι' R M') [AddCommMonoid M''] [Module R M''] {ι'' : Type u_11} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') : b.equiv b' e ≪≫ₗ b'.equiv b'' e' = b.equiv b'' (e.trans e')

@[simp]

theorem Module.Basis.map_equiv {ι' : Type u_2} {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') : b.map (b.equiv b' e) = b'.reindex e.symm

noncomputable def Module.Basis.equiv' {ι' : Type u_2} {ι : Type u_7} {R : Type u_11} {M : Type u_12} {M' : Type u_13} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') [SMulCommClass R 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) : M ≃ₗ[R] M'

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 = { toLinearMap := (b.constr R) (f ∘ ⇑b), invFun := ⇑((b'.constr R) (g ∘ ⇑b')), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Module.Basis.equiv'_apply {ι' : Type u_2} {ι : Type u_7} {R : Type u_11} {M : Type u_12} {M' : Type u_13} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') [SMulCommClass R 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 Module.Basis.equiv'_symm_apply {ι' : Type u_2} {ι : Type u_7} {R : Type u_11} {M : Type u_12} {M' : Type u_13} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') [SMulCommClass R 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 Module.Basis.sum_repr_mul_repr {ι : Type u_7} {R : Type u_11} {M : Type u_12} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {ι' : Type u_14} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) : ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i

noncomputable def Module.Basis.coord {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : M →ₗ[R] R

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 ∘ₗ ↑b.repr

@[simp]

theorem Module.Basis.coord_apply {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (x : M) : (b.coord i) x = (b.repr x) i

theorem Module.Basis.forall_coord_eq_zero_iff {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} : (∀ (i : ι), (b.coord i) x = 0) ↔ x = 0

noncomputable def Module.Basis.sumCoords {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : M →ₗ[R] R

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

Equations

• b.sumCoords = ((Finsupp.lsum ℕ) fun (x : ι) => LinearMap.id) ∘ₗ ↑b.repr

@[simp]

theorem Module.Basis.coe_sumCoords {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : ⇑b.sumCoords = fun (m : M) => (b.repr m).sum fun (x : ι) => id

@[simp]

theorem Module.Basis.coe_sumCoords_of_fintype {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] : ⇑b.sumCoords = ⇑(∑ i : ι, b.coord i)

@[simp]

theorem Module.Basis.sumCoords_self_apply {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : b.sumCoords (b i) = 1

theorem Module.Basis.dvd_coord_smul {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (m : M) (r : R) : r ∣ (b.coord i) (r • m)

theorem Module.Basis.coord_repr_symm {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (f : ι →₀ R) : (b.coord i) (b.repr.symm f) = f i

theorem Module.Basis.coe_sumCoords_eq_finsum {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : ⇑b.sumCoords = fun (m : M) => ∑ᶠ (i : ι), (b.coord i) m

@[simp]

theorem Module.Basis.sumCoords_reindex {ι' : Type u_2} {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') : (b.reindex e).sumCoords = b.sumCoords

theorem Module.Basis.coord_equivFun_symm {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (i : ι) (f : ι → R) : (b.coord i) (b.equivFun.symm f) = f i