Bases

Further results on bases in modules and vector spaces.

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

theorem Basis.linearIndependent {ι : Type u_1} {R : Type u_3} {M : Type u_5} [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_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] (i : ι) : b i ≠ 0

def Basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} {M' : Type u_6} [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_5} [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_5} [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.basis_singleton_iff {R : Type u_7} {M : Type u_8} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (ι : Type u_9) [Unique ι] : Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y

noncomputable def Basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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_5} [Semiring R] [AddCommMonoid 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_5} [Semiring R] [AddCommMonoid 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_5} [Semiring R] [AddCommMonoid 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_5} [AddCommMonoid M] [CommSemiring R₂] [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_5} [AddCommMonoid M] [CommSemiring R₂] [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_5} [Semiring R] [AddCommMonoid 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : Basis ι R M} {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) (i : ι) : (v.isUnitSMul hw) i = w i • v i

theorem Basis.repr_isUnitSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_5} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)) (x : M) (i : ι) : ((v.isUnitSMul hw).repr x) i = ⋯.unit⁻¹ • (v.repr x) i

theorem Basis.eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup 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 = ⊥

theorem Basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_5} [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.mkFinCons {R : Type u_3} {M : Type u_5} [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 = Basis.mk ⋯ ⋯

@[simp]

theorem Basis.coe_mkFinCons {R : Type u_3} {M : Type u_5} [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_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ 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_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ 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_7) [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_7) [Semiring R] : (Basis.finTwoProd R) 0 = (1, 0)

@[simp]

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

@[simp]

theorem Basis.coe_finTwoProd_repr {R : Type u_7} [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_5} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] (b : Basis ι R M) (P : Submodule R M → Sort u_7) (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_7} [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_5} {S : Type u_7} [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_5} {S : Type u_7} [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_5} {S : Type u_7} [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_5} {S : Type u_7} [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).