Bases of dual vector spaces

The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to R$. This file concerns bases on dual vector spaces.

Main definitions

• Bases:
  • Basis.toDual produces the map M →ₗ[R] Dual R M associated to a basis for an R-module M.
  • Basis.toDualEquiv is the equivalence M ≃ₗ[R] Dual R M associated to a finite basis.
  • Basis.dualBasis is a basis for Dual R M given a finite basis for M.
  • Module.DualBases e ε is the proposition that the families e of vectors and ε of dual vectors have the characteristic properties of a basis and a dual.

Main results

• Bases:
  • Module.DualBases.basis and Module.DualBases.coe_basis: if e and ε form a dual pair, then e is a basis.
  • Module.DualBases.coe_dualBasis: if e and ε form a dual pair, then ε is a basis.

noncomputable def Module.Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : M →ₗ[R] Dual R M

The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.

theorem Module.Basis.toDual_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i j : ι) : (b.toDual (b i)) (b j) = if i = j then 1 else 0

@[simp]

theorem Module.Basis.toDual_linearCombination_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : (b.toDual ((Finsupp.linearCombination R ⇑b) f)) (b i) = f i

@[simp]

theorem Module.Basis.toDual_linearCombination_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = f i

theorem Module.Basis.toDual_apply_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) : (b.toDual m) (b i) = (b.repr m) i

theorem Module.Basis.toDual_apply_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (m : M) : (b.toDual (b i)) m = (b.repr m) i

theorem Module.Basis.coe_toDual_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) : b.toDual (b i) = b.coord i

noncomputable def Module.Basis.toDualFlip {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) : M →ₗ[R] R

h.toDualFlip v is the linear map sending w to h.toDual w v.

theorem Module.Basis.toDualFlip_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m₁ m₂ : M) : (b.toDualFlip m₁) m₂ = (b.toDual m₂) m₁

theorem Module.Basis.toDual_eq_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) : (b.toDual m) (b i) = (b.repr m) i

theorem Module.Basis.toDual_eq_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) (i : ι) : (b.toDual m) (b i) = b.equivFun m i

theorem Module.Basis.toDual_injective {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : Function.Injective ⇑b.toDual

theorem Module.Basis.toDual_inj {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (a : b.toDual m = 0) : m = 0

theorem Module.Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : b.toDual.ker = ⊥

theorem Module.Basis.toDual_range {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : b.toDual.range = ⊤

@[simp]

theorem Module.Basis.sum_dual_apply_smul_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] (f : Dual R M) : ∑ x : ι, f (b x) • b.coord x = f

noncomputable def Module.Basis.toDualEquiv {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : M ≃ₗ[R] Dual R M

A vector space is linearly equivalent to its dual space.

@[simp]

theorem Module.Basis.toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) : b.toDualEquiv m = b.toDual m

noncomputable def Module.Basis.dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : Basis ι R (Dual R M)

Maps a basis for V to a basis for the dual space.

theorem Module.Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i j : ι) : (b.dualBasis i) (b j) = if j = i then 1 else 0

theorem Module.Basis.linearCombination_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (f : ι →₀ R) (i : ι) : ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

@[simp]

theorem Module.Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Dual R M) (i : ι) : (b.dualBasis.repr l) i = l (b i)

theorem Module.Basis.dualBasis_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (m : M) : (b.dualBasis i) m = (b.repr m) i

@[simp]

theorem Module.Basis.coe_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : ⇑b.dualBasis = b.coord

@[simp]

theorem Module.Basis.toDual_toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

theorem Module.Basis.dualBasis_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Dual R M) (i : ι) : b.dualBasis.equivFun l i = l (b i)

theorem Module.Basis.eval_injective {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} (b : Basis ι R M) : Function.Injective ⇑(Dual.eval R M)

theorem Module.Basis.eval_ker {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} (b : Basis ι R M) : (Dual.eval R M).ker = ⊥

theorem Module.Basis.eval_range {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) : (Dual.eval R M).range = ⊤

theorem Module.Basis.dualBasis_coord_toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (f : M) : (b.dualBasis.coord i) (b.toDualEquiv f) = (b.coord i) f

theorem Module.Basis.coord_toDualEquiv_symm_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (f : Dual R M) : (b.coord i) (b.toDualEquiv.symm f) = (b.dualBasis.coord i) f

@[simp]

theorem Module.Basis.linearCombination_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : ((Finsupp.linearCombination R b.coord) f) (b i) = f i

simp normal form version of linearCombination_dualBasis

def evalUseFiniteInstance : Lean.Elab.Tactic.TacticM Unit

Try using Set.toFinite to dispatch a Set.Finite goal.

def tacticUse_finite_instance : Lean.ParserDescr

Try using Set.toFinite to dispatch a Set.Finite goal.

structure Module.DualBases {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : ι → M) (ε : ι → Dual R M) : Prop

e and ε have characteristic properties of a basis and its dual

• eval_same (i : ι) : (ε i) (e i) = 1
• eval_of_ne : Pairwise fun (i j : ι) => (ε i) (e j) = 0
• total {m₁ m₂ : M} : (∀ (i : ι), (ε i) m₁ = (ε i) m₂) → m₁ = m₂
• finite (m : M) : {i : ι | (ε i) m ≠ 0}.Finite

noncomputable def Module.DualBases.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (m : M) : ι →₀ R

The coefficients of v on the basis e

@[simp]

theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (m : M) (i : ι) : (h.coeffs m) i = (ε i) m

def Module.DualBases.lc {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (e : ι → M) (l : ι →₀ R) : M

linear combinations of elements of e. This is a convenient abbreviation for Finsupp.linearCombination R e l

theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : ι → M) (l : ι →₀ R) : lc e l = (Finsupp.linearCombination R e) l

theorem Module.DualBases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (l : ι →₀ R) (i : ι) : (ε i) (lc e l) = l i

@[simp]

theorem Module.DualBases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (l : ι →₀ R) : h.coeffs (lc e l) = l

@[simp]

theorem Module.DualBases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (m : M) : lc e (h.coeffs m) = m

For any m : M n, $\sum_{p ∈ Q n} (ε p m) • e p = m$

noncomputable def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) : Basis ι R M

(h : DualBases e ε).basis shows the family of vectors e forms a basis.

@[simp]

theorem Module.DualBases.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (m : M) : h.basis.repr m = h.coeffs m

theorem Module.DualBases.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) (l : ι →₀ R) : h.basis.repr.symm l = lc e l

@[simp]

theorem Module.DualBases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) : ⇑h.basis = e

theorem Module.DualBases.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) {H : Set ι} {x : M} (hmem : x ∈ Submodule.span R (e '' H)) (i : ι) : (ε i) x ≠ 0 → i ∈ H

theorem Module.DualBases.coe_dualBasis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) [DecidableEq ι] [Finite ι] : ⇑h.basis.dualBasis = ε