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 moduleEto a submodulepalong its complementq; it is the unique linear mapf : E → psuch thatf x = xforx ∈ pandf x = 0forx ∈ q.is_compl_equiv_proj p: equivalence between submodulesqsuch thatis_compl p qand projectionsf : E → p,∀ x ∈ p, f x = x.
We also provide some lemmas justifying correctness of our definitions.
Tags
projection, complement subspace
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
- p.quotient_equiv_of_is_compl q h = (linear_equiv.of_bijective (p.mkq.comp q.subtype) _ _).symm
@[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
@[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
@[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) :
submodule.quotient.mk ↑(⇑(p.quotient_equiv_of_is_compl q h) x) = x
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) :
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) _ _
@[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.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)
@[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)
@[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) :
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)
@[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
@[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) :
(p.linear_proj_of_is_compl q h).range = ⊤
@[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
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) :
⇑(p.linear_proj_of_is_compl q h) ↑x = 0
@[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) :
(p.linear_proj_of_is_compl q h).ker = 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) :
(p.linear_proj_of_is_compl q h).comp p.subtype = linear_map.id
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
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) :
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) _ _
@[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) :
↑(f.equiv_prod_of_surjective_of_is_compl g hf 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}
[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) :
⇑(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg) x = (⇑f x, ⇑g x)
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) :
Equivalence between submodules q such that is_compl p q and linear maps f : E →ₗ[R] p
such that ∀ x : p, f x = x.
@[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 _