SeparatingDual.exists_ne_zero'
theorem SeparatingDual.exists_ne_zero' :
∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
[inst_3 : TopologicalSpace R] [inst_4 : Module R V] [self : SeparatingDual R V] (x : V), x ≠ 0 → ∃ f, f x ≠ 0
This theorem states that for any nonzero vector in a topological vector space over some ring, there exists a continuous linear map (element of the algebraic dual) that maps this vector to a nonzero scalar value in the ring. This theorem can be applied to any ring and any topological vector space over this ring. This theorem is significant because it assures that we can always find a continuous linear functional that distinguishes nonzero vectors from the zero vector.
More concisely: For any nonzero vector in a topological vector space over a ring, there exists a continuous linear functional mapping the vector to a nonzero scalar in the ring.
|
SeparatingDual.exists_continuousLinearEquiv_apply_eq
theorem SeparatingDual.exists_continuousLinearEquiv_apply_eq :
∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
[inst_3 : TopologicalSpace V] [inst_4 : TopologicalRing R] [inst_5 : TopologicalAddGroup V] [inst_6 : Module R V]
[inst_7 : SeparatingDual R V] [inst_8 : ContinuousSMul R V] {x y : V}, x ≠ 0 → y ≠ 0 → ∃ A, A x = y
This theorem states that in a topological vector space with a separating dual, the group of continuous linear equivalences acts transitively on the set of non-zero vectors. In other words, for any non-zero vectors `x` and `y` in this space, there exists a continuous linear equivalence `A : V ≃L[R] V` such that `A x = y`.
More concisely: In a topological vector space with a separating dual, for any non-zero vectors `x` and `y`, there exists a continuous linear equivalence mapping `x` to `y`.
|
SeparatingDual.dualMap_surjective_iff
theorem SeparatingDual.dualMap_surjective_iff :
∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
[inst_3 : TopologicalSpace V] [inst_4 : TopologicalRing R] [inst_5 : Module R V] [inst_6 : SeparatingDual R V]
{W : Type u_3} [inst_7 : AddCommGroup W] [inst_8 : Module R W] [inst_9 : FiniteDimensional R W] {f : W →ₗ[R] V},
Function.Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap) ↔ Function.Injective ⇑f
The theorem `SeparatingDual.dualMap_surjective_iff` asserts that for a given finite-dimensional subspace `W` of a space `V` that has a separating dual, any linear functional (represented by `f : W →ₗ[R] V`) on `W` can be extended to a continuous linear functional on `V`. This statement is expressed more generally for an injective linear map from `W` to `V`. The theorem further states that the composition of the dual map (`f.dualMap`) and the conversion of a continuous linear map to a linear map (`ContinuousLinearMap.toLinearMap`) is surjective if and only if the original linear functional `f` is injective.
In mathematical terms, this theorem is saying that the injectivity of a linear functional on a finite-dimensional subspace of a vector space with a separating dual is equivalent to the surjectivity of the dual map composed with the conversion function from a continuous linear map to a linear map. This theorem is useful in the study of dual spaces in functional analysis and linear algebra.
More concisely: For a finite-dimensional subspace W of a vector space V with separating dual, the linear functional f : W → V is injective if and only if the composition of its dual map with the conversion function from continuous linear maps to linear maps is surjective.
|