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

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.

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.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_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) ↑((p.linearProjOfIsCompl q h) x) = (p.linearProjOfIsCompl q h) x

source

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

↑((p.linearProjOfIsCompl q hpq) x) + ↑((q.linearProjOfIsCompl p ⋯) x) = x

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

↑((p.linearProjOfIsCompl q hpq) x) + ↑((q.linearProjOfIsCompl p ⋯) x) = x

Alias of Submodule.linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self.

source

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

↑((q.linearProjOfIsCompl p ⋯) x) = x - ↑((p.linearProjOfIsCompl q hpq) x)

source

@[simp]

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

↑((p.linearProjOfIsCompl q hpq) x) = x ↔ x ∈ p

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

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

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

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

@[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 = p.subtype ∘ₗ p.linearProjOfIsCompl q 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

@[deprecated LinearMap.isProj_iff_isIdempotentElem (since := "2025-01-12")]

theorem LinearMap.isProj_iff_idempotent {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

Alias of LinearMap.isProj_iff_isIdempotentElem.

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.

Documentation

Mathlib.LinearAlgebra.Projection

Projection to a subspace #

Tags #