# 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

source
structure Module.Basis (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
Type (max (max u_1 u_3) u_6)

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 `c`s such that `x = ∑ i, c i`.

- )

Instances For

source
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) } }

source
theorem Module.Basis.repr_injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] :
Function.Injective repr
source
instance Module.Basis.instFunLike {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] :
FunLike (Basis ι R M) ι M

`b i` is the `i`th basis vector.

Equations

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

source
@[simp]
theorem Module.Basis.coe_ofRepr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] ι →₀ R) :
⇑{ repr := e } = fun (i : ι) => e.symm (Finsupp.single i 1)
source
theorem Module.Basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] :
Function.Injective ⇑b
source
theorem Module.Basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
b.repr.symm (Finsupp.single i 1) = b i
source
theorem Module.Basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (c : R) :
b.repr.symm (Finsupp.single i c) = c • b i
source
@[simp]
theorem Module.Basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
b.repr (b i) = Finsupp.single i 1
source
theorem Module.Basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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
source
@[simp]
theorem Module.Basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) :
b.repr.symm v = (Finsupp.linearCombination R ⇑b) v
source
@[simp]
theorem Module.Basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
↑b.repr.symm = Finsupp.linearCombination R ⇑b
source
@[simp]
theorem Module.Basis.repr_linearCombination {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) :
b.repr ((Finsupp.linearCombination R ⇑b) v) = v
source
@[simp]
theorem Module.Basis.linearCombination_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) :
(Finsupp.linearCombination R ⇑b) (b.repr x) = x
source
def Module.Basis.map {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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 }

Instances For

source
@[simp]
theorem Module.Basis.map_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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
source
@[simp]
theorem Module.Basis.map_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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)
source
theorem Module.Basis.coe_map {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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
source
def Module.Basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [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 }

Instances For

source
theorem Module.Basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') (i' : ι') :
(b.reindex e) i' = b (e.symm i')
source
@[simp]
theorem Module.Basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') :
⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
source
theorem Module.Basis.repr_reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [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')
source
@[simp]
theorem Module.Basis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (e : ι ≃ ι') :
(b.reindex e).repr x = Finsupp.mapDomain (⇑e) (b.repr x)
source
@[simp]
theorem Module.Basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
b.reindex (Equiv.refl ι) = b
source
theorem Module.Basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [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`

source
def Module.Basis.equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 := ⋯ }

Instances For

source
def Module.fintypeOfFintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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

Instances For

source
theorem Module.card_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) [Fintype R] [Fintype M] :
Fintype.card M = Fintype.card R ^ Fintype.card ι
source
@[simp]
theorem Module.Basis.equivFun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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`.

source
@[simp]
theorem Module.Basis.equivFun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (u : M) :
b.equivFun u = ⇑(b.repr u)
source
@[simp]
theorem Module.Basis.map_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [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
source
theorem Module.Basis.sum_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) :
∑ i : ι, b.equivFun u i • b i = u
source
@[simp]
theorem Module.Basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) :
∑ i : ι, (b.repr u) i • b i = u
source
@[simp]
theorem Module.Basis.equivFun_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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
source
theorem Module.Basis.repr_sum_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (c : ι → R) :
⇑(b.repr (∑ i : ι, c i • b i)) = c
source
def Module.Basis.ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 }

Instances For

source
@[simp]
theorem Module.Basis.ofEquivFun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) :
((ofEquivFun e).repr x) i = e x i
source
@[simp]
theorem Module.Basis.coe_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) :
⇑(ofEquivFun e) = fun (i : ι) => e.symm (Pi.single i 1)
source
@[simp]
theorem Module.Basis.ofEquivFun_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (v : Basis ι R M) :
ofEquivFun v.equivFun = v
source
@[simp]
theorem Module.Basis.equivFun_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ι → R) :
(ofEquivFun e).equivFun = e
source
theorem Module.Basis.ext {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_13} [Semiring R₁] {σ : R →+* R₁} {M₁ : Type u_14} [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.

source
theorem Module.Basis.ext' {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_13} [Semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M₁ : Type u_14} [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.

source
theorem Module.Basis.ext_elem_iff {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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.

source
theorem Module.Basis.ext_elem {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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.

source
theorem Module.Basis.repr_eq_iff {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
theorem Module.Basis.repr_eq_iff' {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
theorem Module.Basis.apply_eq_iff {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {x : M} {i : ι} :
b i = x ↔ b.repr x = Finsupp.single i 1
source
theorem Module.Basis.repr_apply_eq {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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`

source
theorem Module.Basis.eq_ofRepr_eq_repr {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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.

source
theorem Module.Basis.eq_of_apply_eq {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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.

source
theorem Module.Basis.eq_of_apply_eq_iff {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ : Basis ι R M} :
b₁ = b₂ ↔ ∀ (i : ι), b₁ i = b₂ i
source
def Module.Basis.mapCoeffs {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_13} [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 }

Instances For

source
@[simp]
theorem Module.Basis.mapCoeffs_repr {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_13} [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
source
theorem Module.Basis.mapCoeffs_apply {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_13} [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
source
@[simp]
theorem Module.Basis.coe_mapCoeffs {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R' : Type u_13} [Semiring R'] [Module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c • x = c • x) :
⇑(b.mapCoeffs f h) = ⇑b
source
def Module.Basis.reindexRange {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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) }

Instances For

source
theorem Module.Basis.reindexRange_self {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
theorem Module.Basis.reindexRange_repr_self {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
b.reindexRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1
source
@[simp]
theorem Module.Basis.reindexRange_apply {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : ↑(Set.range ⇑b)) :
b.reindexRange x = ↑x
source
theorem Module.Basis.reindexRange_repr' {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
@[simp]
theorem Module.Basis.reindexRange_repr {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
def Module.Basis.reindexFinsetRange {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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 ⋯)

Instances For

source
theorem Module.Basis.reindexFinsetRange_self {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
@[simp]
theorem Module.Basis.reindexFinsetRange_apply {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : ↥(Finset.image (⇑b) Finset.univ)) :
b.reindexFinsetRange x = ↑x
source
theorem Module.Basis.reindexFinsetRange_repr_self {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
@[simp]
theorem Module.Basis.reindexFinsetRange_repr {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
def Module.Basis.constr {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [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.

Instances For

source
theorem Module.Basis.constr_def {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [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
source
theorem Module.Basis.constr_apply {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [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
source
@[simp]
theorem Module.Basis.constr_basis {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') (i : ι) :
((b.constr S) f) (b i) = f i
source
theorem Module.Basis.constr_eq {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [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
source
theorem Module.Basis.constr_self {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M →ₗ[R] M') :
((b.constr S) fun (i : ι) => f (b i)) = f
source
theorem Module.Basis.constr_range {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [Semiring S] [Module S M'] [SMulCommClass R S M'] {f : ι → M'} :
LinearMap.range ((b.constr S) f) = Submodule.span R (Set.range f)
source
@[simp]
theorem Module.Basis.constr_comp {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] (S : Type u_13) [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
source
@[simp]
theorem Module.Basis.constr_apply_fintype {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] [Module R M'] (S : Type u_14) [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
source
def Module.Basis.equiv {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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

Instances For

source
@[simp]
theorem Module.Basis.equiv_apply {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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)
source
@[simp]
theorem Module.Basis.equiv_refl {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M
source
@[simp]
theorem Module.Basis.equiv_symm {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
@[simp]
theorem Module.Basis.equiv_trans {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Module R M'] {M'' : Type u_13} (b' : Basis ι' R M') [AddCommMonoid M''] [Module R M''] {ι'' : Type u_14} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :
b.equiv b' e ≪≫ₗ b'.equiv b'' e' = b.equiv b'' (e.trans e')
source
@[simp]
theorem Module.Basis.map_equiv {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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
source
def Module.Basis.equiv' {ι' : Type u_2} {ι : Type u_10} {R : Type u_14} {M : Type u_15} {M' : Type u_16} [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 := ⋯ }

Instances For

source
@[simp]
theorem Module.Basis.equiv'_apply {ι' : Type u_2} {ι : Type u_10} {R : Type u_14} {M : Type u_15} {M' : Type u_16} [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)
source
@[simp]
theorem Module.Basis.equiv'_symm_apply {ι' : Type u_2} {ι : Type u_10} {R : Type u_14} {M : Type u_15} {M' : Type u_16} [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)
source
theorem Module.Basis.sum_repr_mul_repr {ι : Type u_10} {R : Type u_14} {M : Type u_15} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {ι' : Type u_17} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) :
∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i
source
def Module.Basis.coord {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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

Instances For

source
@[simp]
theorem Module.Basis.coord_apply {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (a✝ : M) :
(b.coord i) a✝ = (b.repr a✝) i
source
theorem Module.Basis.forall_coord_eq_zero_iff {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} :
(∀ (i : ι), (b.coord i) x = 0) ↔ x = 0
source
noncomputable def Module.Basis.sumCoords {ι : Type u_10} {R : Type u_11} {M : Type u_12} [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

Instances For

source
@[simp]
theorem Module.Basis.coe_sumCoords {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
⇑b.sumCoords = fun (m : M) => (b.repr m).sum fun (x : ι) => id
source
@[simp]
theorem Module.Basis.coe_sumCoords_of_fintype {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] :
⇑b.sumCoords = ⇑(∑ i : ι, b.coord i)
source
@[simp]
theorem Module.Basis.sumCoords_self_apply {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
b.sumCoords (b i) = 1
source
theorem Module.Basis.dvd_coord_smul {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (m : M) (r : R) :
r ∣ (b.coord i) (r • m)
source
theorem Module.Basis.coord_repr_symm {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (f : ι →₀ R) :
(b.coord i) (b.repr.symm f) = f i
source
theorem Module.Basis.coe_sumCoords_eq_finsum {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
⇑b.sumCoords = fun (m : M) => ∑ᶠ (i : ι), (b.coord i) m
source
@[simp]
theorem Module.Basis.sumCoords_reindex {ι' : Type u_2} {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ≃ ι') :
(b.reindex e).sumCoords = b.sumCoords
source
theorem Module.Basis.coord_equivFun_symm {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (i : ι) (f : ι → R) :
(b.coord i) (b.equivFun.symm f) = f i