# mathlib3documentation

linear_algebra.projection

# Projection to a subspace #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

• linear_proj_of_is_compl (p q : submodule R E) (h : is_compl p q): the projection of a module E to a submodule p along its complement q; it is the unique linear map f : E → p such that f x = x for x ∈ p and f x = 0 for x ∈ q.
• is_compl_equiv_proj p: equivalence between submodules q such that is_compl p q and projections f : E → p, ∀ x ∈ p, f x = x.

We also provide some lemmas justifying correctness of our definitions.

## Tags #

projection, complement subspace

theorem linear_map.ker_id_sub_eq_of_proj {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] p} (hf : (x : p), f x = x) :
= p
theorem linear_map.range_eq_of_proj {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] p} (hf : (x : p), f x = x) :
theorem linear_map.is_compl_of_proj {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] p} (hf : (x : p), f x = x) :
noncomputable def submodule.quotient_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) :
(E p) ≃ₗ[R] q

If q is a complement of p, then M/p ≃ q.

Equations
@[simp]
theorem submodule.quotient_equiv_of_is_compl_symm_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : q) :
h).symm) x =
@[simp]
theorem submodule.quotient_equiv_of_is_compl_apply_mk_coe {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : q) :
= x
@[simp]
theorem submodule.mk_quotient_equiv_of_is_compl_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : E p) :
= x
noncomputable def submodule.prod_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) :

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
@[simp]
theorem submodule.coe_prod_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) :
@[simp]
theorem submodule.coe_prod_equiv_of_is_compl' {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : p × q) :
h) x = (x.fst) + (x.snd)
@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_left {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : p) :
h).symm) x = (x, 0)
@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_right {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) (x : q) :
h).symm) x = (0, x)
@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_fst_eq_zero {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) {x : E} :
( h).symm) x).fst = 0 x q
@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_snd_eq_zero {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) {x : E} :
( h).symm) x).snd = 0 x p
@[simp]
theorem submodule.prod_comm_trans_prod_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) :
p).trans h) =
noncomputable def submodule.linear_proj_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] (p q : E) (h : q) :

Projection to a submodule along its complement.

Equations
@[simp]
theorem submodule.linear_proj_of_is_compl_apply_left {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) (x : p) :
h) x = x
@[simp]
theorem submodule.linear_proj_of_is_compl_range {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) :
@[simp]
theorem submodule.linear_proj_of_is_compl_apply_eq_zero_iff {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) {x : E} :
h) x = 0 x q
theorem submodule.linear_proj_of_is_compl_apply_right' {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) (x : E) (hx : x q) :
h) x = 0
@[simp]
theorem submodule.linear_proj_of_is_compl_apply_right {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) (x : q) :
h) x = 0
@[simp]
theorem submodule.linear_proj_of_is_compl_ker {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) :
= q
theorem submodule.linear_proj_of_is_compl_comp_subtype {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) :
theorem submodule.linear_proj_of_is_compl_idempotent {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (h : q) (x : E) :
h) ( h) x) = h) x
theorem submodule.exists_unique_add_of_is_compl_prod {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (hc : q) (x : E) :
∃! (u : p × q), (u.fst) + (u.snd) = x
theorem submodule.exists_unique_add_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (hc : q) (x : E) :
(u : p) (v : q), u + v = x (r : p) (s : q), r + s = x r = u s = v
theorem submodule.linear_proj_add_linear_proj_of_is_compl_eq_self {R : Type u_1} [ring R] {E : Type u_2} [ E] {p q : E} (hpq : q) (x : E) :
( hpq) x) + ( _) x) = x
noncomputable def linear_map.of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) (φ : p →ₗ[R] F) (ψ : q →ₗ[R] F) :

Given linear maps φ and ψ from complement submodules, of_is_compl is the induced linear map over the entire module.

Equations
@[simp]
theorem linear_map.of_is_compl_left_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
ψ) u = φ u
@[simp]
theorem linear_map.of_is_compl_right_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) :
ψ) v = ψ v
theorem linear_map.of_is_compl_eq {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : (u : p), φ u = χ u) (hψ : (u : q), ψ u = χ u) :
= χ
theorem linear_map.of_is_compl_eq' {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = χ.comp p.subtype) (hψ : ψ = χ.comp q.subtype) :
= χ
@[simp]
theorem linear_map.of_is_compl_zero {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) :
= 0
@[simp]
theorem linear_map.of_is_compl_add {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ₁ φ₂ : p →ₗ[R] F} {ψ₁ ψ₂ : q →ₗ[R] F} :
(φ₁ + φ₂) (ψ₁ + ψ₂) = ψ₁ + ψ₂
@[simp]
theorem linear_map.of_is_compl_smul {R : Type u_1} [comm_ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {p q : E} (h : q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (c : R) :
(c φ) (c ψ) = c
noncomputable def linear_map.of_is_compl_prod {E : Type u_2} {F : Type u_3} {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : E} (h : q) :
(p →ₗ[R₁] F) × (q →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F

The linear map from (p →ₗ[R₁] F) × (q →ₗ[R₁] F) to E →ₗ[R₁] F.

Equations
@[simp]
theorem linear_map.of_is_compl_prod_apply {E : Type u_2} {F : Type u_3} {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : E} (h : q) (φ : (p →ₗ[R₁] F) × (q →ₗ[R₁] F)) :
noncomputable def linear_map.of_is_compl_prod_equiv {E : Type u_2} {F : Type u_3} {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : E} (h : q) :
((p →ₗ[R₁] F) × (q →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F

The natural linear equivalence between (p →ₗ[R₁] F) × (q →ₗ[R₁] F) and E →ₗ[R₁] F.

Equations
@[simp]
theorem linear_map.linear_proj_of_is_compl_of_proj {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} (f : E →ₗ[R] p) (hf : (x : p), f x = x) :
= f
noncomputable def linear_map.equiv_prod_of_surjective_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →ₗ[R] F) (g : E →ₗ[R] G) (hf : = ) (hg : = ) (hfg : ) :
E ≃ₗ[R] F × G

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
• hg hfg = _
@[simp]
theorem linear_map.coe_equiv_prod_of_surjective_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : = ) (hg : = ) (hfg : ) :
hg hfg) = f.prod g
@[simp]
theorem linear_map.equiv_prod_of_surjective_of_is_compl_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : = ) (hg : = ) (hfg : ) (x : E) :
hg hfg) x = (f x, g x)
noncomputable def submodule.is_compl_equiv_proj {R : Type u_1} [ring R] {E : Type u_2} [ E] (p : E) :
{q // q} {f // (x : p), f x = x}

Equivalence between submodules q such that is_compl p q and linear maps f : E →ₗ[R] p such that ∀ x : p, f x = x.

Equations
@[simp]
theorem submodule.coe_is_compl_equiv_proj_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] (p : E) (q : {q // q}) :
@[simp]
theorem submodule.coe_is_compl_equiv_proj_symm_apply {R : Type u_1} [ring R] {E : Type u_2} [ E] (p : E) (f : {f // (x : p), f x = x}) :
structure linear_map.is_proj {S : Type u_5} [semiring S] {M : Type u_6} [ M] (m : M) {F : Type u_7} [ M (λ (_x : M), M)] (f : F) :
Prop

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.

theorem linear_map.is_proj_iff_idempotent {S : Type u_5} [semiring S] {M : Type u_6} [ M] (f : M →ₗ[S] M) :
( (p : M), f.comp f = f
def linear_map.is_proj.cod_restrict {S : Type u_5} [semiring S] {M : Type u_6} [ M] {m : M} {f : M →ₗ[S] M} (h : f) :

Restriction of the codomain of a projection of onto a subspace p to p instead of the whole space.

Equations
@[simp]
theorem linear_map.is_proj.cod_restrict_apply {S : Type u_5} [semiring S] {M : Type u_6} [ M] {m : M} {f : M →ₗ[S] M} (h : f) (x : M) :
@[simp]
theorem linear_map.is_proj.cod_restrict_apply_cod {S : Type u_5} [semiring S] {M : Type u_6} [ M] {m : M} {f : M →ₗ[S] M} (h : f) (x : m) :
theorem linear_map.is_proj.cod_restrict_ker {S : Type u_5} [semiring S] {M : Type u_6} [ M] {m : M} {f : M →ₗ[S] M} (h : f) :
theorem linear_map.is_proj.is_compl {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] E} (h : f) :
theorem linear_map.is_proj.eq_conj_prod_map' {R : Type u_1} [ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] E} (h : f) :
theorem linear_map.is_proj.eq_conj_prod_map {R : Type u_1} [comm_ring R] {E : Type u_2} [ E] {p : E} {f : E →ₗ[R] E} (h : f) :
f = _).conj)