# Orthogonal complements of submodules #

In this file, the orthogonal complement of a submodule K is defined, and basic API established. Some of the more subtle results about the orthogonal complement are delayed to Analysis.InnerProductSpace.Projection.

See also BilinForm.orthogonal for orthogonality with respect to a general bilinear form.

## Notation #

The orthogonal complement of a submodule K is denoted by Kᗮ.

The proposition that two submodules are orthogonal, Submodule.IsOrtho, is denoted by U ⟂ V. Note this is not the same unicode symbol as ⊥ (Bot).

def Submodule.orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :

The subspace of vectors orthogonal to a given subspace.

Equations
• K = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {v : E | uK, u, v⟫_𝕜 = 0}, add_mem' := }, zero_mem' := }, smul_mem' := }
Instances For

The subspace of vectors orthogonal to a given subspace.

Equations
Instances For
theorem Submodule.mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) (v : E) :
v K uK, u, v⟫_𝕜 = 0

When a vector is in Kᗮ.

theorem Submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) (v : E) :
v K uK, v, u⟫_𝕜 = 0

When a vector is in Kᗮ, with the inner product the other way round.

theorem Submodule.inner_right_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] {K : } {u : E} {v : E} (hu : u K) (hv : v K) :
u, v⟫_𝕜 = 0

A vector in K is orthogonal to one in Kᗮ.

theorem Submodule.inner_left_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] {K : } {u : E} {v : E} (hu : u K) (hv : v K) :
v, u⟫_𝕜 = 0

A vector in Kᗮ is orthogonal to one in K.

theorem Submodule.mem_orthogonal_singleton_iff_inner_right {𝕜 : Type u_1} {E : Type u_2} [] [] {u : E} {v : E} :
v (Submodule.span 𝕜 {u}) u, v⟫_𝕜 = 0

A vector is in (𝕜 ∙ u)ᗮ iff it is orthogonal to u.

theorem Submodule.mem_orthogonal_singleton_iff_inner_left {𝕜 : Type u_1} {E : Type u_2} [] [] {u : E} {v : E} :
v (Submodule.span 𝕜 {u}) v, u⟫_𝕜 = 0

A vector in (𝕜 ∙ u)ᗮ is orthogonal to u.

theorem Submodule.sub_mem_orthogonal_of_inner_left {𝕜 : Type u_1} {E : Type u_2} [] [] {K : } {x : E} {y : E} (h : ∀ (v : K), x, v⟫_𝕜 = y, v⟫_𝕜) :
x - y K
theorem Submodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_1} {E : Type u_2} [] [] {K : } {x : E} {y : E} (h : ∀ (v : K), v, x⟫_𝕜 = v, y⟫_𝕜) :
x - y K
theorem Submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :

K and Kᗮ have trivial intersection.

theorem Submodule.orthogonal_disjoint {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :

K and Kᗮ have trivial intersection.

theorem Submodule.orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :
K = ⨅ (v : K), LinearMap.ker (() v)

Kᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

theorem Submodule.isClosed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :

The orthogonal complement of any submodule K is closed.

instance Submodule.instOrthogonalCompleteSpace {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) [] :

In a complete space, the orthogonal complement of any submodule K is complete.

Equations
• =
theorem Submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [] [] :
GaloisConnection Submodule.orthogonal Submodule.orthogonal

orthogonal gives a GaloisConnection between Submodule 𝕜 E and its OrderDual.

theorem Submodule.orthogonal_le {𝕜 : Type u_1} {E : Type u_2} [] [] {K₁ : } {K₂ : } (h : K₁ K₂) :
K₂ K₁

orthogonal reverses the ≤ ordering of two subspaces.

theorem Submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [] [] {K₁ : } {K₂ : } (h : K₁ K₂) :
K₁ K₂

orthogonal.orthogonal preserves the ≤ ordering of two subspaces.

theorem Submodule.le_orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :

K is contained in Kᗮᗮ.

theorem Submodule.inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (K₁ : ) (K₂ : ) :
K₁ K₂ = (K₁ K₂)

The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.

theorem Submodule.iInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_4} (K : ι) :
⨅ (i : ι), (K i) = (iSup K)

The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.

theorem Submodule.sInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] (s : Set ()) :
⨅ K ∈ s, K = (sSup s)

The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.

@[simp]
theorem Submodule.top_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [] [] :
@[simp]
theorem Submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [] [] :
@[simp]
theorem Submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :
theorem Submodule.orthogonalFamily_self {𝕜 : Type u_1} {E : Type u_2} [] [] (K : ) :
OrthogonalFamily 𝕜 (fun (b : Bool) => (bif b then K else K)) fun (b : Bool) => Submodule.subtypeₗᵢ (bif b then K else K)
@[simp]
theorem bilinFormOfRealInner_orthogonal {E : Type u_4} [] (K : ) :
Submodule.orthogonalBilin K bilinFormOfRealInner = K

### Orthogonality of submodules #

In this section we define Submodule.IsOrtho U V, with notation U ⟂ V.

The API roughly matches that of Disjoint.

def Submodule.IsOrtho {𝕜 : Type u_1} {E : Type u_2} [] [] (U : ) (V : ) :

The proposition that two submodules are orthogonal. Has notation U ⟂ V.

Equations
Instances For

The proposition that two submodules are orthogonal. Has notation U ⟂ V.

Equations
Instances For
theorem Submodule.isOrtho_iff_le {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } :
U V U V
theorem Submodule.IsOrtho.symm {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } (h : U V) :
V U
theorem Submodule.isOrtho_comm {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } :
U V V U
theorem Submodule.symmetric_isOrtho {𝕜 : Type u_1} {E : Type u_2} [] [] :
Symmetric Submodule.IsOrtho
theorem Submodule.IsOrtho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } (h : U V) {u : E} {v : E} (hu : u U) (hv : v V) :
u, v⟫_𝕜 = 0
theorem Submodule.isOrtho_iff_inner_eq {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } :
U V uU, vV, u, v⟫_𝕜 = 0
@[simp]
theorem Submodule.isOrtho_bot_left {𝕜 : Type u_1} {E : Type u_2} [] [] {V : } :
@[simp]
theorem Submodule.isOrtho_bot_right {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } :
theorem Submodule.IsOrtho.mono_left {𝕜 : Type u_1} {E : Type u_2} [] [] {U₁ : } {U₂ : } {V : } (hU : U₂ U₁) (h : U₁ V) :
U₂ V
theorem Submodule.IsOrtho.mono_right {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V₁ : } {V₂ : } (hV : V₂ V₁) (h : U V₁) :
U V₂
theorem Submodule.IsOrtho.mono {𝕜 : Type u_1} {E : Type u_2} [] [] {U₁ : } {V₁ : } {U₂ : } {V₂ : } (hU : U₂ U₁) (hV : V₂ V₁) (h : U₁ V₁) :
U₂ V₂
@[simp]
theorem Submodule.isOrtho_self {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } :
U U U =
@[simp]
theorem Submodule.isOrtho_orthogonal_right {𝕜 : Type u_1} {E : Type u_2} [] [] (U : ) :
U U
@[simp]
theorem Submodule.isOrtho_orthogonal_left {𝕜 : Type u_1} {E : Type u_2} [] [] (U : ) :
U U
theorem Submodule.IsOrtho.le {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } (h : U V) :
U V
theorem Submodule.IsOrtho.ge {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } (h : U V) :
V U
@[simp]
theorem Submodule.isOrtho_top_right {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } :
@[simp]
theorem Submodule.isOrtho_top_left {𝕜 : Type u_1} {E : Type u_2} [] [] {V : } :
theorem Submodule.IsOrtho.disjoint {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : } (h : U V) :

Orthogonal submodules are disjoint.

@[simp]
theorem Submodule.isOrtho_sup_left {𝕜 : Type u_1} {E : Type u_2} [] [] {U₁ : } {U₂ : } {V : } :
U₁ U₂ V U₁ V U₂ V
@[simp]
theorem Submodule.isOrtho_sup_right {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V₁ : } {V₂ : } :
U V₁ V₂ U V₁ U V₂
@[simp]
theorem Submodule.isOrtho_sSup_left {𝕜 : Type u_1} {E : Type u_2} [] [] {U : Set ()} {V : } :
sSup U V UᵢU, Uᵢ V
@[simp]
theorem Submodule.isOrtho_sSup_right {𝕜 : Type u_1} {E : Type u_2} [] [] {U : } {V : Set ()} :
U sSup V VᵢV, U Vᵢ
@[simp]
theorem Submodule.isOrtho_iSup_left {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Sort u_4} {U : ι} {V : } :
iSup U V ∀ (i : ι), U i V
@[simp]
theorem Submodule.isOrtho_iSup_right {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Sort u_4} {U : } {V : ι} :
U iSup V ∀ (i : ι), U V i
@[simp]
theorem Submodule.isOrtho_span {𝕜 : Type u_1} {E : Type u_2} [] [] {s : Set E} {t : Set E} :
∀ ⦃u : E⦄, u s∀ ⦃v : E⦄, v tu, v⟫_𝕜 = 0
theorem Submodule.IsOrtho.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (f : E →ₗᵢ[𝕜] F) {U : } {V : } (h : U V) :
theorem Submodule.IsOrtho.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (f : E →ₗᵢ[𝕜] F) {U : } {V : } (h : U V) :
@[simp]
theorem Submodule.IsOrtho.map_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (f : E ≃ₗᵢ[𝕜] F) {U : } {V : } :
U V
@[simp]
theorem Submodule.IsOrtho.comap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (f : E ≃ₗᵢ[𝕜] F) {U : } {V : } :
U V
theorem orthogonalFamily_iff_pairwise {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_4} {V : ι} :
(OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) Pairwise ((fun (x x_1 : ) => x x_1) on V)
theorem OrthogonalFamily.of_pairwise {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_4} {V : ι} :
Pairwise ((fun (x x_1 : ) => x x_1) on V)OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)

Alias of the reverse direction of orthogonalFamily_iff_pairwise.

theorem OrthogonalFamily.pairwise {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_4} {V : ι} :
(OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i))Pairwise ((fun (x x_1 : ) => x x_1) on V)

Alias of the forward direction of orthogonalFamily_iff_pairwise.

theorem OrthogonalFamily.isOrtho {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_4} {V : ι} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) {i : ι} {j : ι} (hij : i j) :
V i V j

Two submodules in an orthogonal family with different indices are orthogonal.