Submodule.linearProjOfIsCompl_apply_left
theorem Submodule.linearProjOfIsCompl_apply_left :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{p q : Submodule R E} (h : IsCompl p q) (x : ↥p), (p.linearProjOfIsCompl q h) ↑x = x
The theorem `Submodule.linearProjOfIsCompl_apply_left` states that for any ring `R`, any additive commutative group `E` which is also a module over `R`, and two submodules `p` and `q` of `E` that are complementary (i.e., their sum is the whole module and their intersection is the trivial submodule), if we apply the linear projection associated with `p` and `q` to an element `x` in `p`, we get `x` back. This is essentially saying that the projection of an element onto the submodule it already resides in leaves the element unchanged.
More concisely: For any ring `R`, module `E` over `R`, and complementary submodules `p` and `q` of `E`, the linear projection of any element `x` in `p` onto `p` along `q` equals `x`.
|
LinearMap.isCompl_of_proj
theorem LinearMap.isCompl_of_proj :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
{f : E →ₗ[R] ↥p}, (∀ (x : ↥p), f ↑x = x) → IsCompl p (LinearMap.ker f)
The theorem `LinearMap.isCompl_of_proj` states that for any given ring `R`, an additive commutative group `E`, and a module `E` over `R`, if `p` is a submodule of `E` and `f` is a linear map from `E` to `p`, then for all elements `x` in `p`, if the linear map applied to `x` is `x` itself, then `p` and the kernel of `f` are complementary in `E`. In other words, any `E` can be "uniquely" decomposed into an element in `p` and an element in the kernel of `f`. This theorem is a fundamental result in linear algebra related to projection operators.
More concisely: If `f` is a linear map from a module `E` over a ring `R` to a submodule `p` of `E`, such that `x ∈ p` implies `f(x) = x`, then `p` and the kernel of `f` have a complement in `E`.
|