Projection to a subspace #
In this file we define
linear_proj_of_is_compl (p q : submodule R E) (h : is_compl p q)
: the projection of a moduleE
to a submodulep
along its complementq
; it is the unique linear mapf : E → p
such thatf x = x
forx ∈ p
andf x = 0
forx ∈ q
.is_compl_equiv_proj p
: equivalence between submodulesq
such thatis_compl p q
and projectionsf : E → p
,∀ x ∈ p, f x = x
.
We also provide some lemmas justifying correctness of our definitions.
Tags #
projection, complement subspace
If q
is a complement of p
, then M/p ≃ q
.
Equations
- p.quotient_equiv_of_is_compl q h = (linear_equiv.of_bijective (p.mkq.comp q.subtype) _ _).symm
If q
is a complement of p
, then p × q
is isomorphic to E
. It is the unique
linear map f : E → p
such that f x = x
for x ∈ p
and f x = 0
for x ∈ q
.
Equations
- p.prod_equiv_of_is_compl q h = linear_equiv.of_bijective (p.subtype.coprod q.subtype) _ _
Projection to a submodule along its complement.
Equations
- p.linear_proj_of_is_compl q h = (linear_map.fst R ↥p ↥q).comp ↑((p.prod_equiv_of_is_compl q h).symm)
Given linear maps φ
and ψ
from complement submodules, of_is_compl
is
the induced linear map over the entire module.
Equations
- linear_map.of_is_compl h φ ψ = (φ.coprod ψ).comp ↑((p.prod_equiv_of_is_compl q h).symm)
The linear map from (p →ₗ[R₁] F) × (q →ₗ[R₁] F)
to E →ₗ[R₁] F
.
The natural linear equivalence between (p →ₗ[R₁] F) × (q →ₗ[R₁] F)
and E →ₗ[R₁] F
.
Equations
- linear_map.of_is_compl_prod_equiv h = {to_fun := (linear_map.of_is_compl_prod h).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (φ : E →ₗ[R₁] F), (φ.dom_restrict p, φ.dom_restrict q), left_inv := _, right_inv := _}
If f : E →ₗ[R] F
and g : E →ₗ[R] G
are two surjective linear maps and
their kernels are complement of each other, then x ↦ (f x, g x)
defines
a linear equivalence E ≃ₗ[R] F × G
.
Equations
- f.equiv_prod_of_surjective_of_is_compl g hf hg hfg = linear_equiv.of_bijective (f.prod g) _ _
Equivalence between submodules q
such that is_compl p q
and linear maps f : E →ₗ[R] p
such that ∀ x : p, f x = x
.
A linear endomorphism of a module E
is a projection onto a submodule p
if it sends every element
of E
to p
and fixes every element of p
.
The definition allow more generally any fun_like
type and not just linear maps, so that it can be
used for example with continuous_linear_map
or matrix
.
Restriction of the codomain of a projection of onto a subspace p
to p
instead of the whole
space.
Equations
- h.cod_restrict = linear_map.cod_restrict m f _