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 mapM →ₗ[R] Dual R M
associated to a basis for anR
-moduleM
.Basis.toDual_equiv
is the equivalenceM ≃ₗ[R] Dual R M
associated to a finite basis.Basis.dualBasis
is a basis forDual R M
given a finite basis forM
.Module.DualBases e ε
is the proposition that the familiese
of vectors andε
of dual vectors have the characteristic properties of a basis and a dual.
Main results #
- Bases:
Module.DualBases.basis
andModule.DualBases.coe_basis
: ife
andε
form a dual pair, thene
is a basis.Module.DualBases.coe_dualBasis
: ife
andε
form a dual pair, thenε
is a basis.
The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.
Instances For
h.toDual_flip v
is the linear map sending w
to h.toDual w v
.
Equations
- b.toDualFlip m = b.toDual.flip m
Instances For
A vector space is linearly equivalent to its dual space.
Equations
Instances For
Maps a basis for V
to a basis for the dual space.
Equations
- b.dualBasis = b.map b.toDualEquiv
Instances For
simp
normal form version of linearCombination_dualBasis
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
Equations
- tacticUse_finite_instance = Lean.ParserDescr.node `tacticUse_finite_instance 1024 (Lean.ParserDescr.nonReservedSymbol "use_finite_instance" false)
Instances For
e
and ε
have characteristic properties of a basis and its dual
Instances For
The coefficients of v
on the basis e
Equations
Instances For
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
(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 := ⋯ } }