LinearMap.dualMap_injective_iff
theorem LinearMap.dualMap_injective_iff :
∀ {K : Type uK} [inst : Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f
The theorem `LinearMap.dualMap_injective_iff` states that for any field `K`, and for any two types `V₁` and `V₂` considered as modules over `K`, if `f` is a linear map from `V₁` to `V₂`, then the dual map of `f` is injective if and only if `f` is surjective. Here, a function is injective if for every pair of elements from `V₁`, if they are mapped to the same element in `V₂` by `f` then they must have been the same element to begin with. Conversely, `f` is surjective if for every element in `V₂`, there is some element in `V₁` that `f` maps to it.
More concisely: For any field `K` and modules `V₁`, `V₂` over `K`, a linear map `f` from `V₁` to `V₂` is injective if and only if its dual map is surjective.
|
Basis.total_coord
theorem Basis.total_coord :
∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι),
((Finsupp.total ι (Module.Dual R M) R b.coord) f) (b i) = f i
The theorem `Basis.total_coord` states that for any commutative ring `R`, an `R`-module `M`, and a finite type `ι`, if `b` is a basis of `M` over `R` and `f` is a linear combination of the basis vectors (expressed as a function from `ι` to `R`), then applying the mapping `Finsupp.total` (which interprets `f` as a linear combination of the elements in the basis `b` and evaluates this linear combination) to `f` and then evaluating this at basis vector `b i` is equal to the coefficient `f i`. In other words, `Finsupp.total` properly distributes the coefficients of the linear combination across the basis vectors.
More concisely: For any commutative ring R, R-module M, finite type ι, basis b of M over R, and function f : ι → R representing a linear combination of basis vectors, we have Finsupp.total f (b i) = fi for all i in ι.
|
Subspace.isCompl_dualAnnihilator
theorem Subspace.isCompl_dualAnnihilator :
∀ {K : Type uK} [inst : Field K] {V₁ : Type uV₁} [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
{W W' : Subspace K V₁}, IsCompl W W' → IsCompl (Submodule.dualAnnihilator W) (Submodule.dualAnnihilator W')
The theorem `Subspace.isCompl_dualAnnihilator` states that in the context of vector spaces, if two subspaces `W` and `W'` are complementary (i.e., their direct sum is the entire space and they intersect only at the zero vector, denoted as `IsCompl W W'`), then their dual annihilators (the sets of linear maps that send all vectors in `W` and `W'` respectively to zero) are also complementary. This means that the structure of direct sum decompositions is preserved under the operation of taking dual annihilators.
More concisely: If subspaces `W` and `W'` of a vector space are complementary, then their dual annihilators annihilate each other, i.e., the annihilator of `W'` is contained in the annihilator of `W` and vice versa.
|
LinearMap.dualMap_injective_of_surjective
theorem LinearMap.dualMap_injective_of_surjective :
∀ {R : Type u} [inst : CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [inst_1 : AddCommMonoid M₁]
[inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {f : M₁ →ₗ[R] M₂},
Function.Surjective ⇑f → Function.Injective ⇑f.dualMap
The theorem `LinearMap.dualMap_injective_of_surjective` states that for any commutative semiring `R` and modules `M₁` and `M₂` over `R`, if a linear map `f` from `M₁` to `M₂` is surjective, then the dual map of `f` is injective. Here, a function is surjective if for every element in the codomain (here `M₂`), there is an element in the domain (here `M₁`) which maps to it. Similarly, a function is injective if different elements in the domain (here the dual of `M₁`) always map to different elements in the codomain (here the dual of `M₂`). The dual map of a linear map `f : M₁ →ₗ[R] M₂` is defined on the duals of `M₂` and `M₁`, which are the spaces of all linear maps from `M₂` and `M₁` to `R`, respectively.
More concisely: If a linear map between R-modules is surjective, then its dual map is injective.
|
Basis.linearEquiv_dual_iff_finiteDimensional
theorem Basis.linearEquiv_dual_iff_finiteDimensional :
∀ {K : Type uK} {V : Type uV} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V
This theorem states that for any vector space `V` over a field `K`, there exists an isomorphism between the vector space and its dual space (which is the space of linear maps from `V` to `K`), if and only if `V` is finite-dimensional. This is a consequence of the Erdős-Kaplansky theorem in linear algebra.
More concisely: A finite-dimensional vector space over a field is isomorphic to its dual space.
|
LinearMap.dualMap_surjective_iff
theorem LinearMap.dualMap_surjective_iff :
∀ {K : Type uK} [inst : Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f
The theorem `LinearMap.dualMap_surjective_iff` states that in the context of vector spaces, the dual map of a linear function `f` is surjective if and only if `f` itself is injective. Here, `f` is a linear map between two vector spaces `V₁` and `V₂` over a field `K`. Surjectivity of the dual map of `f` means that for every element in the dual space of `V₂`, there exists an element in the dual space of `V₁` such that the dual map of `f` applied on this element equals the given element in the dual space of `V₂`. Injectivity of `f` means that if `f` applied on two different elements of `V₁` yields the same result in `V₂`, then those two elements must be the same.
More concisely: The linear map `f` between vector spaces `V₁` and `V₂` over a field `K` has a surjective dual if and only if `f` is injective.
|
Module.DualBases.lc_coeffs
theorem Module.DualBases.lc_coeffs :
∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{e : ι → M} {ε : ι → Module.Dual R M} [inst_3 : DecidableEq ι] (h : Module.DualBases e ε) (m : M),
Module.DualBases.lc e (h.coeffs m) = m
This theorem, named `Module.DualBases.lc_coeffs`, states that for any element `m` of a module `M` over a commutative ring `R`, there exists a linear combination of a set of basis vectors `e` indexed by `ι`, such that the coefficients of this linear combination are determined by a dual basis `ε`, i.e., a set of linear maps from `M` to `R`. This theorem asserts that the linear combination of basis vectors `e` weighted by the coefficients `(ε p m)` is equal to the module element `m`. This is true if `e` and `ε` form a pair of dual bases, and the equality is decidable for all indices in `ι`.
More concisely: For any module element `m` over a commutative ring and any dual basis `(ε\_i)` of a basis `(e\_i)` of the module, there exists coefficients `(c\_i)` in the ring such that `m = ∑_(i ∈ I) c\_i * e\_i`, where the coefficients are determined by `c\_i = ε\_i(m)`.
|
Submodule.dualRestrict_ker_eq_dualAnnihilator
theorem Submodule.dualRestrict_ker_eq_dualAnnihilator :
∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(W : Submodule R M), LinearMap.ker W.dualRestrict = W.dualAnnihilator
This theorem states that the kernel of the dual restriction map from the dual space of a module `V` to the dual space of a submodule `W` is equal to the dual annihilator of `W`. In this context, `R` is a commutative semiring, `M` is an additive commutative monoid, and `M` further becomes a module over `R`. The submodule `W` is a subset of `M`. This is essentially the definition of the dual annihilator of the submodule `W`.
More concisely: The kernel of the restriction map from the dual space of an `R`-module `V` to the dual space of a submodule `W` equals the annihilator of `W` in `V^dual`.
|
Submodule.range_dualMap_mkQ_eq
theorem Submodule.range_dualMap_mkQ_eq :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(W : Submodule R M), LinearMap.range W.mkQ.dualMap = W.dualAnnihilator
This theorem states that for any given commutative ring `R` and an abelian group `M` that is also an `R`-module, and any submodule `W` of `M`, the range of the dual map of the quotient map `W.mkQ` (which maps from the dual of the quotient module `(V/W)^*` to the dual of `V`, `V^*`) is equal to the dual annihilator of `W`. Here, the dual annihilator of a submodule is the set of linear functionals that vanish on that submodule.
More concisely: The dual map of the quotient of an `R`-module `M` by a submodule `W` equals the restriction of the dual annihilator of `W` to the dual of `M`.
|
Submodule.dualAnnihilator_gc
theorem Submodule.dualAnnihilator_gc :
∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
GaloisConnection (⇑OrderDual.toDual ∘ Submodule.dualAnnihilator)
(Submodule.dualCoannihilator ∘ ⇑OrderDual.ofDual)
The theorem `Submodule.dualAnnihilator_gc` establishes a Galois connection between the dual annihilator of a submodule and the coannihilator of a submodule of the dual space in the context of a commutative semiring and an additive commutative monoid. More specifically, for any ring `R` and module `M` equipped with a commutative semiring structure and an additive commutative monoid structure, respectively, the dual function of the dual annihilator of a submodule and the coannihilator of a submodule of the dual space form a Galois connection. This means that for all submodules `a` and `b`, `a` is less than or equal to the coannihilator of the dual of `b` if and only if the dual of the dual annihilator of `a` is less than or equal to `b`.
More concisely: The dual annihilator and coannihilator of submodules in the context of a commutative semiring and an additive commutative monoid form a Galois connection.
|
Submodule.sup_dualAnnihilator_le_inf
theorem Submodule.sup_dualAnnihilator_le_inf :
∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(U V : Submodule R M), U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator
This theorem states that for any two submodules `U` and `V` of a module `M` over a commutative semiring `R`, the sup (or join) of the dual annihilators of `U` and `V` is less than or equal to the dual annihilator of the intersection of `U` and `V`. In other words, combining the sets of all forms that annihilate `U` and `V` respectively gives a set that is a subset of all forms that annihilate both `U` and `V` at the same time.
The "dual annihilator" of a submodule is a concept from the dual space theory in Linear Algebra, it consists of all the linear functionals that send every vector in the submodule to zero.
More concisely: For any commutative semiring R and modules M, M\* (the dual space of M), the annihilator of U ∩ V is contained in the annihilator of U ⊕ V (where U, V are submodules of M) in the dual space M\*.
|
LinearMap.dualMap_bijective_iff
theorem LinearMap.dualMap_bijective_iff :
∀ {K : Type uK} [inst : Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f
The theorem `LinearMap.dualMap_bijective_iff` states that for any field `K` and any vector spaces `V₁` and `V₂` over `K` with the addition of commutative groups, and for any linear map `f` from `V₁` to `V₂`, the dual map of `f` is bijective (i.e., both injective and surjective) if and only if `f` itself is bijective.
More concisely: For any field K and vector spaces V₁ and V₂ over K, a linear map f from V₁ to V₂ is bijective if and only if its dual map is bijective.
|
Submodule.iSup_dualAnnihilator_le_iInf
theorem Submodule.iSup_dualAnnihilator_le_iInf :
∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_1}
(U : ι → Submodule R M), ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator
This theorem expresses a property of submodules in the context of module theory. Given an indexed family `(U : ι → Submodule R M)` of submodules of a module `M` over a commutative semiring `R`, the theorem states that the supremum (join) of the dual annihilators of each submodule `U i` is less than or equal to the dual annihilator of the infimum (meet) of all the submodules `U i`. Here, the dual annihilator of a submodule is the set of linear functionals that vanish on that submodule.
More concisely: For every indexed family of submodules `(U : ι → Submodule R M)` of a module `M` over a commutative semiring `R`, the dual annihilator of the infimum of the `U i`'s contains the supremum of the dual annihilators of the `U i`'s.
|
Module.eval_ker
theorem Module.eval_ker :
∀ (K : Type uK) (V : Type uV) [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : Module.Free K V], LinearMap.ker (Module.Dual.eval K V) = ⊥
This theorem states that for any commutative ring `K` and any module `V` over `K` that is free, the kernel of the evaluation linear map, which maps the module `V` to the dual of the dual of `V`, is trivial (i.e., it consists only of the zero vector). This means that the evaluation map is injective, or equivalently, it does not map any non-zero vector in `V` to the zero vector in the dual of the dual of `V`. Hence, in the context of module theory, this theorem is asserting the reflexivity of finite-dimensional vector spaces.
More concisely: For any commutative ring `K` and free `K`-module `V`, the evaluation map from `V` to `(V^*)^*` is injective.
|
Mathlib.LinearAlgebra.Dual._auxLemma.11
theorem Mathlib.LinearAlgebra.Dual._auxLemma.11 :
∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{W : Submodule R M} (φ : Module.Dual R M), (φ ∈ W.dualAnnihilator) = ∀ w ∈ W, φ w = 0
This theorem states that for any commutative semiring `R`, any additive commutative monoid `M` serving as an `R`-module, and any submodule `W` of `M`, a linear map `φ` from `M` to `R` (identified as a member of the dual space of `M`) is in the dual annihilator of `W` if and only if it maps every element of `W` to zero. In simpler terms, it states that a linear map is in the dual annihilator of a submodule when it annihilates every element of that submodule.
More concisely: A linear map from an `R`-module to `R` belongs to the dual annihilator of a submodule if and only if it maps every submodule element to zero.
|
Module.IsReflexive.bijective_dual_eval'
theorem Module.IsReflexive.bijective_dual_eval' :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[self : Module.IsReflexive R M], Function.Bijective ⇑(Module.Dual.eval R M)
This theorem states that for any commutative ring 'R' and additive commutative group 'M' which forms a module over 'R', if the module 'M' is reflexive, then the natural map from 'M' to its double dual (obtained through the `Module.Dual.eval` function) is a bijection. A module is deemed reflexive if it is isomorphic to its double dual. A bijection, defined by `Function.Bijective`, is a function that is both injective (every element of the input maps to a unique element of the output) and surjective (every element of the output has a preimage in the input).
More concisely: If a commutative 'R'-module M is reflexive, then the natural map from M to its double dual is a bijection.
|