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.

source

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.

Equations

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

Instances For

source

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

source

@[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

source

@[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

source

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

source

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

source

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

source

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.

Equations

b.toDualFlip m = b.toDual.flip m

Instances For

source

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₁

source

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

source

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

source

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

source

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

source

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

LinearMap.ker b.toDual = ⊥

source

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 ι] :

LinearMap.range b.toDual = ⊤

source

@[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

source

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.

Equations

b.toDualEquiv = LinearEquiv.ofBijective b.toDual ⋯

Instances For

source

@[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

source

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.

Equations

b.dualBasis = b.map b.toDualEquiv

Instances For

source

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

source

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

source

@[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)

source

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

source

@[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

source

@[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

source

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)

source

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)

source

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

LinearMap.ker (Dual.eval R M) = ⊥

source

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

LinearMap.range (Dual.eval R M) = ⊤

source

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

source

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

source

@[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

source

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.

Instances For

source

def tacticUse_finite_instance :

Lean.ParserDescr

Equations

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

Instances For

source

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

Instances For

source

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

Equations

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

Instances For

source

@[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

source

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

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

Instances For

source

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

source

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

source

@[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

source

@[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

source

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.

Equations

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

Instances For

source

@[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

source

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

source

@[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

source

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

source

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 = ε

Documentation

Mathlib.LinearAlgebra.Dual.Basis

Bases of dual vector spaces #

Main definitions #

Main results #