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.constr b R 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.

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

• )

instance uniqueBasis {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : Unique (Basis ι R M)

Equations

• uniqueBasis = { default := { repr := default }, uniq := ⋯ }

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

Equations

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

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

instance 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 ith basis vector.

Equations

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

@[simp]

theorem 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)

theorem 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

theorem 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

theorem 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

@[simp]

theorem 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

theorem 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

@[simp]

theorem 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.total ι M R ⇑b) v

@[simp]

theorem 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.total ι M R ⇑b

@[simp]

theorem Basis.repr_total {ι : 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.total ι M R ⇑b) v) = v

@[simp]

theorem Basis.total_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.total ι M R ⇑b) (b.repr x) = x

theorem Basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : LinearMap.range ↑b.repr = Finsupp.supported R R Set.univ

theorem Basis.mem_span_repr_support {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (m : M) : m ∈ Submodule.span R (⇑b '' ↑(b.repr m).support)

theorem Basis.repr_support_subset_of_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (s : Set ι) {m : M} (hm : m ∈ Submodule.span R (⇑b '' s)) : ↑(b.repr m).support ⊆ s

theorem Basis.mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {m : M} {s : Set ι} : m ∈ Submodule.span R (⇑b '' s) ↔ ↑(b.repr m).support ⊆ s

@[simp]

theorem Basis.self_mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] {i : ι} {s : Set ι} : b i ∈ Submodule.span R (⇑b '' s) ↔ i ∈ s

@[simp]

theorem Basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : ∀ (a : M), (b.coord i) a = (b.repr a) i

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

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

noncomputable def Basis.sumCoords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.coe_sumCoords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : ⇑b.sumCoords = fun (m : M) => (b.repr m).sum fun (x : ι) => id

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

@[simp]

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

@[simp]

theorem Basis.sumCoords_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 : ι) : b.sumCoords (b i) = 1

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

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

theorem Basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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₁ : M →ₛₗ[σ] M₁} {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_6} [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₁ : M ≃ₛₗ[σ] M₁} {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_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} {y : M} : x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i

Two elements are equal iff their coordinates are equal.

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

Alias of the reverse direction of Basis.ext_elem_iff.

---

Two elements are equal iff their coordinates are equal.

theorem Basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.repr_eq_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.repr_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.eq_ofRepr_eq_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ : Basis ι R M} {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 Basis.eq_of_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ : Basis ι R M} {b₂ : Basis ι R M} : (∀ (i : ι), b₁ i = b₂ i) → b₁ = b₂

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

@[simp]

theorem 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

def 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 }

@[simp]

theorem 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)

theorem 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

@[simp]

theorem Basis.mapCoeffs_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 (Module.compHom.toLinearEquiv f.symm).symm

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

theorem Basis.mapCoeffs_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.coe_mapCoeffs {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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

def 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 }

theorem 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')

@[simp]

theorem 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

theorem 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')

@[simp]

theorem 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)

@[simp]

theorem 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

theorem 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

@[simp]

theorem Basis.sumCoords_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).sumCoords = b.sumCoords

def Basis.reindexRange {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid 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.reindexRange = if h : Nontrivial R then b.reindex (Equiv.ofInjective ⇑b ⋯) else { repr := Module.subsingletonEquiv R M ↑(Set.range ⇑b) }

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

theorem Basis.reindexRange_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.reindexRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1

@[simp]

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

theorem Basis.reindexRange_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) {bi : M} {i : ι} (h : b i = bi) : (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

@[simp]

theorem Basis.reindexRange_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) (i : ι) (h : optParam (b i ∈ Set.range ⇑b) ⋯) : (b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i

def Basis.reindexFinsetRange {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] : Basis { x : M // x ∈ 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 Basis.reindexFinsetRange_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) (h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯) : b.reindexFinsetRange ⟨b i, h⟩ = b i

@[simp]

theorem Basis.reindexFinsetRange_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : { x : M // x ∈ Finset.image (⇑b) Finset.univ }) : b.reindexFinsetRange x = ↑x

theorem Basis.reindexFinsetRange_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [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 Basis.reindexFinsetRange_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : M) (i : ι) (h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯) : (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i

theorem Basis.linearIndependent {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : LinearIndependent R ⇑b

theorem Basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] (i : ι) : b i ≠ 0

theorem Basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) : x ∈ Submodule.span R (Set.range ⇑b)

@[simp]

theorem Basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid 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_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial M] : Nonempty ι

theorem Basis.mem_submodule_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {P : Submodule R M} (b : Basis ι R ↥P) {x : M} : x ∈ P ↔ ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) => x • ↑(b i)

If the submodule P has a basis, x ∈ P iff it is a linear combination of basis vectors.

def Basis.constr {ι : 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) (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 Basis.constr_def {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') : (b.constr S) f = Finsupp.total M' M' R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr

theorem Basis.constr_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) (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 Basis.constr_basis {ι : 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) (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 Basis.constr_eq {ι : 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) (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 Basis.constr_self {ι : 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) (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 Basis.constr_range {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] {f : ι → M'} : LinearMap.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_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι 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

def Basis.equiv {ι : Type u_1} {ι' : Type u_2} {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) (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 Basis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {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) (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_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M

@[simp]

theorem Basis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {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) (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_6} {M' : Type u_7} {M'' : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') [AddCommMonoid M''] [Module R M''] {ι'' : Type u_10} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') : b.equiv b' e ≪≫ₗ 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_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') : b.map (b.equiv b' e) = b'.reindex e.symm

def Basis.prod {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') : Basis (ι ⊕ ι') R (M × M')

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

Equations

• b.prod b' = { repr := b.repr.prod b'.repr ≪≫ₗ (Finsupp.sumFinsuppLEquivProdFinsupp R).symm }

@[simp]

theorem Basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (x : M × M') (i : ι) : ((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i

@[simp]

theorem Basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (x : M × M') (i : ι') : ((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i

theorem Basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (i : ι) : ((b.prod b') (Sum.inl i)).1 = b i

theorem Basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (i : ι') : ((b.prod b') (Sum.inr i)).1 = 0

theorem Basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (i : ι) : ((b.prod b') (Sum.inl i)).2 = 0

theorem Basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (i : ι') : ((b.prod b') (Sum.inr i)).2 = b' i

@[simp]

theorem Basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (i : ι ⊕ ι') : (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

theorem Basis.noZeroSMulDivisors {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) : NoZeroSMulDivisors R M

theorem Basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem Basis.eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M) (rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0) : N = ⊥

def Basis.singleton (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] : Basis ι R R

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

Equations

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

@[simp]

theorem Basis.singleton_apply (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] (i : ι) : (Basis.singleton ι R) i = 1

@[simp]

theorem Basis.singleton_repr (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] (x : R) (i : ι) : ((Basis.singleton ι R).repr x) i = x

theorem Basis.basis_singleton_iff {R : Type u_10} {M : Type u_11} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (ι : Type u_12) [Unique ι] : Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y

def Basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] : 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 }

instance Basis.emptyUnique {ι : Type u_1} {R : Type u_3} (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] : Unique (Basis ι R M)

Equations

• Basis.emptyUnique M = { default := Basis.empty M, uniq := ⋯ }

def 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 := ⋯ }

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

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 ι

@[simp]

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

@[simp]

theorem 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)

@[simp]

theorem 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

theorem 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

theorem 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

@[simp]

theorem 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

theorem 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

def 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

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

@[simp]

theorem 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 : ι) : ((Basis.ofEquivFun e).repr x) i = e x i

@[simp]

theorem 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) : ⇑(Basis.ofEquivFun e) = fun (i : ι) => e.symm (Function.update 0 i 1)

@[simp]

theorem 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) : Basis.ofEquivFun v.equivFun = v

@[simp]

theorem 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) : (Basis.ofEquivFun e).equivFun = e

@[simp]

theorem Basis.constr_apply_fintype {ι : 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'] (S : Type u_10) [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

theorem Basis.mem_submodule_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {P : Submodule R M} (b : Basis ι R ↥P) {x : M} : x ∈ P ↔ ∃ (c : ι → R), x = ∑ i : ι, c i • ↑(b i)

If the submodule P has a finite basis, x ∈ P iff it is a linear combination of basis vectors.

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

def Basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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) : 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 = let __src := (b.constr R) (f ∘ ⇑b); { toLinearMap := __src, invFun := ⇑((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_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {ι' : Type u_10} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) : ∑ 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_6} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] (b : Basis ι R M) : ⋯.Maximal

Any basis is a maximal linear independent set.

noncomputable def Basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent 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

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

@[simp]

theorem Basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {x : M} (hli : LinearIndependent 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_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent 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_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent 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_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent 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_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent 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_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} [DecidableEq ι] {i : ι} {j : ι} : ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

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

noncomputable def Basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent 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 ⋯ ⋯

theorem Basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) (i : ι) : ↑((Basis.span hli) i) = v i

theorem Basis.groupSMul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → G} : Submodule.span R (Set.range (w • v)) = ⊤

def Basis.groupSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass 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, groupSMul provides the basis corresponding to w • v.

Equations

• v.groupSMul w = Basis.mk ⋯ ⋯

theorem Basis.groupSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : Basis ι R M} {w : ι → G} (i : ι) : (v.groupSMul w) i = (w • ⇑v) i

theorem Basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} : Submodule.span R (Set.range (w • v)) = ⊤

def Basis.unitsSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup 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, unitsSMul provides the basis corresponding to w • v.

Equations

• v.unitsSMul w = Basis.mk ⋯ ⋯

theorem Basis.unitsSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : (v.unitsSMul w) i = w i • v i

@[simp]

theorem Basis.coord_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [CommRing R₂] [AddCommGroup M] [Module R₂ M] (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) : (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

@[simp]

theorem Basis.repr_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [CommRing R₂] [AddCommGroup M] [Module R₂ M] (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) : ((e.unitsSMul w).repr v) i = (w i)⁻¹ • (e.repr v) i

def Basis.isUnitSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] (v : Basis ι R M) {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) : Basis ι R M

A version of unitsSMul that uses IsUnit.

Equations

• v.isUnitSMul hw = v.unitsSMul fun (i : ι) => ⋯.unit

theorem Basis.isUnitSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : Basis ι R M} {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) (i : ι) : (v.isUnitSMul hw) i = w i • v i

noncomputable def Basis.mkFinCons {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R ↥N) (hli : ∀ (c : R), ∀ 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.mkFinCons y b hli hsp = let_fun span_b := ⋯; Basis.mk ⋯ ⋯

@[simp]

theorem Basis.coe_mkFinCons {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R ↥N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) : ⇑(Basis.mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

noncomputable def Basis.mkFinConsOfLE {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} {O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ 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.mkFinConsOfLE y yO b hNO hli hsp = Basis.mkFinCons ⟨y, yO⟩ (b.map (Submodule.comapSubtypeEquivOfLe hNO).symm) ⋯ ⋯

@[simp]

theorem Basis.coe_mkFinConsOfLE {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} {O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N) : ⇑(Basis.mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons ⟨y, yO⟩ (⇑(Submodule.inclusion hNO) ∘ ⇑b)

def Basis.finTwoProd (R : Type u_10) [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.finTwoProd R = Basis.ofEquivFun (LinearEquiv.finTwoArrow R R).symm

@[simp]

theorem Basis.finTwoProd_zero (R : Type u_10) [Semiring R] : (Basis.finTwoProd R) 0 = (1, 0)

@[simp]

theorem Basis.finTwoProd_one (R : Type u_10) [Semiring R] : (Basis.finTwoProd R) 1 = (0, 1)

@[simp]

theorem Basis.coe_finTwoProd_repr {R : Type u_10} [Semiring R] (x : R × R) : ⇑((Basis.finTwoProd R).repr x) = ![x.1, x.2]

def Submodule.inductionOnRankAux {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] (b : Basis ι R M) (P : Submodule R M → Sort u_10) (ih : (N : Submodule R M) → ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N) (n : ℕ) (N : Submodule R M) (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ 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

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

theorem Basis.mem_center_iff {ι : Type u_1} {R : Type u_3} {A : Type u_10} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A] (b : Basis ι R A) {z : A} : z ∈ Set.center A ↔ (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)

An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements.

noncomputable def Basis.restrictScalars {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) : Basis ι R ↥(Submodule.span R (Set.range ⇑b))

Let b be an S-basis of M. Let R be a CommRing such that Algebra R S has no zero smul divisors, then the submodule of M spanned by b over R admits b as an R-basis.

Equations

• Basis.restrictScalars R b = Basis.span ⋯

@[simp]

theorem Basis.restrictScalars_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (i : ι) : ↑((Basis.restrictScalars R b) i) = b i

@[simp]

theorem Basis.restrictScalars_repr_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : ↥(Submodule.span R (Set.range ⇑b))) (i : ι) : (algebraMap R S) (((Basis.restrictScalars R b).repr m) i) = (b.repr ↑m) i

theorem Basis.mem_span_iff_repr_mem {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : M) : m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)

Let b be an S-basis of M. Then m : M lies in the R-module spanned by b iff all the coordinates of m on the basis b are in R (see Basis.mem_span for the case R = S).

theorem basis_finite_of_finite_spans {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Nontrivial R] [Module R M] (w : Set M) (hw : w.Finite) (s : Submodule.span R w = ⊤) {ι : Type w} (b : Basis ι R M) : Finite ι

Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.

theorem union_support_maximal_linearIndependent_eq_range_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Nontrivial R] [Module R M] {ι : Type w} (b : Basis ι R M) {κ : Type w'} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : ⋃ (k : κ), ↑(b.repr (v k)).support = Set.univ

Over any ring R, if b is a basis for a module M, and s is a maximal linearly independent set, then the union of the supports of x ∈ s (when written out in the basis b) is all of b.

theorem infinite_basis_le_maximal_linearIndependent' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Nontrivial R] [Module R M] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w'} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

theorem infinite_basis_le_maximal_linearIndependent {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Nontrivial R] [Module R M] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : Cardinal.mk ι ≤ Cardinal.mk κ

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.