# Projection to a subspace #

In this file we define

- `Submodule.linearProjOfIsCompl (p q : Submodule R E) (h : IsCompl 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`.
- `Submodule.isComplEquivProj p`: equivalence between submodules `q` such that `IsCompl 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

source
theorem LinearMap.ker_id_sub_eq_of_proj {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] ↥p} (hf : ∀ (x : ↥p), f ↑x = x) :
ker (id - p.subtype ∘ₗ f) = p
source
theorem LinearMap.range_eq_of_proj {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] ↥p} (hf : ∀ (x : ↥p), f ↑x = x) :
range f = ⊤
source
theorem LinearMap.isCompl_of_proj {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] ↥p} (hf : ∀ (x : ↥p), f ↑x = x) :
IsCompl p (ker f)
source
def Submodule.quotientEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) :
(E ⧸ p) ≃ₗ[R] ↥q

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

Equations

- p.quotientEquivOfIsCompl q h = (LinearEquiv.ofBijective (p.mkQ ∘ₗ q.subtype) ⋯).symm

Instances For

source
@[simp]
theorem Submodule.quotientEquivOfIsCompl_symm_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : ↥q) :
(p.quotientEquivOfIsCompl q h).symm x = Quotient.mk ↑x
source
@[simp]
theorem Submodule.quotientEquivOfIsCompl_apply_mk_coe {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : ↥q) :
(p.quotientEquivOfIsCompl q h) (Quotient.mk ↑x) = x
source
@[simp]
theorem Submodule.mk_quotientEquivOfIsCompl_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : E ⧸ p) :
Quotient.mk ↑((p.quotientEquivOfIsCompl q h) x) = x
source
def Submodule.prodEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) :
(↥p × ↥q) ≃ₗ[R] E

If `q` is a complement of `p`, then `p × q` is isomorphic to `E`.

Equations

- p.prodEquivOfIsCompl q h = LinearEquiv.ofBijective (p.subtype.coprod q.subtype) ⋯

Instances For

source
@[simp]
theorem Submodule.coe_prodEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) :
↑(p.prodEquivOfIsCompl q h) = p.subtype.coprod q.subtype
source
@[simp]
theorem Submodule.coe_prodEquivOfIsCompl' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : ↥p × ↥q) :
(p.prodEquivOfIsCompl q h) x = ↑x.1 + ↑x.2
source
@[simp]
theorem Submodule.prodEquivOfIsCompl_symm_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : ↥p) :
(p.prodEquivOfIsCompl q h).symm ↑x = (x, 0)
source
@[simp]
theorem Submodule.prodEquivOfIsCompl_symm_apply_right {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) (x : ↥q) :
(p.prodEquivOfIsCompl q h).symm ↑x = (0, x)
source
@[simp]
theorem Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) {x : E} :
((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
source
@[simp]
theorem Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) {x : E} :
((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p
source
@[simp]
theorem Submodule.prodComm_trans_prodEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) :
LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q h = q.prodEquivOfIsCompl p ⋯
source
def Submodule.linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) :
E →ₗ[R] ↥p

Projection to a submodule along a complement. It is the unique linear map `f : E → p` such that `f x = x` for `x ∈ p` and `f x = 0` for `x ∈ q`.

See also `LinearMap.linearProjOfIsCompl`.

Equations

- p.linearProjOfIsCompl q h = LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q h).symm

Instances For

source
noncomputable def Submodule.IsCompl.projection {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
E →ₗ[R] E

The linear projection onto a subspace along its complement as a map from the full space to itself, as opposed to `Submodule.linearProjOfIsCompl`, which maps into the subtype. This version is important as it satisfies `IsIdempotentElem`.

Equations

- Submodule.IsCompl.projection hpq = p.subtype ∘ₗ p.linearProjOfIsCompl q hpq

Instances For

source
theorem Submodule.IsCompl.projection_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(projection hpq) x = ↑((p.linearProjOfIsCompl q hpq) x)
source
@[simp]
theorem Submodule.coe_linearProjOfIsCompl_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
↑((p.linearProjOfIsCompl q hpq) x) = (IsCompl.projection hpq) x
source
@[simp]
theorem Submodule.IsCompl.projection_apply_mem {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(projection hpq) x ∈ p
source
@[simp]
theorem Submodule.linearProjOfIsCompl_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) (x : ↥p) :
(p.linearProjOfIsCompl q h) ↑x = x
source
@[simp]
theorem Submodule.IsCompl.projection_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : ↥p) :
(projection hpq) ↑x = ↑x
source
@[simp]
theorem Submodule.linearProjOfIsCompl_range {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) :
LinearMap.range (p.linearProjOfIsCompl q h) = ⊤
source
@[simp]
theorem Submodule.IsCompl.projection_range {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
LinearMap.range (projection hpq) = p
source
theorem Submodule.linearProjOfIsCompl_surjective {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) :
Function.Surjective ⇑(p.linearProjOfIsCompl q h)
source
@[simp]
theorem Submodule.linearProjOfIsCompl_apply_eq_zero_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) {x : E} :
(p.linearProjOfIsCompl q h) x = 0 ↔ x ∈ q
source
@[simp]
theorem Submodule.IsCompl.projection_apply_eq_zero_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) {x : E} :
(projection hpq) x = 0 ↔ x ∈ q
source
theorem Submodule.linearProjOfIsCompl_apply_right' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) (x : E) (hx : x ∈ q) :
(p.linearProjOfIsCompl q h) x = 0
source
@[simp]
theorem Submodule.linearProjOfIsCompl_apply_right {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) (x : ↥q) :
(p.linearProjOfIsCompl q h) ↑x = 0
source
@[simp]
theorem Submodule.linearProjOfIsCompl_ker {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) :
LinearMap.ker (p.linearProjOfIsCompl q h) = q
source
@[simp]
theorem Submodule.IsCompl.projection_ker {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
LinearMap.ker (projection hpq) = q
source
theorem Submodule.linearProjOfIsCompl_comp_subtype {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) :
p.linearProjOfIsCompl q h ∘ₗ p.subtype = LinearMap.id
source
theorem Submodule.linearProjOfIsCompl_isCompl_projection {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) (x : E) :
(p.linearProjOfIsCompl q h) ((IsCompl.projection h) x) = (p.linearProjOfIsCompl q h) x
source
@[deprecated Submodule.linearProjOfIsCompl_isCompl_projection (since := "2025-07-29")]
theorem Submodule.linearProjOfIsCompl_idempotent {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (h : IsCompl p q) (x : E) :
(p.linearProjOfIsCompl q h) ((IsCompl.projection h) x) = (p.linearProjOfIsCompl q h) x

Alias of `Submodule.linearProjOfIsCompl_isCompl_projection`.

source
@[simp]
theorem Submodule.IsCompl.projection_isIdempotentElem {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
IsIdempotentElem (projection hpq)

The linear projection onto a subspace along its complement is an idempotent.

source
theorem Submodule.existsUnique_add_of_isCompl_prod {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hc : IsCompl p q) (x : E) :
∃! u : ↥p × ↥q, ↑u.1 + ↑u.2 = x
source
theorem Submodule.existsUnique_add_of_isCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hc : IsCompl 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.IsCompl.projection_add_projection_eq_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(projection hpq) x + (projection ⋯) x = x
source
@[deprecated Submodule.IsCompl.projection_add_projection_eq_self (since := "2025-07-29")]
theorem Submodule.linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(IsCompl.projection hpq) x + (IsCompl.projection ⋯) x = x

Alias of `Submodule.IsCompl.projection_add_projection_eq_self`.

source
@[deprecated Submodule.linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self (since := "2025-07-11")]
theorem Submodule.linear_proj_add_linearProjOfIsCompl_eq_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(IsCompl.projection hpq) x + (IsCompl.projection ⋯) x = x

Alias of `Submodule.IsCompl.projection_add_projection_eq_self`.

Alias of `Submodule.IsCompl.projection_add_projection_eq_self`.

source
theorem Submodule.IsCompl.projection_eq_self_sub_projection {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(projection ⋯) x = x - (projection hpq) x
source
@[deprecated Submodule.IsCompl.projection_eq_self_sub_projection (since := "2025-07-29")]
theorem Submodule.linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(IsCompl.projection ⋯) x = x - (IsCompl.projection hpq) x

Alias of `Submodule.IsCompl.projection_eq_self_sub_projection`.

source
@[simp]
theorem Submodule.IsCompl.projection_eq_self_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(projection hpq) x = x ↔ x ∈ p

The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`.

source
@[deprecated Submodule.IsCompl.projection_eq_self_iff (since := "2025-07-29")]
theorem Submodule.linearProjOfIsCompl_eq_self_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) :
(IsCompl.projection hpq) x = x ↔ x ∈ p

Alias of `Submodule.IsCompl.projection_eq_self_iff`.

The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`.

source
def LinearMap.linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (q : Submodule R E) {F : Type u_7} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i) (h : IsCompl (range i) q) :
E →ₗ[R] F

Projection to the image of an injection along a complement.

This has an advantage over `Submodule.linearProjOfIsCompl` in that it allows the user better definitional control over the type.

Equations

- LinearMap.linearProjOfIsCompl q i hi h = ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ (LinearMap.range i).linearProjOfIsCompl q h

Instances For

source
@[simp]
theorem LinearMap.linearProjOfIsCompl_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (q : Submodule R E) {F : Type u_7} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i) (h : IsCompl (range i) q) (x : F) :
(linearProjOfIsCompl q i hi h) (i x) = x
source
theorem LinearMap.linearProjOfIsCompl_apply_right' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (q : Submodule R E) {F : Type u_7} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i) (h : IsCompl (range i) q) (x : E) (hx : x ∈ q) :
(linearProjOfIsCompl q i hi h) x = 0
source
@[simp]
theorem LinearMap.linearProjOfIsCompl_apply_right {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (q : Submodule R E) {F : Type u_7} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i) (h : IsCompl (range i) q) (x : ↥q) :
(linearProjOfIsCompl q i hi h) ↑x = 0
source
@[simp]
theorem LinearMap.ker_linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (q : Submodule R E) {F : Type u_7} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i) (h : IsCompl (range i) q) :
ker (linearProjOfIsCompl q i hi h) = q
source
def LinearMap.ofIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) (φ : ↥p →ₗ[R] F) (ψ : ↥q →ₗ[R] F) :
E →ₗ[R] F

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

Equations

- LinearMap.ofIsCompl h φ ψ = φ.coprod ψ ∘ₗ ↑(p.prodEquivOfIsCompl q h).symm

Instances For

source
@[simp]
theorem LinearMap.ofIsCompl_left_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (u : ↥p) :
(ofIsCompl h φ ψ) ↑u = φ u
source
@[simp]
theorem LinearMap.ofIsCompl_right_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (v : ↥q) :
(ofIsCompl h φ ψ) ↑v = ψ v
source
theorem LinearMap.ofIsCompl_eq {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : ∀ (u : ↥p), φ u = χ ↑u) (hψ : ∀ (u : ↥q), ψ u = χ ↑u) :
ofIsCompl h φ ψ = χ
source
theorem LinearMap.ofIsCompl_eq' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = χ ∘ₗ p.subtype) (hψ : ψ = χ ∘ₗ q.subtype) :
ofIsCompl h φ ψ = χ
source
theorem LinearMap.ofIsCompl_eq_add {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} :
ofIsCompl hpq φ ψ = φ ∘ₗ p.linearProjOfIsCompl q hpq + ψ ∘ₗ q.linearProjOfIsCompl p ⋯
source
@[simp]
theorem LinearMap.ofIsCompl_zero {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) :
ofIsCompl h 0 0 = 0
source
@[simp]
theorem LinearMap.ofIsCompl_add {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ₁ φ₂ : ↥p →ₗ[R] F} {ψ₁ ψ₂ : ↥q →ₗ[R] F} :
ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂
source
@[simp]
theorem LinearMap.ofIsCompl_smul {R : Type u_7} [CommRing R] {E : Type u_8} [AddCommGroup E] [Module R E] {F : Type u_9} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} (c : R) :
ofIsCompl h (c • φ) (c • ψ) = c • ofIsCompl h φ ψ
source
theorem LinearMap.surjective_comp_linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} {M : Type u_6} [AddCommMonoid M] (h : IsCompl p q) [Module R M] :
Function.Surjective (p.linearProjOfIsCompl q h).comp
source
theorem LinearMap.surjective_comp_subtype_of_isComplemented {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {M : Type u_6} [AddCommMonoid M] (h : IsComplemented p) [Module R M] :
Function.Surjective fun (f : E →ₗ[R] M) => f ∘ₗ p.subtype
source
@[simp]
theorem LinearMap.range_ofIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} :
range (ofIsCompl hpq φ ψ) = range φ ⊔ range ψ
source
theorem LinearMap.ofIsCompl_subtype_zero_eq {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
ofIsCompl hpq p.subtype 0 = Submodule.IsCompl.projection hpq
source
theorem LinearMap.ofIsCompl_symm {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F} {ψ : ↥q →ₗ[R] F} :
ofIsCompl ⋯ ψ φ = ofIsCompl hpq φ ψ
source
def LinearMap.ofIsComplProd {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {R₁ : Type u_7} [CommRing R₁] [Module R₁ E] [Module R₁ F] {p q : Submodule R₁ E} (h : IsCompl 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

- LinearMap.ofIsComplProd h = { toFun := fun (φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)) => LinearMap.ofIsCompl h φ.1 φ.2, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem LinearMap.ofIsComplProd_apply {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {R₁ : Type u_7} [CommRing R₁] [Module R₁ E] [Module R₁ F] {p q : Submodule R₁ E} (h : IsCompl p q) (φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)) :
(ofIsComplProd h) φ = ofIsCompl h φ.1 φ.2
source
def LinearMap.ofIsComplProdEquiv {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {R₁ : Type u_7} [CommRing R₁] [Module R₁ E] [Module R₁ F] {p q : Submodule R₁ E} (h : IsCompl 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

- LinearMap.ofIsComplProdEquiv h = { toLinearMap := LinearMap.ofIsComplProd h, invFun := fun (φ : E →ₗ[R₁] F) => (φ.domRestrict p, φ.domRestrict q), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem LinearMap.linearProjOfIsCompl_of_proj {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} (f : E →ₗ[R] ↥p) (hf : ∀ (x : ↥p), f ↑x = x) :
p.linearProjOfIsCompl (ker f) ⋯ = f
source
def LinearMap.equivProdOfSurjectiveOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] (f : E →ₗ[R] F) (g : E →ₗ[R] G) (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (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.equivProdOfSurjectiveOfIsCompl g hf hg hfg = LinearEquiv.ofBijective (f.prod g) ⋯

Instances For

source
@[simp]
theorem LinearMap.coe_equivProdOfSurjectiveOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) :
↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = f.prod g
source
@[simp]
theorem LinearMap.equivProdOfSurjectiveOfIsCompl_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) (x : E) :
(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
source
def Submodule.isComplEquivProj {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) :
{ q : Submodule R E // IsCompl p q } ≃ { f : E →ₗ[R] ↥p // ∀ (x : ↥p), f ↑x = x }

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Submodule.coe_isComplEquivProj_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : { q : Submodule R E // IsCompl p q }) :
↑(p.isComplEquivProj q) = p.linearProjOfIsCompl ↑q ⋯
source
@[simp]
theorem Submodule.coe_isComplEquivProj_symm_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (f : { f : E →ₗ[R] ↥p // ∀ (x : ↥p), f ↑x = x }) :
↑(p.isComplEquivProj.symm f) = LinearMap.ker ↑f
source
def Submodule.isIdempotentElemEquiv {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) :
{ f : Module.End R E // IsIdempotentElem f ∧ LinearMap.range f = p } ≃ { f : E →ₗ[R] ↥p // ∀ (x : ↥p), f ↑x = x }

The idempotent endomorphisms of a module with range equal to a submodule are in 1-1 correspondence with linear maps to the submodule that restrict to the identity on the submodule.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Submodule.isIdempotentElemEquiv_apply_coe {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (f : { f : Module.End R E // IsIdempotentElem f ∧ LinearMap.range f = p }) :
↑(p.isIdempotentElemEquiv f) = LinearMap.codRestrict p ↑f ⋯
source
@[simp]
theorem Submodule.isIdempotentElemEquiv_symm_apply_coe {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (f : { f : E →ₗ[R] ↥p // ∀ (x : ↥p), f ↑x = x }) :
↑(p.isIdempotentElemEquiv.symm f) = p.subtype ∘ₗ ↑f
source
structure LinearMap.IsProj {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] (m : Submodule S M) {F : Type u_7} [FunLike F 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 `FunLike` type and not just linear maps, so that it can be used for example with `ContinuousLinearMap` or `Matrix`.

- map_mem (x : M) : f x ∈ m
- map_id (x : M) : x ∈ m → f x = x

Instances For

source
theorem LinearMap.isProj_range_iff_isIdempotentElem {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] (f : M →ₗ[S] M) :
IsProj (range f) f ↔ IsIdempotentElem f
source
theorem LinearMap.IsIdempotentElem.isProj_range {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] (f : M →ₗ[S] M) :
IsIdempotentElem f → IsProj (range f) f

Alias of the reverse direction of `LinearMap.isProj_range_iff_isIdempotentElem`.

source
theorem LinearMap.isProj_iff_isIdempotentElem {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] (f : M →ₗ[S] M) :
(∃ (p : Submodule S M), IsProj p f) ↔ IsIdempotentElem f
source
theorem LinearMap.IsProj.isIdempotentElem {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj m f) :
IsIdempotentElem f
source
theorem LinearMap.IsProj.mem_iff_map_id {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj m f) {x : M} :
x ∈ m ↔ f x = x
source
def LinearMap.IsProj.codRestrict {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj 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.codRestrict = LinearMap.codRestrict m f ⋯

Instances For

source
@[simp]
theorem LinearMap.IsProj.codRestrict_apply {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj m f) (x : M) :
↑(h.codRestrict x) = f x
source
@[simp]
theorem LinearMap.IsProj.codRestrict_apply_cod {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj m f) (x : ↥m) :
h.codRestrict ↑x = x
source
theorem LinearMap.IsProj.codRestrict_ker {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj m f) :
ker h.codRestrict = ker f
source
theorem LinearMap.IsProj.isCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] E} (h : IsProj p f) :
IsCompl p (ker f)
source
theorem LinearMap.IsProj.eq_conj_prod_map' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] E} (h : IsProj p f) :
f = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm
source
theorem LinearMap.IsProj.submodule_unique {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {f : M →ₗ[S] M} {m₁ m₂ : Submodule S M} (hf₁ : IsProj m₁ f) (hf₂ : IsProj m₂ f) :
m₁ = m₂
source
theorem LinearMap.IsProj.range {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (h : IsProj m f) :
range f = m
source
theorem LinearMap.IsProj.bot (S : Type u_5) [Semiring S] (M : Type u_6) [AddCommMonoid M] [Module S M] :
IsProj ⊥ 0
source
theorem LinearMap.IsProj.top (S : Type u_5) [Semiring S] (M : Type u_6) [AddCommMonoid M] [Module S M] :
IsProj ⊤ id
source
theorem LinearMap.IsProj.subtype_comp_codRestrict {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) :
U.subtype ∘ₗ hf.codRestrict = f
source
theorem LinearMap.IsProj.submodule_eq_top_iff {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj m f) :
m = ⊤ ↔ f = id
source
theorem LinearMap.IsProj.submodule_eq_bot_iff {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {m : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj m f) :
m = ⊥ ↔ f = 0
source
theorem LinearMap.IsIdempotentElem.isCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
IsCompl (range f) (ker f)
source
theorem LinearMap.IsIdempotentElem.mem_range_iff {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {p : M →ₗ[S] M} (hp : IsIdempotentElem p) {x : M} :
x ∈ range p ↔ p x = x

Given an idempotent linear operator `p`, we have `x ∈ range p` if and only if `p(x) = x` for all `x`.

source
theorem LinearMap.IsIdempotentElem.eq_isCompl_projection {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {T : E →ₗ[R] E} (hT : IsIdempotentElem T) :
T = Submodule.IsCompl.projection ⋯

An idempotent linear operator is equal to the linear projection onto its range along its kernel.

source
theorem LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {T : E →ₗ[R] E} :
IsIdempotentElem T ↔ ∃ (h : IsCompl (range T) (ker T)), T = Submodule.IsCompl.projection h

A linear map is an idempotent if and only if it equals the projection onto its range along its kernel.

source
theorem LinearMap.IsIdempotentElem.comp_eq_right_iff {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M] {q : M →ₗ[S] M} (hq : IsIdempotentElem q) {E : Type u_7} [AddCommMonoid E] [Module S E] (p : E →ₗ[S] M) :
q ∘ₗ p = p ↔ range p ≤ range q

Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`.

source
theorem LinearMap.IsIdempotentElem.ext_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
p = q ↔ range p = range q ∧ ker p = ker q

Idempotent operators are equal iff their range and kernels are.

source
theorem LinearMap.IsIdempotentElem.ext {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
range p = range q ∧ ker p = ker q → p = q

Alias of the reverse direction of `LinearMap.IsIdempotentElem.ext_iff`.

Idempotent operators are equal iff their range and kernels are.

source
theorem LinearMap.IsIdempotentElem.range_eq_ker {S : Type u_5} [Semiring S] {E : Type u_7} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :
range p = ker (1 - p)
source
theorem LinearMap.IsIdempotentElem.ker_eq_range {S : Type u_5} [Semiring S] {E : Type u_7} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :
ker p = range (1 - p)
source
theorem LinearMap.IsIdempotentElem.comp_eq_left_iff {S : Type u_5} [Semiring S] {M : Type u_7} [AddCommGroup M] [Module S M] {q : M →ₗ[S] M} (hq : IsIdempotentElem q) {E : Type u_8} [AddCommGroup E] [Module S E] (p : M →ₗ[S] E) :
p ∘ₗ q = p ↔ ker q ≤ ker p
source
theorem LinearMap.IsProj.eq_conj_prodMap {R : Type u_1} [CommRing R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {f : E →ₗ[R] E} (h : IsProj p f) :
f = (p.prodEquivOfIsCompl (ker f) ⋯).conj (id.prodMap 0)
source
theorem LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
range f ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

`range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`, for idempotent `f`.

source
theorem LinearMap.IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
range f ∈ Module.End.invtSubmodule T → f ∘ₗ T ∘ₗ f = T ∘ₗ f

Alias of the forward direction of `LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

`range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`, for idempotent `f`.

source
theorem LinearMap.IsIdempotentElem.range_mem_invtSubmodule {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
f ∘ₗ T ∘ₗ f = T ∘ₗ f → range f ∈ Module.End.invtSubmodule T

Alias of the reverse direction of `LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

`range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`, for idempotent `f`.

source
theorem LinearMap.IsProj.mem_invtSubmodule_iff {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} {U : Submodule R E} (hf : IsProj U f) :
U ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f
source
theorem LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
ker f ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T

`ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`, for idempotent `f`.

source
theorem LinearMap.IsIdempotentElem.ker_mem_invtSubmodule {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
f ∘ₗ T ∘ₗ f = f ∘ₗ T → ker f ∈ Module.End.invtSubmodule T

Alias of the reverse direction of `LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

`ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`, for idempotent `f`.

source
theorem LinearMap.IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
ker f ∈ Module.End.invtSubmodule T → f ∘ₗ T ∘ₗ f = f ∘ₗ T

Alias of the forward direction of `LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

`ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`, for idempotent `f`.

source
theorem LinearMap.IsIdempotentElem.commute_iff {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hf : IsIdempotentElem f) :
Commute f T ↔ range f ∈ Module.End.invtSubmodule T ∧ ker f ∈ Module.End.invtSubmodule T

An idempotent operator `f` commutes with a linear operator `T` if and only if both `range f` and `ker f` are invariant under `T`.

source
theorem LinearMap.IsIdempotentElem.commute_iff_of_isUnit {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {T f : E →ₗ[R] E} (hT : IsUnit T) (hf : IsIdempotentElem f) :
Commute f T ↔ Submodule.map T (range f) = range f ∧ Submodule.map T (ker f) = ker f

An idempotent operator `f` commutes with an unit operator `T` if and only if `T (range f) = range f` and `T (ker f) = ker f`.