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.

def Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : M →ₗ[R] Module.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.

Equations

• b.toDual = (b.constr ℕ) fun (v : ι) => (b.constr ℕ) fun (w : ι) => if w = v then 1 else 0

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

def 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.toDual_flip v is the linear map sending w to h.toDual w v.

Equations

• b.toDualFlip m = b.toDual.flip m

theorem 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 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 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 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 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 Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : LinearMap.ker b.toDual = ⊥

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

@[simp]

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

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

A vector space is linearly equivalent to its dual space.

Equations

• b.toDualEquiv = LinearEquiv.ofBijective b.toDual ⋯

@[simp]

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

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

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

Equations

• b.dualBasis = b.map b.toDualEquiv

theorem Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup 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 Basis.linearCombination_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup 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 Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) : (b.dualBasis.repr l) i = l (b i)

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

@[simp]

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

@[simp]

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

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

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

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

theorem Basis.dualBasis_coord_toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup 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 Basis.coord_toDualEquiv_symm_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (f : Module.Dual R M) : (b.coord i) (b.toDualEquiv.symm f) = (b.dualBasis.coord i) f

@[simp]

theorem Basis.linearCombination_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup 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.

Equations

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

def tacticUse_finite_instance : Lean.ParserDescr

Equations

• tacticUse_finite_instance = Lean.ParserDescr.node `tacticUse_finite_instance 1024 (Lean.ParserDescr.nonReservedSymbol "use_finite_instance" false)

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} : (∀ (i : ι), (ε i) m = 0) → m = 0
• finite (m : M) : {i : ι | (ε i) m ≠ 0}.Finite

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

The coefficients of v on the basis e

Equations

• h.coeffs m = { support := ⋯.toFinset, toFun := fun (i : ι) => (ε i) m, mem_support_toFun := ⋯ }

@[simp]

theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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

Equations

• Module.DualBases.lc e l = l.sum fun (i : ι) (a : R) => a • e i

theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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

def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup 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.

Equations

• h.basis = { repr := { toFun := h.coeffs, map_add' := ⋯, map_smul' := ⋯, invFun := Module.DualBases.lc e, left_inv := ⋯, right_inv := ⋯ } }

@[simp]

theorem Module.DualBases.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup 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} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Dual R M} (h : DualBases e ε) [DecidableEq ι] [Finite ι] : ⇑h.basis.dualBasis = ε