linear_algebra.projection

source

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} (hf : ∀ (x : ↥p), ⇑f ↑x = x) :

linear_map.ker (linear_map.id - p.subtype.comp f) = p

source

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} (hf : ∀ (x : ↥p), ⇑f ↑x = x) :

linear_map.range f = ⊤

source

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} (hf : ∀ (x : ↥p), ⇑f ↑x = x) :

is_compl p (linear_map.ker f)

source

noncomputable 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) (h : is_compl p q) :

(E ⧸ p) ≃ₗ[R] ↥q

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

source

@[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) :

⇑((p.quotient_equiv_of_is_compl q h).symm) x = submodule.quotient.mk ↑x

source

@[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) :

⇑(p.quotient_equiv_of_is_compl q h) (submodule.quotient.mk ↑x) = x

source

@[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 : E ⧸ p) :

submodule.quotient.mk ↑(⇑(p.quotient_equiv_of_is_compl q h) x) = x

source

noncomputable 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) (h : 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

p.prod_equiv_of_is_compl q h = linear_equiv.of_bijective (p.subtype.coprod q.subtype) _

source

@[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) :

↑(p.prod_equiv_of_is_compl q h) = p.subtype.coprod q.subtype

source

@[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) :

⇑(p.prod_equiv_of_is_compl q h) x = ↑(x.fst) + ↑(x.snd)

source

@[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) :

⇑((p.prod_equiv_of_is_compl q h).symm) ↑x = (x, 0)

source

@[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) :

⇑((p.prod_equiv_of_is_compl q h).symm) ↑x = (0, x)

source

@[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} :

(⇑((p.prod_equiv_of_is_compl q h).symm) x).fst = 0 ↔ x ∈ q

source

@[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} :

(⇑((p.prod_equiv_of_is_compl q h).symm) x).snd = 0 ↔ x ∈ p

source

@[simp]

theorem submodule.prod_comm_trans_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) :

(linear_equiv.prod_comm R ↥q ↥p).trans (p.prod_equiv_of_is_compl q h) = q.prod_equiv_of_is_compl p _

source

noncomputable 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) (h : is_compl p q) :

E →ₗ[R] ↥p

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)

source

@[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) :

⇑(p.linear_proj_of_is_compl q h) ↑x = x

source

@[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) :

linear_map.range (p.linear_proj_of_is_compl q h) = ⊤

source

@[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} :

⇑(p.linear_proj_of_is_compl q h) x = 0 ↔ x ∈ q

source

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) (hx : x ∈ q) :

⇑(p.linear_proj_of_is_compl q h) x = 0

source

@[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) :

⇑(p.linear_proj_of_is_compl q h) ↑x = 0

source

@[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) :

linear_map.ker (p.linear_proj_of_is_compl q h) = q

source

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) :

(p.linear_proj_of_is_compl q h).comp p.subtype = linear_map.id

source

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) :

⇑(p.linear_proj_of_is_compl q h) ↑(⇑(p.linear_proj_of_is_compl q h) x) = ⇑(p.linear_proj_of_is_compl q h) x

source

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

∃! (u : ↥p × ↥q), ↑(u.fst) + ↑(u.snd) = x

source

theorem submodule.exists_unique_add_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} (hc : is_compl p q) (x : E) :

∃ (u : ↥p) (v : ↥q), ↑u + ↑v = x ∧ ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = u ∧ s = v

source

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

↑(⇑(p.linear_proj_of_is_compl q hpq) x) + ↑(⇑(q.linear_proj_of_is_compl p _) x) = x

source

noncomputable def linear_map.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] {p q : submodule R E} (h : is_compl p q) (φ : ↥p →ₗ[R] F) (ψ : ↥q →ₗ[R] F) :

E →ₗ[R] F

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)

source

@[simp]

theorem linear_map.of_is_compl_left_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] {p q : submodule R E} (h : is_compl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (u : ↥p) :

⇑(linear_map.of_is_compl h φ ψ) ↑u = ⇑φ u

source

@[simp]

theorem linear_map.of_is_compl_right_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] {p q : submodule R E} (h : is_compl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (v : ↥q) :

⇑(linear_map.of_is_compl h φ ψ) ↑v = ⇑ψ v

source

theorem linear_map.of_is_compl_eq {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] {p q : submodule R E} (h : is_compl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : ∀ (u : ↥p), ⇑φ u = ⇑χ ↑u) (hψ : ∀ (u : ↥q), ⇑ψ u = ⇑χ ↑u) :

linear_map.of_is_compl h φ ψ = χ

source

theorem linear_map.of_is_compl_eq' {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] {p q : submodule R E} (h : is_compl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = χ.comp p.subtype) (hψ : ψ = χ.comp q.subtype) :

linear_map.of_is_compl h φ ψ = χ

source

@[simp]

theorem linear_map.of_is_compl_zero {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] {p q : submodule R E} (h : is_compl p q) :

linear_map.of_is_compl h 0 0 = 0

source

@[simp]

theorem linear_map.of_is_compl_add {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] {p q : submodule R E} (h : is_compl p q) {φ₁ φ₂ : ↥p →ₗ[R] F} {ψ₁ ψ₂ : ↥q →ₗ[R] F} :

linear_map.of_is_compl h (φ₁ + φ₂) (ψ₁ + ψ₂) = linear_map.of_is_compl h φ₁ ψ₁ + linear_map.of_is_compl h φ₂ ψ₂

source

@[simp]

theorem linear_map.of_is_compl_smul {R : Type u_1} [comm_ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {p q : submodule R E} (h : is_compl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (c : R) :

linear_map.of_is_compl h (c • φ) (c • ψ) = c • linear_map.of_is_compl h φ ψ

source

noncomputable def linear_map.of_is_compl_prod {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : submodule R₁ E} (h : is_compl p 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

linear_map.of_is_compl_prod h = {to_fun := λ (φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), linear_map.of_is_compl h φ.fst φ.snd, map_add' := _, map_smul' := _}

source

@[simp]

theorem linear_map.of_is_compl_prod_apply {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : submodule R₁ E} (h : is_compl p q) (φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)) :

⇑(linear_map.of_is_compl_prod h) φ = linear_map.of_is_compl h φ.fst φ.snd

source

noncomputable def linear_map.of_is_compl_prod_equiv {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {R₁ : Type u_7} [comm_ring R₁] [module R₁ E] [module R₁ F] {p q : submodule R₁ E} (h : is_compl p 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

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 := _}

source

@[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) :

p.linear_proj_of_is_compl (linear_map.ker f) _ = f

source

noncomputable 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) (hf : linear_map.range f = ⊤) (hg : linear_map.range g = ⊤) (hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :

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

f.equiv_prod_of_surjective_of_is_compl g hf hg hfg = linear_equiv.of_bijective (f.prod g) _

source

@[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 : linear_map.range f = ⊤) (hg : linear_map.range g = ⊤) (hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :

↑(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg) = f.prod g

source

@[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 : linear_map.range f = ⊤) (hg : linear_map.range g = ⊤) (hfg : is_compl (linear_map.ker f) (linear_map.ker g)) (x : E) :

⇑(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg) x = (⇑f x, ⇑g x)

source

noncomputable 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

p.is_compl_equiv_proj = {to_fun := λ (q : {q // is_compl p q}), ⟨p.linear_proj_of_is_compl ↑q _, _⟩, inv_fun := λ (f : {f // ∀ (x : ↥p), ⇑f ↑x = x}), ⟨linear_map.ker ↑f, _⟩, left_inv := _, right_inv := _}

source

@[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}) :

↑(⇑(p.is_compl_equiv_proj) q) = p.linear_proj_of_is_compl ↑q _

source

@[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}) :

↑(⇑(p.is_compl_equiv_proj.symm) f) = linear_map.ker ↑f

source

structure linear_map.is_proj {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] (m : submodule S M) {F : Type u_7} [fun_like F M (λ (_x : M), M)] (f : F) :

Prop

map_mem : ∀ (x : M), ⇑f x ∈ m
map_id : ∀ (x : M), x ∈ m → ⇑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.

source

theorem linear_map.is_proj_iff_idempotent {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] (f : M →ₗ[S] M) :

(∃ (p : submodule S M), linear_map.is_proj p f) ↔ f.comp f = f

source

def linear_map.is_proj.cod_restrict {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] {m : submodule S M} {f : M →ₗ[S] M} (h : linear_map.is_proj m f) :

M →ₗ[S] ↥m

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 _

source

@[simp]

theorem linear_map.is_proj.cod_restrict_apply {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] {m : submodule S M} {f : M →ₗ[S] M} (h : linear_map.is_proj m f) (x : M) :

↑(⇑(h.cod_restrict) x) = ⇑f x

source

@[simp]

theorem linear_map.is_proj.cod_restrict_apply_cod {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] {m : submodule S M} {f : M →ₗ[S] M} (h : linear_map.is_proj m f) (x : ↥m) :

⇑(h.cod_restrict) ↑x = x

source

theorem linear_map.is_proj.cod_restrict_ker {S : Type u_5} [semiring S] {M : Type u_6} [add_comm_monoid M] [module S M] {m : submodule S M} {f : M →ₗ[S] M} (h : linear_map.is_proj m f) :

linear_map.ker h.cod_restrict = linear_map.ker f

source

theorem linear_map.is_proj.is_compl {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] E} (h : linear_map.is_proj p f) :

is_compl p (linear_map.ker f)

source

theorem linear_map.is_proj.eq_conj_prod_map' {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] E} (h : linear_map.is_proj p f) :

f = (p.prod_equiv_of_is_compl (linear_map.ker f) _).to_linear_map.comp ((linear_map.id.prod_map 0).comp (p.prod_equiv_of_is_compl (linear_map.ker f) _).symm.to_linear_map)

source

theorem linear_map.is_proj.eq_conj_prod_map {R : Type u_1} [comm_ring R] {E : Type u_2} [add_comm_group E] [module R E] {p : submodule R E} {f : E →ₗ[R] E} (h : linear_map.is_proj p f) :

f = ⇑((p.prod_equiv_of_is_compl (linear_map.ker f) _).conj) (linear_map.id.prod_map 0)

mathlib3 documentation

Projection to a subspace #

Tags #