doc-next-gen

Mathlib.LinearAlgebra.Projection

Module docstring

{"# 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 "}

LinearMap.ker_id_sub_eq_of_proj theorem
{f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : ker (id - p.subtype.comp f) = p
Full source 
theorem ker_id_sub_eq_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) :
    ker (id - p.subtype.comp f) = p := by
  ext x
  simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]
  exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by rw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩
Kernel of Identity Minus Projection Equals Submodule
Informal description
Let $E$ be a module over a ring $R$ and $p$ be a submodule of $E$. For any linear map $f: E \to p$ such that $f(x) = x$ for all $x \in p$, the kernel of the map $\text{id} - \iota \circ f$ equals $p$, where $\iota: p \hookrightarrow E$ is the inclusion map and $\text{id}$ is the identity map on $E$.
LinearMap.range_eq_of_proj theorem
{f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : range f = ⊤
Full source 
theorem range_eq_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : range f = ⊤ :=
  range_eq_top.2 fun x => ⟨x, hf x⟩
Range of Projection Map is Entire Submodule
Informal description
Let $E$ be a module over a ring $R$ and $p$ be a submodule of $E$. For any linear map $f: E \to p$ such that $f(x) = x$ for all $x \in p$, the range of $f$ is the entire submodule $p$ (i.e., $\text{range}(f) = \top$).
LinearMap.isCompl_of_proj theorem
{f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : IsCompl p (ker f)
Full source 
theorem isCompl_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : IsCompl p (ker f) := by
  constructor
  · rw [disjoint_iff_inf_le]
    rintro x ⟨hpx, hfx⟩
    rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
    simp only [hfx, SetLike.mem_coe, zero_mem]
  · rw [codisjoint_iff_le_sup]
    intro x _
    rw [mem_sup']
    refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
    rw [mem_ker, LinearMap.map_sub, hf, sub_self]
Complementarity of Submodule and Kernel under Projection Condition
Informal description
Let $E$ be a module over a ring $R$ and $p$ be a submodule of $E$. For any linear map $f: E \to p$ such that $f(x) = x$ for all $x \in p$, the submodule $p$ and the kernel of $f$ are complementary, i.e., $p \sqcap \ker f = \bot$ and $p \sqcup \ker f = \top$.
Submodule.quotientEquivOfIsCompl definition
(h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q
Full source 
/-- If `q` is a complement of `p`, then `M/p ≃ q`. -/
def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q :=
  LinearEquiv.symm <|
    LinearEquiv.ofBijective (p.mkQ.comp q.subtype)
      ⟨by rw [← ker_eq_bot, ker_comp, ker_mkQ, disjoint_iff_comap_eq_bot.1 h.symm.disjoint], by
        rw [← range_eq_top, range_comp, range_subtype, map_mkQ_eq_top, h.sup_eq_top]⟩
Linear equivalence between quotient module and complement submodule
Informal description
Given a module $E$ over a ring $R$ and two submodules $p$ and $q$ of $E$ that are complements (i.e., $p \sqcap q = \bot$ and $p \sqcup q = \top$), there is a linear equivalence between the quotient module $E ⧸ p$ and the submodule $q$. This equivalence is constructed by composing the quotient map $E \to E ⧸ p$ with the inclusion map $q \hookrightarrow E$, and it is bijective due to the complementarity of $p$ and $q$.
Submodule.quotientEquivOfIsCompl_symm_apply theorem
(h : IsCompl p q) (x : q) : -- Porting note: type ascriptions needed on the RHS(quotientEquivOfIsCompl p q h).symm x = (Quotient.mk x : E ⧸ p)
Full source 
@[simp]
theorem quotientEquivOfIsCompl_symm_apply (h : IsCompl p q) (x : q) :
    -- Porting note: type ascriptions needed on the RHS
    (quotientEquivOfIsCompl p q h).symm x = (Quotient.mk x : E ⧸ p) := rfl
Inverse of Linear Equivalence between Quotient Module and Complement Submodule
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be submodules of $E$ that are complements (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x \in q$, the inverse of the linear equivalence $\text{quotientEquivOfIsCompl}\, p\, q\, h$ maps $x$ to the equivalence class $[x]$ in the quotient module $E ⧸ p$.
Submodule.quotientEquivOfIsCompl_apply_mk_coe theorem
(h : IsCompl p q) (x : q) : quotientEquivOfIsCompl p q h (Quotient.mk x) = x
Full source 
@[simp]
theorem quotientEquivOfIsCompl_apply_mk_coe (h : IsCompl p q) (x : q) :
    quotientEquivOfIsCompl p q h (Quotient.mk x) = x :=
  (quotientEquivOfIsCompl p q h).apply_symm_apply x
Linear equivalence $\varphi$ maps equivalence class of $x$ to $x$ for $x \in q$
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be submodules of $E$ that are complements (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x \in q$, the linear equivalence $\varphi : E ⧸ p \to q$ satisfies $\varphi([x]) = x$, where $[x]$ denotes the equivalence class of $x$ in the quotient module $E ⧸ p$.
Submodule.mk_quotientEquivOfIsCompl_apply theorem
(h : IsCompl p q) (x : E ⧸ p) : (Quotient.mk (quotientEquivOfIsCompl p q h x) : E ⧸ p) = x
Full source 
@[simp]
theorem mk_quotientEquivOfIsCompl_apply (h : IsCompl p q) (x : E ⧸ p) :
    (Quotient.mk (quotientEquivOfIsCompl p q h x) : E ⧸ p) = x :=
  (quotientEquivOfIsCompl p q h).symm_apply_apply x
Quotient Map and Linear Equivalence Identity for Complementary Submodules
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be submodules of $E$ that are complements (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x$ in the quotient module $E ⧸ p$, the equivalence class of the image of $x$ under the linear equivalence $\text{quotientEquivOfIsCompl}\ p\ q\ h$ (which maps $E ⧸ p$ to $q$) is equal to $x$ itself. In other words, the composition of the quotient map with the inverse of the linear equivalence acts as the identity on $E ⧸ p$.
Submodule.prodEquivOfIsCompl definition
(h : IsCompl p q) : (p × q) ≃ₗ[R] E
Full source 
/-- 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`. -/
def prodEquivOfIsCompl (h : IsCompl p q) : (p × q) ≃ₗ[R] E := by
  apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)
  constructor
  · rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]
    rw [range_subtype, range_subtype]
    exact h.1
  · rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
Linear isomorphism between complementary submodules and their direct sum
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R$, the direct product $p \times q$ is linearly isomorphic to $E$ via the map $(x, y) \mapsto x + y$.
Submodule.coe_prodEquivOfIsCompl theorem
(h : IsCompl p q) : (prodEquivOfIsCompl p q h : p × q →ₗ[R] E) = p.subtype.coprod q.subtype
Full source 
@[simp]
theorem coe_prodEquivOfIsCompl (h : IsCompl p q) :
    (prodEquivOfIsCompl p q h : p × qp × q →ₗ[R] E) = p.subtype.coprod q.subtype := rfl
Linear isomorphism between complementary submodules equals coproduct of inclusions
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R$, the linear isomorphism $\text{prodEquivOfIsCompl}\ p\ q\ h \colon p \times q \to E$ is equal to the coproduct of the inclusion maps $p \hookrightarrow E$ and $q \hookrightarrow E$, i.e., $(x, y) \mapsto x + y$.
Submodule.coe_prodEquivOfIsCompl' theorem
(h : IsCompl p q) (x : p × q) : prodEquivOfIsCompl p q h x = x.1 + x.2
Full source 
@[simp]
theorem coe_prodEquivOfIsCompl' (h : IsCompl p q) (x : p × q) :
    prodEquivOfIsCompl p q h x = x.1 + x.2 := rfl
Linear isomorphism decomposition for complementary submodules: $\text{prodEquivOfIsCompl}(x_1, x_2) = x_1 + x_2$
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R$, and any element $(x_1, x_2) \in p \times q$, the linear isomorphism $\text{prodEquivOfIsCompl}\ p\ q\ h$ maps $(x_1, x_2)$ to $x_1 + x_2 \in E$.
Submodule.prodEquivOfIsCompl_symm_apply_left theorem
(h : IsCompl p q) (x : p) : (prodEquivOfIsCompl p q h).symm x = (x, 0)
Full source 
@[simp]
theorem prodEquivOfIsCompl_symm_apply_left (h : IsCompl p q) (x : p) :
    (prodEquivOfIsCompl p q h).symm x = (x, 0) :=
  (prodEquivOfIsCompl p q h).symm_apply_eq.2 <| by simp
Inverse projection of left submodule element to direct product
Informal description
Let $p$ and $q$ be complementary submodules of a module $E$ over a ring $R$. For any element $x \in p$, the inverse of the linear isomorphism $\text{prodEquivOfIsCompl}\, p\, q\, h$ maps $x$ to the pair $(x, 0)$ in the direct product $p \times q$.
Submodule.prodEquivOfIsCompl_symm_apply_right theorem
(h : IsCompl p q) (x : q) : (prodEquivOfIsCompl p q h).symm x = (0, x)
Full source 
@[simp]
theorem prodEquivOfIsCompl_symm_apply_right (h : IsCompl p q) (x : q) :
    (prodEquivOfIsCompl p q h).symm x = (0, x) :=
  (prodEquivOfIsCompl p q h).symm_apply_eq.2 <| by simp
Inverse projection of complementary submodule element maps to zero in first component
Informal description
Let $p$ and $q$ be complementary submodules of a module $E$ over a ring $R$. For any element $x \in q$, the inverse of the linear isomorphism $\text{prodEquivOfIsCompl}\, p\, q\, h$ maps $x$ to the pair $(0, x) \in p \times q$.
Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero theorem
(h : IsCompl p q) {x : E} : ((prodEquivOfIsCompl p q h).symm x).1 = 0 ↔ x ∈ q
Full source 
@[simp]
theorem prodEquivOfIsCompl_symm_apply_fst_eq_zero (h : IsCompl p q) {x : E} :
    ((prodEquivOfIsCompl p q h).symm x).1 = 0 ↔ x ∈ q := by
  conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
  rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]
First Component Vanishes in Inverse Projection iff Element Belongs to Complement
Informal description
Let $p$ and $q$ be complementary submodules of an $R$-module $E$. For any $x \in E$, the first component of the inverse of the linear isomorphism $\text{prodEquivOfIsCompl}\, p\, q\, h$ evaluated at $x$ is zero if and only if $x$ belongs to $q$.
Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero theorem
(h : IsCompl p q) {x : E} : ((prodEquivOfIsCompl p q h).symm x).2 = 0 ↔ x ∈ p
Full source 
@[simp]
theorem prodEquivOfIsCompl_symm_apply_snd_eq_zero (h : IsCompl p q) {x : E} :
    ((prodEquivOfIsCompl p q h).symm x).2 = 0 ↔ x ∈ p := by
  conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
  rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]
Characterization of elements in submodule $p$ via projection to complement $q$
Informal description
Let $p$ and $q$ be complementary submodules of an $R$-module $E$. For any $x \in E$, the second component of the inverse of the isomorphism $\text{prodEquivOfIsCompl}\, p\, q\, h$ evaluated at $x$ is zero if and only if $x$ belongs to $p$.
Submodule.prodComm_trans_prodEquivOfIsCompl theorem
(h : IsCompl p q) : LinearEquiv.prodComm R q p ≪≫ₗ prodEquivOfIsCompl p q h = prodEquivOfIsCompl q p h.symm
Full source 
@[simp]
theorem prodComm_trans_prodEquivOfIsCompl (h : IsCompl p q) :
    LinearEquiv.prodCommLinearEquiv.prodComm R q p ≪≫ₗ prodEquivOfIsCompl p q h = prodEquivOfIsCompl q p h.symm :=
  LinearEquiv.ext fun _ => add_comm _ _
Compatibility of Product Swap with Complementary Submodule Isomorphism
Informal description
Let $R$ be a ring, and let $E$ be an $R$-module with complementary submodules $p$ and $q$. The composition of the linear isomorphism swapping the components of $q \times p$ with the linear isomorphism from $p \times q$ to $E$ is equal to the linear isomorphism from $q \times p$ to $E$ induced by the symmetry of complementarity.
Submodule.linearProjOfIsCompl definition
(h : IsCompl p q) : E →ₗ[R] p
Full source 
/-- Projection to a submodule along a complement.

See also `LinearMap.linearProjOfIsCompl`. -/
def linearProjOfIsCompl (h : IsCompl p q) : E →ₗ[R] p :=
  LinearMap.fstLinearMap.fst R p q ∘ₗ ↑(prodEquivOfIsCompl p q h).symm
Linear projection onto a submodule along its complement
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R$, the linear projection $\text{linearProjOfIsCompl}\ p\ q\ h$ is the unique linear map from $E$ to $p$ such that for any $x \in p$, $\text{linearProjOfIsCompl}\ p\ q\ h\ x = x$, and for any $x \in q$, $\text{linearProjOfIsCompl}\ p\ q\ h\ x = 0$. This projection is constructed as the composition of the first projection linear map $\text{LinearMap.fst}\ R\ p\ q$ with the inverse of the linear isomorphism $\text{prodEquivOfIsCompl}\ p\ q\ h$ that maps $(x, y) \in p \times q$ to $x + y \in E$.
Submodule.linearProjOfIsCompl_apply_left theorem
(h : IsCompl p q) (x : p) : linearProjOfIsCompl p q h x = x
Full source 
@[simp]
theorem linearProjOfIsCompl_apply_left (h : IsCompl p q) (x : p) :
    linearProjOfIsCompl p q h x = x := by simp [linearProjOfIsCompl]
Projection to Complementary Submodule Acts as Identity on Submodule Elements
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \sqcap q = \bot$ and $p \sqcup q = \top$). For any element $x \in p$, the linear projection $\text{linearProjOfIsCompl}\, p\, q\, h$ maps $x$ to itself, i.e., $\text{linearProjOfIsCompl}\, p\, q\, h\, x = x$.
Submodule.linearProjOfIsCompl_range theorem
(h : IsCompl p q) : range (linearProjOfIsCompl p q h) = ⊤
Full source 
@[simp]
theorem linearProjOfIsCompl_range (h : IsCompl p q) : range (linearProjOfIsCompl p q h) = ⊤ :=
  range_eq_of_proj (linearProjOfIsCompl_apply_left h)
Range of Projection onto Complementary Submodule is Entire Submodule
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). The range of the linear projection $\text{linearProjOfIsCompl}\, p\, q\, h$ from $E$ to $p$ along $q$ is the entire submodule $p$ (i.e., $\text{range}(\text{linearProjOfIsCompl}\, p\, q\, h) = p$).
Submodule.linearProjOfIsCompl_surjective theorem
(h : IsCompl p q) : Function.Surjective (linearProjOfIsCompl p q h)
Full source 
theorem linearProjOfIsCompl_surjective (h : IsCompl p q) :
    Function.Surjective (linearProjOfIsCompl p q h) :=
  range_eq_top.mp (linearProjOfIsCompl_range h)
Surjectivity of Projection onto Complementary Submodule
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). The linear projection $\text{linearProjOfIsCompl}\, p\, q\, h$ from $E$ to $p$ along $q$ is surjective.
Submodule.linearProjOfIsCompl_apply_eq_zero_iff theorem
(h : IsCompl p q) {x : E} : linearProjOfIsCompl p q h x = 0 ↔ x ∈ q
Full source 
@[simp]
theorem linearProjOfIsCompl_apply_eq_zero_iff (h : IsCompl p q) {x : E} :
    linearProjOfIsCompllinearProjOfIsCompl p q h x = 0 ↔ x ∈ q := by simp [linearProjOfIsCompl]
Projection onto $p$ along $q$ vanishes if and only if the element is in $q$
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \sqcap q = \bot$ and $p \sqcup q = \top$). For any $x \in E$, the projection $\text{linearProjOfIsCompl}\ p\ q\ h\ x$ of $x$ onto $p$ along $q$ is zero if and only if $x$ belongs to $q$.
Submodule.linearProjOfIsCompl_apply_right' theorem
(h : IsCompl p q) (x : E) (hx : x ∈ q) : linearProjOfIsCompl p q h x = 0
Full source 
theorem linearProjOfIsCompl_apply_right' (h : IsCompl p q) (x : E) (hx : x ∈ q) :
    linearProjOfIsCompl p q h x = 0 :=
  (linearProjOfIsCompl_apply_eq_zero_iff h).2 hx
Projection onto $p$ along $q$ vanishes on elements of $q$
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any $x \in E$ such that $x \in q$, the projection of $x$ onto $p$ along $q$ is zero, i.e., $\text{linearProjOfIsCompl}\ p\ q\ h\ x = 0$.
Submodule.linearProjOfIsCompl_apply_right theorem
(h : IsCompl p q) (x : q) : linearProjOfIsCompl p q h x = 0
Full source 
@[simp]
theorem linearProjOfIsCompl_apply_right (h : IsCompl p q) (x : q) :
    linearProjOfIsCompl p q h x = 0 :=
  linearProjOfIsCompl_apply_right' h x x.2
Projection onto Submodule $p$ Vanishes on Complement $q$
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x \in q$, the projection of $x$ onto $p$ along $q$ is zero, i.e., $\text{linearProjOfIsCompl}\, p\, q\, h\, x = 0$.
Submodule.linearProjOfIsCompl_ker theorem
(h : IsCompl p q) : ker (linearProjOfIsCompl p q h) = q
Full source 
@[simp]
theorem linearProjOfIsCompl_ker (h : IsCompl p q) : ker (linearProjOfIsCompl p q h) = q :=
  ext fun _ => mem_ker.trans (linearProjOfIsCompl_apply_eq_zero_iff h)
Kernel of Projection onto Submodule along Complement is the Complement Submodule
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). The kernel of the linear projection $\text{linearProjOfIsCompl}\ p\ q\ h$ from $E$ onto $p$ along $q$ is equal to $q$.
Submodule.linearProjOfIsCompl_comp_subtype theorem
(h : IsCompl p q) : (linearProjOfIsCompl p q h).comp p.subtype = LinearMap.id
Full source 
theorem linearProjOfIsCompl_comp_subtype (h : IsCompl p q) :
    (linearProjOfIsCompl p q h).comp p.subtype = LinearMap.id :=
  LinearMap.ext <| linearProjOfIsCompl_apply_left h
Projection onto Complementary Submodule Acts as Identity on Submodule Elements
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). The composition of the linear projection $\text{linearProjOfIsCompl}\, p\, q\, h$ onto $p$ along $q$ with the inclusion map $p \hookrightarrow E$ is equal to the identity map on $p$. In other words, for any $x \in p$, we have $\text{linearProjOfIsCompl}\, p\, q\, h\, x = x$.
Submodule.linearProjOfIsCompl_idempotent theorem
(h : IsCompl p q) (x : E) : linearProjOfIsCompl p q h (linearProjOfIsCompl p q h x) = linearProjOfIsCompl p q h x
Full source 
theorem linearProjOfIsCompl_idempotent (h : IsCompl p q) (x : E) :
    linearProjOfIsCompl p q h (linearProjOfIsCompl p q h x) = linearProjOfIsCompl p q h x :=
  linearProjOfIsCompl_apply_left h _
Idempotence of Projection onto Complementary Submodule
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x \in E$, the linear projection $\pi_p : E \to p$ along $q$ satisfies $\pi_p(\pi_p(x)) = \pi_p(x)$.
Submodule.existsUnique_add_of_isCompl_prod theorem
(hc : IsCompl p q) (x : E) : ∃! u : p × q, (u.fst : E) + u.snd = x
Full source 
theorem existsUnique_add_of_isCompl_prod (hc : IsCompl p q) (x : E) :
    ∃! u : p × q, (u.fst : E) + u.snd = x :=
  (prodEquivOfIsCompl _ _ hc).toEquiv.bijective.existsUnique _
Unique Decomposition into Complementary Submodules
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be submodules of $E$ that are complements (i.e., $p \sqcap q = \bot$ and $p \sqcup q = \top$ in the lattice of submodules). Then for any element $x \in E$, there exists a unique pair $(u, v) \in p \times q$ such that $u + v = x$.
Submodule.existsUnique_add_of_isCompl theorem
(hc : IsCompl p q) (x : E) : ∃ (u : p) (v : q), (u : E) + v = x ∧ ∀ (r : p) (s : q), (r : E) + s = x → r = u ∧ s = v
Full source 
theorem existsUnique_add_of_isCompl (hc : IsCompl p q) (x : E) :
    ∃ (u : p) (v : q), (u : E) + v = x ∧ ∀ (r : p) (s : q), (r : E) + s = x → r = u ∧ s = v :=
  let ⟨u, hu₁, hu₂⟩ := existsUnique_add_of_isCompl_prod hc x
  ⟨u.1, u.2, hu₁, fun r s hrs => Prod.eq_iff_fst_eq_snd_eq.1 (hu₂ ⟨r, s⟩ hrs)⟩
Unique Decomposition into Complementary Submodules
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any element $x \in E$, there exist unique elements $u \in p$ and $v \in q$ such that $u + v = x$. Moreover, if $r \in p$ and $s \in q$ satisfy $r + s = x$, then $r = u$ and $s = v$.
Submodule.linear_proj_add_linearProjOfIsCompl_eq_self theorem
(hpq : IsCompl p q) (x : E) : (p.linearProjOfIsCompl q hpq x + q.linearProjOfIsCompl p hpq.symm x : E) = x
Full source 
theorem linear_proj_add_linearProjOfIsCompl_eq_self (hpq : IsCompl p q) (x : E) :
    (p.linearProjOfIsCompl q hpq x + q.linearProjOfIsCompl p hpq.symm x : E) = x := by
  dsimp only [linearProjOfIsCompl]
  rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
  exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x
Decomposition via Complementary Projections: $\pi_p(x) + \pi_q(x) = x$
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). For any $x \in E$, the sum of the projections of $x$ onto $p$ along $q$ and onto $q$ along $p$ equals $x$ itself, i.e., \[ \pi_p(x) + \pi_q(x) = x, \] where $\pi_p \colon E \to p$ and $\pi_q \colon E \to q$ are the linear projection maps associated with the decomposition $E = p \oplus q$.
LinearMap.linearProjOfIsCompl definition
{F : Type*} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective i) (h : IsCompl (LinearMap.range i) q) : E →ₗ[R] F
Full source 
/-- 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. -/
def linearProjOfIsCompl {F : Type*} [AddCommGroup F] [Module R F]
    (i : F →ₗ[R] E) (hi : Function.Injective i)
    (h : IsCompl (LinearMap.range i) q) : E →ₗ[R] F :=
  (LinearEquiv.ofInjective i hi).symm ∘ₗ (LinearMap.range i).linearProjOfIsCompl q h
Linear projection onto the domain of an injective linear map along a complementary submodule
Informal description
Given an injective linear map \( i : F \to E \) between modules over a ring \( R \), and a submodule \( q \) of \( E \) that is complementary to the range of \( i \), the linear projection \( \text{linearProjOfIsCompl} \) is the unique linear map from \( E \) to \( F \) such that for any \( x \) in the range of \( i \), \( \text{linearProjOfIsCompl}\ q\ i\ \text{hi}\ h\ (i\ x) = x \), and for any \( x \in q \), \( \text{linearProjOfIsCompl}\ q\ i\ \text{hi}\ h\ x = 0 \). This projection is constructed as the composition of the inverse of the linear equivalence \( \text{LinearEquiv.ofInjective}\ i\ \text{hi} \) with the linear projection \( \text{linearProjOfIsCompl} \) onto the range of \( i \) along \( q \).
LinearMap.linearProjOfIsCompl_apply_left theorem
{F : Type*} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective i) (h : IsCompl (LinearMap.range i) q) (x : F) : linearProjOfIsCompl q i hi h (i x) = x
Full source 
@[simp]
theorem linearProjOfIsCompl_apply_left {F : Type*} [AddCommGroup F] [Module R F]
    (i : F →ₗ[R] E) (hi : Function.Injective i)
    (h : IsCompl (LinearMap.range i) q) (x : F) :
    linearProjOfIsCompl q i hi h (i x) = x := by
  let ix : LinearMap.range i := ⟨i x, mem_range_self i x⟩
  change linearProjOfIsCompl q i hi h ix = x
  rw [linearProjOfIsCompl, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.symm_apply_eq, Submodule.linearProjOfIsCompl_apply_left, Subtype.ext_iff,
    LinearEquiv.ofInjective_apply]
Projection along complement acts as inverse on range: $\pi_q \circ i = \text{id}_F$
Informal description
Let $E$ and $F$ be modules over a ring $R$, and let $i : F \to E$ be an injective linear map. Given a submodule $q$ of $E$ that is complementary to the range of $i$ (i.e., $\text{range}(i) \sqcap q = \bot$ and $\text{range}(i) \sqcup q = \top$), the linear projection $\pi_q : E \to F$ along $q$ satisfies $\pi_q(i(x)) = x$ for all $x \in F$.
LinearMap.ofIsCompl definition
{p q : Submodule R E} (h : IsCompl p q) (φ : p →ₗ[R] F) (ψ : q →ₗ[R] F) : E →ₗ[R] F
Full source 
/-- Given linear maps `φ` and `ψ` from complement submodules, `LinearMap.ofIsCompl` is
the induced linear map over the entire module. -/
def ofIsCompl {p q : Submodule R E} (h : IsCompl p q) (φ : p →ₗ[R] F) (ψ : q →ₗ[R] F) : E →ₗ[R] F :=
  LinearMap.coprodLinearMap.coprod φ ψ ∘ₗ ↑(Submodule.prodEquivOfIsCompl _ _ h).symm
Linear map induced by complementary submodules
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R$, and linear maps $\phi \colon p \to F$ and $\psi \colon q \to F$ to another module $F$, the linear map $\operatorname{ofIsCompl} h \phi \psi \colon E \to F$ is defined as the composition of the coproduct of $\phi$ and $\psi$ with the inverse of the linear isomorphism between $E$ and the direct product $p \times q$ induced by the complementarity of $p$ and $q$. In other words, for any $x \in E$, we have $(\operatorname{ofIsCompl} h \phi \psi)(x) = \phi(u) + \psi(v)$, where $x = u + v$ is the unique decomposition of $x$ into components $u \in p$ and $v \in q$.
LinearMap.ofIsCompl_left_apply theorem
(h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) : ofIsCompl h φ ψ (u : E) = φ u
Full source 
@[simp]
theorem ofIsCompl_left_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
    ofIsCompl h φ ψ (u : E) = φ u := by simp [ofIsCompl]
Action of Linear Map from Complementary Submodules on Left Submodule Elements
Informal description
Let $p$ and $q$ be complementary submodules of a module $E$ over a ring $R$, and let $\phi \colon p \to F$ and $\psi \colon q \to F$ be linear maps to another module $F$. For any element $u \in p$, the linear map $\operatorname{ofIsCompl}\, h\, \phi\, \psi$ satisfies $\operatorname{ofIsCompl}\, h\, \phi\, \psi\, u = \phi(u)$.
LinearMap.ofIsCompl_right_apply theorem
(h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) : ofIsCompl h φ ψ (v : E) = ψ v
Full source 
@[simp]
theorem ofIsCompl_right_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) :
    ofIsCompl h φ ψ (v : E) = ψ v := by simp [ofIsCompl]
Action of Linear Map on Complementary Submodule's Right Component
Informal description
Let $E$ be a module over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $E = p \oplus q$). Given linear maps $\phi \colon p \to F$ and $\psi \colon q \to F$ to another module $F$, for any element $v \in q$, the linear map $\operatorname{ofIsCompl}\, h\, \phi\, \psi$ satisfies $\operatorname{ofIsCompl}\, h\, \phi\, \psi\, v = \psi v$.
LinearMap.ofIsCompl_eq theorem
(h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : ∀ u, φ u = χ u) (hψ : ∀ u, ψ u = χ u) : ofIsCompl h φ ψ = χ
Full source 
theorem ofIsCompl_eq (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F}
    (hφ : ∀ u, φ u = χ u) (hψ : ∀ u, ψ u = χ u) : ofIsCompl h φ ψ = χ := by
  ext x
  obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
  simp [ofIsCompl, hφ, hψ]
Uniqueness of Linear Map Extension on Complementary Submodules
Informal description
Let $E$ and $F$ be modules over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $E = p \oplus q$). Given linear maps $\phi \colon p \to F$, $\psi \colon q \to F$, and $\chi \colon E \to F$ such that $\phi(u) = \chi(u)$ for all $u \in p$ and $\psi(v) = \chi(v)$ for all $v \in q$, the linear map $\operatorname{ofIsCompl}\, h\, \phi\, \psi$ constructed from the complementary submodules is equal to $\chi$.
LinearMap.ofIsCompl_eq' theorem
(h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = χ.comp p.subtype) (hψ : ψ = χ.comp q.subtype) : ofIsCompl h φ ψ = χ
Full source 
theorem ofIsCompl_eq' (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F}
    (hφ : φ = χ.comp p.subtype) (hψ : ψ = χ.comp q.subtype) : ofIsCompl h φ ψ = χ :=
  ofIsCompl_eq h (fun _ => hφ.symm ▸ rfl) fun _ => hψ.symm ▸ rfl
Uniqueness of Linear Map Extension via Complementary Submodules' Inclusions
Informal description
Let $E$ and $F$ be modules over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $E = p \oplus q$). Given linear maps $\phi \colon p \to F$, $\psi \colon q \to F$, and $\chi \colon E \to F$ such that $\phi = \chi \circ \iota_p$ and $\psi = \chi \circ \iota_q$, where $\iota_p \colon p \hookrightarrow E$ and $\iota_q \colon q \hookrightarrow E$ are the inclusion maps, then the linear map $\operatorname{ofIsCompl}\, h\, \phi\, \psi$ is equal to $\chi$.
LinearMap.ofIsCompl_zero theorem
(h : IsCompl p q) : (ofIsCompl h 0 0 : E →ₗ[R] F) = 0
Full source 
@[simp]
theorem ofIsCompl_zero (h : IsCompl p q) : (ofIsCompl h 0 0 : E →ₗ[R] F) = 0 :=
  ofIsCompl_eq _ (fun _ => rfl) fun _ => rfl
Zero Linear Map Extension on Complementary Submodules
Informal description
Let $E$ and $F$ be modules over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$. The linear map $\operatorname{ofIsCompl}\, h\, 0\, 0 \colon E \to F$ constructed from the zero maps on $p$ and $q$ is equal to the zero map on $E$.
LinearMap.ofIsCompl_add theorem
(h : IsCompl p q) {φ₁ φ₂ : p →ₗ[R] F} {ψ₁ ψ₂ : q →ₗ[R] F} : ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂
Full source 
@[simp]
theorem ofIsCompl_add (h : IsCompl p q) {φ₁ φ₂ : p →ₗ[R] F} {ψ₁ ψ₂ : q →ₗ[R] F} :
    ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂ :=
  ofIsCompl_eq _ (by simp) (by simp)
Additivity of Linear Map Construction on Complementary Submodules
Informal description
Let $E$ and $F$ be modules over a ring $R$, and let $p$ and $q$ be complementary submodules of $E$ (i.e., $E = p \oplus q$). For any linear maps $\phi_1, \phi_2 \colon p \to F$ and $\psi_1, \psi_2 \colon q \to F$, the linear map constructed from the sum of these maps satisfies: \[ \operatorname{ofIsCompl}\, h\, (\phi_1 + \phi_2)\, (\psi_1 + \psi_2) = \operatorname{ofIsCompl}\, h\, \phi_1\, \psi_1 + \operatorname{ofIsCompl}\, h\, \phi_2\, \psi_2 \]
LinearMap.ofIsCompl_smul theorem
{R : Type*} [CommRing R] {E : Type*} [AddCommGroup E] [Module R E] {F : Type*} [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 φ ψ
Full source 
@[simp]
theorem ofIsCompl_smul {R : Type*} [CommRing R] {E : Type*} [AddCommGroup E] [Module R E]
    {F : Type*} [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 φ ψ :=
  ofIsCompl_eq _ (by simp) (by simp)
Scalar Multiplication Commutes with Linear Map Construction on Complementary Submodules
Informal description
Let $R$ be a commutative ring, and let $E$ and $F$ be modules over $R$ with $E$ being an additive commutative group. Let $p$ and $q$ be complementary submodules of $E$ (i.e., $E = p \oplus q$). For any linear maps $\phi \colon p \to F$ and $\psi \colon q \to F$, and any scalar $c \in R$, the linear map constructed from the scalar multiples $c \cdot \phi$ and $c \cdot \psi$ via $\operatorname{ofIsCompl}$ is equal to the scalar multiple $c$ applied to the linear map constructed from $\phi$ and $\psi$: \[ \operatorname{ofIsCompl}\, h\, (c \cdot \phi)\, (c \cdot \psi) = c \cdot \operatorname{ofIsCompl}\, h\, \phi\, \psi. \]
LinearMap.ofIsComplProd definition
{p q : Submodule R₁ E} (h : IsCompl p q) : (p →ₗ[R₁] F) × (q →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F
Full source 
/-- The linear map from `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` to `E →ₗ[R₁] F`. -/
def ofIsComplProd {p q : Submodule R₁ E} (h : IsCompl p q) :
    (p →ₗ[R₁] F) × (q →ₗ[R₁] F)(p →ₗ[R₁] F) × (q →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F where
  toFun φ := ofIsCompl h φ.1 φ.2
  map_add' := by intro φ ψ; rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]
  map_smul' := by intro c φ; simp [Prod.smul_snd, Prod.smul_fst, ofIsCompl_smul]
Linear map from pairs of linear maps on complementary submodules
Informal description
Given two complementary submodules \( p \) and \( q \) of a module \( E \) over a ring \( R_1 \), the linear map \( \operatorname{ofIsComplProd} \) sends a pair of linear maps \( (\phi, \psi) \in (p \to_{R_1} F) \times (q \to_{R_1} F) \) to the linear map \( E \to_{R_1} F \) defined by \( \operatorname{ofIsCompl} h \phi \psi \). This map is linear in both components, meaning it preserves addition and scalar multiplication: - For any \( \phi_1, \phi_2 \in p \to_{R_1} F \) and \( \psi_1, \psi_2 \in q \to_{R_1} F \), we have \( \operatorname{ofIsComplProd} h (\phi_1 + \phi_2, \psi_1 + \psi_2) = \operatorname{ofIsComplProd} h (\phi_1, \psi_1) + \operatorname{ofIsComplProd} h (\phi_2, \psi_2) \). - For any scalar \( c \in R_1 \) and any \( \phi \in p \to_{R_1} F \), \( \psi \in q \to_{R_1} F \), we have \( \operatorname{ofIsComplProd} h (c \cdot \phi, c \cdot \psi) = c \cdot \operatorname{ofIsComplProd} h (\phi, \psi) \).
LinearMap.ofIsComplProd_apply theorem
{p q : Submodule R₁ E} (h : IsCompl p q) (φ : (p →ₗ[R₁] F) × (q →ₗ[R₁] F)) : ofIsComplProd h φ = ofIsCompl h φ.1 φ.2
Full source 
@[simp]
theorem ofIsComplProd_apply {p q : Submodule R₁ E} (h : IsCompl p q)
    (φ : (p →ₗ[R₁] F) × (q →ₗ[R₁] F)) : ofIsComplProd h φ = ofIsCompl h φ.1 φ.2 :=
  rfl
Application of Linear Map Construction from Complementary Submodules
Informal description
Given two complementary submodules $p$ and $q$ of a module $E$ over a ring $R_1$, and a pair of linear maps $(\phi, \psi) \in (p \to_{R_1} F) \times (q \to_{R_1} F)$, the linear map $\operatorname{ofIsComplProd} h (\phi, \psi)$ is equal to the linear map $\operatorname{ofIsCompl} h \phi \psi$ constructed from the individual components $\phi$ and $\psi$.
LinearMap.ofIsComplProdEquiv definition
{p q : Submodule R₁ E} (h : IsCompl p q) : ((p →ₗ[R₁] F) × (q →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F
Full source 
/-- The natural linear equivalence between `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` and `E →ₗ[R₁] F`. -/
def ofIsComplProdEquiv {p q : Submodule R₁ E} (h : IsCompl p q) :
    ((p →ₗ[R₁] F) × (q →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F :=
  { ofIsComplProd h with
    invFun := fun φ => ⟨φ.domRestrict p, φ.domRestrict q⟩
    left_inv := fun φ ↦ by
      ext x
      · exact ofIsCompl_left_apply h x
      · exact ofIsCompl_right_apply h x
    right_inv := fun φ ↦ by
      ext x
      obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x
      rw [← hab]; simp }
Linear equivalence between product of linear maps on complementary submodules and linear maps on the whole space
Informal description
Given two complementary submodules \( p \) and \( q \) of a module \( E \) over a ring \( R_1 \), there is a natural linear equivalence between the product space of linear maps \( (p \to_{R_1} F) \times (q \to_{R_1} F) \) and the space of linear maps \( E \to_{R_1} F \). This equivalence is constructed as follows: - The forward map takes a pair of linear maps \( (\phi, \psi) \) and combines them into a single linear map on \( E \) using the decomposition \( E = p \oplus q \). - The inverse map restricts a given linear map \( \varphi : E \to F \) to the submodules \( p \) and \( q \), returning the pair \( (\varphi|_p, \varphi|_q) \). The equivalence preserves the linear structure, meaning it respects addition and scalar multiplication in both directions.
LinearMap.linearProjOfIsCompl_of_proj theorem
(f : E →ₗ[R] p) (hf : ∀ x : p, f x = x) : p.linearProjOfIsCompl (ker f) (isCompl_of_proj hf) = f
Full source 
@[simp, nolint simpNF] -- Porting note: linter claims that LHS doesn't simplify, but it does
-- It seems the side condition `hf` is not applied by `simpNF`.
theorem linearProjOfIsCompl_of_proj (f : E →ₗ[R] p) (hf : ∀ x : p, f x = x) :
    p.linearProjOfIsCompl (ker f) (isCompl_of_proj hf) = f := by
  ext x
  have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
  rcases mem_sup'.1 this with ⟨x, y, rfl⟩
  simp [hf]
Projection onto Submodule Equals Given Map When Acting as Identity on Submodule
Informal description
Let $E$ be a module over a ring $R$ and $p$ a submodule of $E$. For any linear map $f: E \to p$ such that $f(x) = x$ for all $x \in p$, the projection map $\text{linearProjOfIsCompl}\, p\, (\ker f)\, h$ (where $h$ is the proof that $p$ and $\ker f$ are complementary) equals $f$.
LinearMap.equivProdOfSurjectiveOfIsCompl definition
(f : E →ₗ[R] F) (g : E →ₗ[R] G) (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) : E ≃ₗ[R] F × G
Full source 
/-- 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`. -/
def equivProdOfSurjectiveOfIsCompl (f : E →ₗ[R] F) (g : E →ₗ[R] G) (hf : range f = ⊤)
    (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) : E ≃ₗ[R] F × G :=
  LinearEquiv.ofBijective (f.prod g)
    ⟨by simp [← ker_eq_bot, hfg.inf_eq_bot], by
      rw [← range_eq_top]
      simp [range_prod_eq hfg.sup_eq_top, *]⟩
Linear equivalence from surjective maps with complementary kernels
Informal description
Given two surjective linear maps \( f : E \to F \) and \( g : E \to G \) over a ring \( R \), if their kernels are complementary subspaces of \( E \), then the map \( x \mapsto (f(x), g(x)) \) defines a linear equivalence \( E \simeq F \times G \).
LinearMap.coe_equivProdOfSurjectiveOfIsCompl theorem
{f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) : (equivProdOfSurjectiveOfIsCompl f g hf hg hfg : E →ₗ[R] F × G) = f.prod g
Full source 
@[simp]
theorem coe_equivProdOfSurjectiveOfIsCompl {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤)
    (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) :
    (equivProdOfSurjectiveOfIsCompl f g hf hg hfg : E →ₗ[R] F × G) = f.prod g := rfl
Linear equivalence from surjective maps with complementary kernels equals product map
Informal description
Given two surjective linear maps \( f : E \to F \) and \( g : E \to G \) over a ring \( R \) with complementary kernels, the linear equivalence \( E \simeq F \times G \) induced by \( f \) and \( g \) is equal to the product map \( f \times g \), i.e., \( \text{equivProdOfSurjectiveOfIsCompl}\,f\,g\,hf\,hg\,hfg = f \times g \).
LinearMap.equivProdOfSurjectiveOfIsCompl_apply theorem
{f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) (x : E) : equivProdOfSurjectiveOfIsCompl f g hf hg hfg x = (f x, g x)
Full source 
@[simp]
theorem equivProdOfSurjectiveOfIsCompl_apply {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : range f = ⊤)
    (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) (x : E) :
    equivProdOfSurjectiveOfIsCompl f g hf hg hfg x = (f x, g x) := rfl
Application of Linear Equivalence from Surjective Maps with Complementary Kernels: \( x \mapsto (f(x), g(x)) \)
Informal description
Given two surjective linear maps \( f : E \to F \) and \( g : E \to G \) over a ring \( R \), if their kernels are complementary subspaces of \( E \), then for any \( x \in E \), the linear equivalence \( \text{equivProdOfSurjectiveOfIsCompl}\,f\,g\,hf\,hg\,hfg \) maps \( x \) to the pair \((f(x), g(x))\).
Submodule.isComplEquivProj definition
: { q // IsCompl p q } ≃ { f : E →ₗ[R] p // ∀ x : p, f x = x }
Full source 
/-- Equivalence between submodules `q` such that `IsCompl p q` and linear maps `f : E →ₗ[R] p`
such that `∀ x : p, f x = x`. -/
def isComplEquivProj : { q // IsCompl p q }{ q // IsCompl p q } ≃ { f : E →ₗ[R] p // ∀ x : p, f x = x } where
  toFun q := ⟨linearProjOfIsCompl p q q.2, linearProjOfIsCompl_apply_left q.2⟩
  invFun f := ⟨ker (f : E →ₗ[R] p), isCompl_of_proj f.2⟩
  left_inv := fun ⟨q, hq⟩ => by simp only [linearProjOfIsCompl_ker, Subtype.coe_mk]
  right_inv := fun ⟨f, hf⟩ => Subtype.eq <| f.linearProjOfIsCompl_of_proj hf
Equivalence between complement submodules and projection maps
Informal description
The equivalence `Submodule.isComplEquivProj p` establishes a bijection between the set of submodules `q` that are complements to `p` (i.e., `IsCompl p q`) and the set of linear maps `f : E →ₗ[R] p` that act as the identity on `p` (i.e., `∀ x ∈ p, f x = x`). More precisely: - The forward direction maps a complement submodule `q` to the linear projection onto `p` along `q`. - The backward direction maps a projection map `f` to its kernel, which is a complement to `p`.
Submodule.coe_isComplEquivProj_apply theorem
(q : { q // IsCompl p q }) : (p.isComplEquivProj q : E →ₗ[R] p) = linearProjOfIsCompl p q q.2
Full source 
@[simp]
theorem coe_isComplEquivProj_apply (q : { q // IsCompl p q }) :
    (p.isComplEquivProj q : E →ₗ[R] p) = linearProjOfIsCompl p q q.2 := rfl
Equivalence Application Yields Projection Map
Informal description
For any submodule $q$ that is a complement to $p$ (i.e., $\text{IsCompl}\ p\ q$), the linear map obtained by applying the equivalence $\text{isComplEquivProj}\ p$ to $q$ is equal to the linear projection $\text{linearProjOfIsCompl}\ p\ q\ h$, where $h$ is the proof that $q$ is a complement to $p$.
Submodule.coe_isComplEquivProj_symm_apply theorem
(f : { f : E →ₗ[R] p // ∀ x : p, f x = x }) : (p.isComplEquivProj.symm f : Submodule R E) = ker (f : E →ₗ[R] p)
Full source 
@[simp]
theorem coe_isComplEquivProj_symm_apply (f : { f : E →ₗ[R] p // ∀ x : p, f x = x }) :
    (p.isComplEquivProj.symm f : Submodule R E) = ker (f : E →ₗ[R] p) := rfl
Kernel of Projection is Complement Submodule
Informal description
For any linear map $f \colon E \to p$ that acts as the identity on the submodule $p$, the kernel of $f$ is the complement submodule corresponding to $f$ under the equivalence `Submodule.isComplEquivProj p`. In other words, if $f$ is a projection onto $p$, then $\ker f$ is the unique submodule $q$ such that $p$ and $q$ are complements.
Submodule.isIdempotentElemEquiv definition
: { f : Module.End R E // IsIdempotentElem f ∧ range f = p } ≃ { f : E →ₗ[R] p // ∀ x : p, f x = x }
Full source 
/-- 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. -/
@[simps] def isIdempotentElemEquiv :
    { f : Module.End R E // IsIdempotentElem f ∧ range f = p }{ f : Module.End R E // IsIdempotentElem f ∧ range f = p } ≃
    { f : E →ₗ[R] p // ∀ x : p, f x = x } where
  toFun f := ⟨f.1.codRestrict _ fun x ↦ by simp_rw [← f.2.2]; exact mem_range_self f.1 x,
    fun ⟨x, hx⟩ ↦ Subtype.ext <| by
      obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
      exact DFunLike.congr_fun f.2.1 x⟩
  invFun f := ⟨p.subtype ∘ₗ f.1, LinearMap.ext fun x ↦ by simp [f.2], le_antisymm
    ((range_comp_le_range _ _).trans_eq p.range_subtype)
    fun x hx ↦ ⟨x, Subtype.ext_iff.1 <| f.2 ⟨x, hx⟩⟩⟩
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between idempotent endomorphisms and identity-preserving projections
Informal description
The equivalence between idempotent endomorphisms of a module $E$ with range equal to a submodule $p$ and linear maps from $E$ to $p$ that restrict to the identity on $p$. More precisely: - Given an idempotent endomorphism $f$ of $E$ (i.e., $f \circ f = f$) with range $p$, the corresponding linear map is the restriction of $f$ to $p$. - Conversely, given a linear map $g : E \to p$ that acts as the identity on $p$, the corresponding endomorphism is the composition of $g$ with the inclusion map $p \hookrightarrow E$. This establishes a bijective correspondence between these two types of maps.
LinearMap.IsProj structure
{F : Type*} [FunLike F M M] (f : F)
Full source 
/--
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`.
-/
structure IsProj {F : Type*} [FunLike F M M] (f : F) : Prop where
  map_mem : ∀ x, f x ∈ m
  map_id : ∀ x ∈ m, f x = x
Projection onto a Submodule
Informal description
A linear endomorphism \( f \) of a module \( M \) is called a projection onto a submodule \( p \) if it maps every element of \( M \) to \( p \) and acts as the identity on \( p \). More generally, this definition applies to any function-like type \( F \) (not just linear maps), allowing it to be used with types such as continuous linear maps or matrices.
LinearMap.isProj_iff_isIdempotentElem theorem
(f : M →ₗ[S] M) : (∃ p : Submodule S M, IsProj p f) ↔ IsIdempotentElem f
Full source 
theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) :
    (∃ p : Submodule S M, IsProj p f) ↔ IsIdempotentElem f := by
  constructor
  · intro ⟨p, hp⟩
    ext x
    exact hp.map_id (f x) (hp.map_mem x)
  · intro h
    use range f
    constructor
    · intro x
      exact mem_range_self f x
    · intro x hx
      obtain ⟨y, hy⟩ := mem_range.1 hx
      rw [← hy, ← Module.End.mul_apply, h]
Projection Characterization: $f$ is a projection if and only if $f$ is idempotent
Informal description
A linear endomorphism $f \colon M \to M$ over a semiring $S$ is a projection onto some submodule $p$ of $M$ if and only if $f$ is idempotent, i.e., $f \circ f = f$.
LinearMap.IsProj.codRestrict definition
{f : M →ₗ[S] M} (h : IsProj m f) : M →ₗ[S] m
Full source 
/-- Restriction of the codomain of a projection of onto a subspace `p` to `p` instead of the whole
space.
-/
def codRestrict {f : M →ₗ[S] M} (h : IsProj m f) : M →ₗ[S] m :=
  f.codRestrict m h.map_mem
Restriction of a projection map to its image submodule
Informal description
Given a linear endomorphism \( f \) of a module \( M \) over a semiring \( S \) that is a projection onto a submodule \( m \) (i.e., \( f \) maps every element of \( M \) to \( m \) and acts as the identity on \( m \)), the function restricts the codomain of \( f \) to \( m \), yielding a linear map from \( M \) to \( m \).
LinearMap.IsProj.codRestrict_apply theorem
{f : M →ₗ[S] M} (h : IsProj m f) (x : M) : ↑(h.codRestrict x) = f x
Full source 
@[simp]
theorem codRestrict_apply {f : M →ₗ[S] M} (h : IsProj m f) (x : M) : ↑(h.codRestrict x) = f x :=
  f.codRestrict_apply m x
Codomain-Restricted Projection Preserves Action on Elements
Informal description
Let $f : M \to M$ be a linear projection onto a submodule $m$ of $M$ over a semiring $S$. For any $x \in M$, the image of $x$ under the codomain-restricted projection $h.\text{codRestrict} : M \to m$ equals $f(x)$ when viewed in $M$, i.e., $h.\text{codRestrict}(x) = f(x)$ where the left-hand side is implicitly coerced from $m$ back to $M$.
LinearMap.IsProj.codRestrict_apply_cod theorem
{f : M →ₗ[S] M} (h : IsProj m f) (x : m) : h.codRestrict x = x
Full source 
@[simp]
theorem codRestrict_apply_cod {f : M →ₗ[S] M} (h : IsProj m f) (x : m) : h.codRestrict x = x := by
  ext
  rw [codRestrict_apply]
  exact h.map_id x x.2
Identity Action of Codomain-Restricted Projection on Submodule Elements
Informal description
Let $f : M \to M$ be a linear projection onto a submodule $m$ of $M$ over a semiring $S$. For any element $x \in m$, the codomain-restricted projection $h.\text{codRestrict}$ acts as the identity on $x$, i.e., $h.\text{codRestrict}(x) = x$.
LinearMap.IsProj.codRestrict_ker theorem
{f : M →ₗ[S] M} (h : IsProj m f) : ker h.codRestrict = ker f
Full source 
theorem codRestrict_ker {f : M →ₗ[S] M} (h : IsProj m f) : ker h.codRestrict = ker f :=
  f.ker_codRestrict m _
Kernel Equality for Codomain-Restricted Projection
Informal description
For any linear endomorphism $f$ of a module $M$ over a semiring $S$ that is a projection onto a submodule $m$, the kernel of the codomain-restricted projection $h.\text{codRestrict}$ is equal to the kernel of $f$. That is, $\ker(h.\text{codRestrict}) = \ker f$.
LinearMap.IsProj.isCompl theorem
{f : E →ₗ[R] E} (h : IsProj p f) : IsCompl p (ker f)
Full source 
theorem isCompl {f : E →ₗ[R] E} (h : IsProj p f) : IsCompl p (ker f) := by
  rw [← codRestrict_ker]
  exact isCompl_of_proj h.codRestrict_apply_cod
Complementarity of Submodule and Kernel under Linear Projection
Informal description
Let $E$ be a module over a ring $R$ and $p$ be a submodule of $E$. For any linear projection $f: E \to E$ onto $p$ (i.e., $f$ maps $E$ to $p$ and acts as the identity on $p$), the submodule $p$ and the kernel of $f$ are complementary. That is, $p \sqcap \ker f = \bot$ and $p \sqcup \ker f = \top$.