nonzero_span_atom
theorem nonzero_span_atom :
∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
v ≠ 0 → IsAtom (Submodule.span K {v})
This theorem states that for a module over a division ring, the span of a non-zero element is an atom of the lattice of submodules. In other words, for any non-zero element `v` in a module `V` over a division ring `K`, the smallest submodule of `V` that contains `v` (i.e., its span) is an "atom". Here, an "atom" refers to a submodule with no other submodules between it and the zero submodule, and it itself is not the zero submodule. This means that there are no submodules strictly between the span of `v` and the zero submodule in the lattice of submodules of `V`.
More concisely: For a non-zero element in a module over a division ring, its span is an atom in the lattice of submodules.
|
atom_iff_nonzero_span
theorem atom_iff_nonzero_span :
∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(W : Submodule K V), IsAtom W ↔ ∃ v, v ≠ 0 ∧ W = Submodule.span K {v}
This theorem states that, for a given module `V` over a division ring `K`, a submodule `W` of `V` is an atom if and only if there exists a non-zero element `v` from `V` such that `W` is exactly the span of `{v}`. Here, an "atom" is defined as a submodule with no other submodules between it and `⊥` (the zero submodule), and not being `⊥` itself. In other words, an atomic submodule in this context is a submodule generated by a single non-zero element.
More concisely: A submodule `W` of a module `V` over a division ring is an atom if and only if it is generated by a single non-zero element.
|
Submodule.exists_le_ker_of_lt_top
theorem Submodule.exists_le_ker_of_lt_top :
∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
∀ p < ⊤, ∃ f, f ≠ 0 ∧ p ≤ LinearMap.ker f
The theorem `Submodule.exists_le_ker_of_lt_top` states that for any DivisionRing `K`, Additive Commutative Group `V`, and `V` being a `K`-Module, if `p` is a subspace of the vector space `V` such that `p` is strictly less than the top element (`⊤`, which usually represents the entire space), then there exists a non-zero linear map `f` from `V` to `K` such that `p` is a subset of the kernel of `f`. The kernel of a linear map are all the vectors that are mapped to the zero vector.
More concisely: If `p` is a proper subspace of a `K`-Module `V` over a division ring `K`, then there exists a non-zero linear map `f` from `V` to `K` such that `p` is contained in the kernel of `f`.
|
LinearMap.exists_extend
theorem LinearMap.exists_extend :
∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {p : Submodule K V} (f : ↥p →ₗ[K] V'),
∃ g, g ∘ₗ p.subtype = f
This theorem states that for any linear map `f`, which is defined on a subspace `p` and maps to a vector space `V'` over a division ring `K`, there exists another linear map `g` which extends `f` to the whole space `V`. In other words, `g` is such that when it is composed with the inclusion of the subspace `p` into `V`, it equals the original map `f`. This theorem thus guarantees the existence of extensions of linear maps defined on subspaces to the entire vector space.
More concisely: Given a linear map `f` on a subspace `p` of a vector space `V` over a division ring `K`, there exists a linear extension `g` of `f` to all of `V`.
|