mathlib documentation

linear_algebra.projection

Projection to a subspace

In this file we define

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} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] p} :
(∀ (x : p), f x = x)(linear_map.id - p.subtype.comp f).ker = p

theorem linear_map.range_eq_of_proj {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] p} :
(∀ (x : p), f x = x)f.range =

theorem linear_map.is_compl_of_proj {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] p} :
(∀ (x : p), f x = x)is_compl p f.ker

def submodule.quotient_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) :

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} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : q) :

@[simp]
theorem submodule.quotient_equiv_of_is_compl_apply_mk_coe {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : q) :

@[simp]
theorem submodule.mk_quotient_equiv_of_is_compl_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : p.quotient) :

def submodule.prod_equiv_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) :
is_compl p q((p × q) ≃ₗ[R] E)

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} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) :

@[simp]
theorem submodule.coe_prod_equiv_of_is_compl' {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : p × q) :

@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_left {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : p) :

@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_right {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) (x : q) :

@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_fst_eq_zero {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) {x : E} :

@[simp]
theorem submodule.prod_equiv_of_is_compl_symm_apply_snd_eq_zero {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) (h : is_compl p q) {x : E} :

def submodule.linear_proj_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p q : submodule R E) :
is_compl p q(E →ₗ[R] p)

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} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) (x : p) :

@[simp]
theorem submodule.linear_proj_of_is_compl_range {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) :

@[simp]
theorem submodule.linear_proj_of_is_compl_apply_eq_zero_iff {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) {x : E} :

theorem submodule.linear_proj_of_is_compl_apply_right' {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) (x : E) :
x q(p.linear_proj_of_is_compl q h) x = 0

@[simp]
theorem submodule.linear_proj_of_is_compl_apply_right {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) (x : q) :

@[simp]
theorem submodule.linear_proj_of_is_compl_ker {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) :

theorem submodule.linear_proj_of_is_compl_comp_subtype {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) :

theorem submodule.linear_proj_of_is_compl_idempotent {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p q : submodule R E} (h : is_compl p q) (x : E) :

@[simp]
theorem linear_map.linear_proj_of_is_compl_of_proj {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} (f : E →ₗ[R] p) (hf : ∀ (x : p), f x = x) :

def linear_map.equiv_prod_of_surjective_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (f : E →ₗ[R] F) (g : E →ₗ[R] G) :
f.range = g.range = is_compl f.ker g.ker(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
@[simp]
theorem linear_map.coe_equiv_prod_of_surjective_of_is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : f.range = ) (hg : g.range = ) (hfg : is_compl f.ker g.ker) :

@[simp]
theorem linear_map.equiv_prod_of_surjective_of_is_compl_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : f.range = ) (hg : g.range = ) (hfg : is_compl f.ker g.ker) (x : E) :

def submodule.is_compl_equiv_proj {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p : submodule R E) :
{q // is_compl p 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} [add_comm_group E] [module R E] (p : submodule R E) (q : {q // is_compl p q}) :

@[simp]
theorem submodule.coe_is_compl_equiv_proj_symm_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] (p : submodule R E) (f : {f // ∀ (x : p), f x = x}) :