Revision #2560 → #3168 · back to history
modifiedContinuous dual space (intro)33f0b69422c1
| Field | From #2560 | To #3168 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.LinearMap | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedAlgebraic dual space8f0f4355ddc9
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Algebraic dual space","snippet":"is defined as the set of all linear maps"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}(\\varphi +\\psi )(x)&=\\varphi (x)+\\psi (x)\\\\(a\\varphi )(x)&=a\\left(\\varphi (x)\\right)\\end{aligned}}}"}] | — |
modifiedA linear functional on R^281895c411ce7
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Algebraic dual space","snippet":"For example, if we express the vector space"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}(\\varphi +\\psi )(x)&=\\varphi (x)+\\psi (x)\\\\(a\\varphi )(x)&=a\\left(\\varphi (x)\\right)\\end{aligned}}}"}] | — |
modifiedDual basis (finite-dimensional)41735d4ff9d0
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Finite-dimensional case","snippet":"the dual basis is a set"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {e} ^{i}(c^{1}\\mathbf {e} _{1}+\\cdots +c^{n}\\mathbf {e} _{n})=c^{i},\\quad i=1,\\ldots ,n}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {e} ^{i}(\\mathbf {e} _{j})=\\delta _{j}^{i}}"}] | — |
modifiedBi-orthogonality property932adb08a507
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Finite-dimensional case","snippet":"is referred to as the bi-orthogonality property"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {e} ^{i}(c^{1}\\mathbf {e} _{1}+\\cdots +c^{n}\\mathbf {e} _{n})=c^{i},\\quad i=1,\\ldots ,n}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {e} ^{i}(\\mathbf {e} _{j})=\\delta _{j}^{i}}"}] | — |
modifiedVerifying a dual basis36dbb0166517
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Finite-dimensional case","snippet":"These are a basis of"},{"type":"math_alttext","value":"{\\displaystyle g(x)=g(\\alpha _{1}\\mathbf {e} _{1}+\\dots +\\alpha _{n}\\mathbf {e} _{n})=\\alpha _{1}g(\\mathbf {e} _{1})+\\dots +\\alpha _{n}g(\\mathbf {e} _{n})=\\mathbf {e} ^{1}(x)g(\\mathbf {e} _{1})+\\dots +\\mathbf {e} ^{n}(x)g(\\mathbf {e} _{n})}"}] | — |
modifiedDual basis of a non-orthogonal basis of R^26516474f1215
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Finite-dimensional case","snippet":"let its basis be chosen as"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}e^{11}&e^{12}\\\\e^{21}&e^{22}\\end{bmatrix}}{\\begin{bmatrix}e_{11}&e_{21}\\\\e_{12}&e_{22}\\end{bmatrix}}={\\begin{bmatrix}1&0\\\\0&1\\end{bmatrix}}.}"}] | — |
modifiedMatrix biorthogonality of basis and dual basisfc077aacb3f1
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Finite-dimensional case","snippet":"is a matrix whose columns are the basis vectors and"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {E}}^{\\textrm {T}}\\cdot E=I_{n},}"}] | — |
modifiedErdős–Kaplansky theoreme7ae04001119
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Infinite-dimensional case","snippet":"The exact dimension of the dual is given by the Erdős–Kaplansky theorem"},{"type":"math_alttext","value":"{\\displaystyle \\mathrm {dim} (V)=|A|<|F|^{|A|}=|V^{\\ast }|=\\mathrm {max} (|\\mathrm {dim} (V^{\\ast })|,|F|),}"}] | — |
modifiedTranspose of a linear map239ed389a53a
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Transpose of a linear map","snippet":"then the transpose (or dual )"},{"type":"math_alttext","value":"{\\displaystyle f^{*}(\\varphi )=\\varphi \\circ f\\,}"}] | — |
modifiedIdentity characterizing the transpose5386a7d60e33
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Transpose of a linear map","snippet":"This identity characterizes the transpose"},{"type":"math_alttext","value":"{\\displaystyle [f^{*}(\\varphi ),\\,v]=[\\varphi ,\\,f(v)],}"}] | — |
modifiedBasic annihilator properties0869f6a8436c
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Quotient spaces and annihilators","snippet":"The annihilator of a subset is itself a vector space."},{"type":"math_alttext","value":"{\\displaystyle \\{0\\}\\subseteq T^{0}\\subseteq S^{0}\\subseteq V^{*}.}"}] | — |
modifiedAnnihilators of subsets, sums and intersectionsee181e1a2559
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Quotient spaces and annihilators","snippet":"are two subsets of"},{"type":"math_alttext","value":"{\\displaystyle A^{0}+B^{0}\\subseteq (A\\cap B)^{0}.}"},{"type":"math_alttext","value":"{\\displaystyle \\left(\\bigcup _{i\\in I}A_{i}\\right)^{0}=\\bigcap _{i\\in I}A_{i}^{0}.}"},{"type":"math_alttext","value":"{\\displaystyle (A+B)^{0}=A^{0}\\cap B^{0}}"},{"type":"math_alttext","value":"{\\displaystyle (A\\cap B)^{0}=A^{0}+B^{0}.}"}] | — |
modifiedDouble annihilator and Galois connection (finite-dim)0454ae75fbe7
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Quotient spaces and annihilators","snippet":"forming the annihilator is a Galois connection on the lattice of subsets"},{"type":"math_alttext","value":"{\\displaystyle W^{00}=W}"}] | — |
modifiedContinuous dual space134d9935446c
| Field | From #2560 | To #3168 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.LinearMap | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedPolar topology on the continuous dualdd2526394bcb
| Field | From #2560 | To #3168 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.Dual | Mathlib.Analysis.LocallyConvex.Polar |
modifiedStrong topology2505a05f94e5
| Field | From #2560 | To #3168 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.LinearMap | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedStrong topology is normed for normed spaces798a0dc021a7
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Topologies on the dual","snippet":"is normed (in fact a Banach space if the field of scalars is complete)"},{"type":"math_alttext","value":"{\\displaystyle \\|\\varphi \\|=\\sup _{\\|x\\|\\leq 1}|\\varphi (x)|.}"}] | — |
modifiedDuals of quotient and subspace via annihilator560496a1e028
| Field | From #2560 | To #3168 |
|---|
| anchors | [{"section":"Annihilators","snippet":"Then, the dual of the quotient"},{"type":"math_alttext","value":"{\\displaystyle \\ker(j')=W^{\\perp }}"}] | — |
addedDouble dual spacef5862c895cc2
addedTranspose is an antihomomorphism of algebras4125652eae81
addedAnnihilator reverses inclusions840c89c902ad