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] { x // x ∈ p }} (hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x) :

LinearMap.ker (LinearMap.id - LinearMap.comp (Submodule.subtype p) 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] { x // x ∈ p }} (hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x) :

LinearMap.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] { x // x ∈ p }} (hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x) :

IsCompl p (LinearMap.ker f)

source

def Submodule.quotientEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) :

(E ⧸ p) ≃ₗ[R] { x // x ∈ q }

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

Equations

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

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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : { x // x ∈ q }) :

↑(LinearEquiv.symm (Submodule.quotientEquivOfIsCompl p q h)) x = Submodule.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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : { x // x ∈ q }) :

↑(Submodule.quotientEquivOfIsCompl p q h) (Submodule.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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : E ⧸ p) :

Submodule.Quotient.mk ↑(↑(Submodule.quotientEquivOfIsCompl p q h) x) = x

source

def Submodule.prodEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) :

({ x // x ∈ p } × { x // x ∈ 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

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

Instances For

source

@[simp]

theorem Submodule.coe_prodEquivOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) :

↑(Submodule.prodEquivOfIsCompl p q h) = LinearMap.coprod (Submodule.subtype p) (Submodule.subtype q)

source

@[simp]

theorem Submodule.coe_prodEquivOfIsCompl' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : { x // x ∈ p } × { x // x ∈ q }) :

↑(Submodule.prodEquivOfIsCompl p q h) x = ↑x.fst + ↑x.snd

source

@[simp]

theorem Submodule.prodEquivOfIsCompl_symm_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : { x // x ∈ p }) :

↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h)) ↑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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) (x : { x // x ∈ q }) :

↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h)) ↑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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) {x : E} :

(↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h)) x).fst = 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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) {x : E} :

(↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h)) x).snd = 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 : Submodule R E) (q : Submodule R E) (h : IsCompl p q) :

LinearEquiv.trans (LinearEquiv.prodComm R { x // x ∈ q } { x // x ∈ p }) (Submodule.prodEquivOfIsCompl p q h) = Submodule.prodEquivOfIsCompl q p (_ : IsCompl q p)

source

def Submodule.linearProjOfIsCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (q : Submodule R E) (h : IsCompl p q) :

E →ₗ[R] { x // x ∈ p }

Projection to a submodule along its complement.

Equations

Submodule.linearProjOfIsCompl p q h = LinearMap.comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h))

Instances For

source

@[simp]

theorem Submodule.linearProjOfIsCompl_apply_left {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (h : IsCompl p q) (x : { x // x ∈ p }) :

↑(Submodule.linearProjOfIsCompl p q h) ↑x = x

source

@[simp]

theorem Submodule.linearProjOfIsCompl_range {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (h : IsCompl p q) :

LinearMap.range (Submodule.linearProjOfIsCompl p 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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {x : E} :

↑(Submodule.linearProjOfIsCompl p q h) 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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) (x : E) (hx : x ∈ q) :

↑(Submodule.linearProjOfIsCompl p 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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) (x : { x // x ∈ q }) :

↑(Submodule.linearProjOfIsCompl p 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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) :

LinearMap.ker (Submodule.linearProjOfIsCompl p q h) = q

source

theorem Submodule.linearProjOfIsCompl_comp_subtype {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (h : IsCompl p q) :

LinearMap.comp (Submodule.linearProjOfIsCompl p q h) (Submodule.subtype p) = LinearMap.id

source

theorem Submodule.linearProjOfIsCompl_idempotent {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (h : IsCompl p q) (x : E) :

↑(Submodule.linearProjOfIsCompl p q h) ↑(↑(Submodule.linearProjOfIsCompl p q h) x) = ↑(Submodule.linearProjOfIsCompl p q h) x

source

theorem Submodule.existsUnique_add_of_isCompl_prod {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (hc : IsCompl p q) (x : E) :

∃! u, ↑u.fst + ↑u.snd = x

source

theorem Submodule.existsUnique_add_of_isCompl {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (hc : IsCompl p q) (x : E) :

∃ u v, ↑u + ↑v = x ∧ ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = x → r = u ∧ s = v

source

theorem Submodule.linear_proj_add_linearProjOfIsCompl_eq_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (hpq : IsCompl p q) (x : E) :

↑(↑(Submodule.linearProjOfIsCompl p q hpq) x) + ↑(↑(Submodule.linearProjOfIsCompl q p (_ : IsCompl q p)) 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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) (φ : { x // x ∈ p } →ₗ[R] F) (ψ : { x // x ∈ 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 φ ψ = LinearMap.comp (LinearMap.coprod φ ψ) ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p q h))

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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ : { x // x ∈ p } →ₗ[R] F} {ψ : { x // x ∈ q } →ₗ[R] F} (u : { x // x ∈ p }) :

↑(LinearMap.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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ : { x // x ∈ p } →ₗ[R] F} {ψ : { x // x ∈ q } →ₗ[R] F} (v : { x // x ∈ q }) :

↑(LinearMap.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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ : { x // x ∈ p } →ₗ[R] F} {ψ : { x // x ∈ q } →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u) (hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u) :

LinearMap.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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ : { x // x ∈ p } →ₗ[R] F} {ψ : { x // x ∈ q } →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = LinearMap.comp χ (Submodule.subtype p)) (hψ : ψ = LinearMap.comp χ (Submodule.subtype q)) :

LinearMap.ofIsCompl h φ ψ = χ

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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) :

LinearMap.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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ₁ : { x // x ∈ p } →ₗ[R] F} {φ₂ : { x // x ∈ p } →ₗ[R] F} {ψ₁ : { x // x ∈ q } →ₗ[R] F} {ψ₂ : { x // x ∈ q } →ₗ[R] F} :

LinearMap.ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = LinearMap.ofIsCompl h φ₁ ψ₁ + LinearMap.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 : Submodule R E} {q : Submodule R E} (h : IsCompl p q) {φ : { x // x ∈ p } →ₗ[R] F} {ψ : { x // x ∈ q } →ₗ[R] F} (c : R) :

LinearMap.ofIsCompl h (c • φ) (c • ψ) = c • LinearMap.ofIsCompl h φ ψ

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 : Submodule R₁ E} {q : Submodule R₁ E} (h : IsCompl p q) :

({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F

The linear map from (p →ₗ[R₁] F) × (q →ₗ[R₁] F) to E →ₗ[R₁] F.

Equations

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

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 : Submodule R₁ E} {q : Submodule R₁ E} (h : IsCompl p q) (φ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)) :

↑(LinearMap.ofIsComplProd h) φ = LinearMap.ofIsCompl h φ.fst φ.snd

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 : Submodule R₁ E} {q : Submodule R₁ E} (h : IsCompl p q) :

(({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F

The natural linear equivalence between (p →ₗ[R₁] F) × (q →ₗ[R₁] F) and E →ₗ[R₁] F.

Equations

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

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] { x // x ∈ p }) (hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x) :

Submodule.linearProjOfIsCompl p (LinearMap.ker f) (_ : IsCompl p (LinearMap.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 : LinearMap.range f = ⊤) (hg : LinearMap.range g = ⊤) (hfg : IsCompl (LinearMap.ker f) (LinearMap.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

LinearMap.equivProdOfSurjectiveOfIsCompl f g hf hg hfg = LinearEquiv.ofBijective (LinearMap.prod f g) (_ : Function.Injective ↑(LinearMap.prod f g) ∧ Function.Surjective ↑(LinearMap.prod f 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 : LinearMap.range f = ⊤) (hg : LinearMap.range g = ⊤) (hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)) :

↑(LinearMap.equivProdOfSurjectiveOfIsCompl f g hf hg hfg) = LinearMap.prod f 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 : LinearMap.range f = ⊤) (hg : LinearMap.range g = ⊤) (hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)) (x : E) :

↑(LinearMap.equivProdOfSurjectiveOfIsCompl f 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 // IsCompl p q } ≃ { f // ∀ (x : { x // 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 // IsCompl p q }) :

↑(↑(Submodule.isComplEquivProj p) q) = Submodule.linearProjOfIsCompl p ↑q (_ : IsCompl p ↑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 // ∀ (x : { x // x ∈ p }), ↑f ↑x = x }) :

↑(↑(Submodule.isComplEquivProj p).symm f) = LinearMap.ker ↑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 fun x => 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 FunLike type and not just linear maps, so that it can be used for example with ContinuousLinearMap or Matrix.

Instances For

source

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, LinearMap.IsProj p f) ↔ LinearMap.comp f f = f

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 : LinearMap.IsProj m f) :

M →ₗ[S] { x // x ∈ m }

Restriction of the codomain of a projection of onto a subspace p to p instead of the whole space.

Equations

LinearMap.IsProj.codRestrict h = LinearMap.codRestrict m f (_ : ∀ (x : M), ↑f x ∈ m)

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 : LinearMap.IsProj m f) (x : M) :

↑(↑(LinearMap.IsProj.codRestrict h) 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 : LinearMap.IsProj m f) (x : { x // x ∈ m }) :

↑(LinearMap.IsProj.codRestrict h) ↑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 : LinearMap.IsProj m f) :

LinearMap.ker (LinearMap.IsProj.codRestrict h) = LinearMap.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 : LinearMap.IsProj p f) :

IsCompl p (LinearMap.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 : LinearMap.IsProj p f) :

f = LinearMap.comp (↑(Submodule.prodEquivOfIsCompl p (LinearMap.ker f) (_ : IsCompl p (LinearMap.ker f)))) (LinearMap.comp (LinearMap.prodMap LinearMap.id 0) ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p (LinearMap.ker f) (_ : IsCompl p (LinearMap.ker f)))))

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 : LinearMap.IsProj p f) :

f = ↑(LinearEquiv.conj (Submodule.prodEquivOfIsCompl p (LinearMap.ker f) (_ : IsCompl p (LinearMap.ker f)))) (LinearMap.prodMap LinearMap.id 0)