# mathlib3documentation

analysis.inner_product_space.orthogonal

# Orthogonal complements of submodules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.inner_product_space.projection.

See also bilin_form.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.is_ortho, is denoted by U ⟂ V. Note this is not the same unicode symbol as ⊥ (has_bot).

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

The subspace of vectors orthogonal to a given subspace.

Equations
Instances for ↥submodule.orthogonal
theorem submodule.mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) (v : E) :
v K (u : E), u K = 0

When a vector is in Kᗮ.

theorem submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) (v : E) :
v K (u : E), u K = 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} [is_R_or_C 𝕜] [ E] {K : E} {u v : E} (hu : u K) (hv : v K) :
= 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} [is_R_or_C 𝕜] [ E] {K : E} {u v : E} (hu : u K) (hv : v K) :
= 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} [is_R_or_C 𝕜] [ E] {u v : E} :
v {u}) = 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} [is_R_or_C 𝕜] [ E] {u v : E} :
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} [is_R_or_C 𝕜] [ E] {K : E} {x y : E} (h : (v : K), ) :
x - y K
theorem submodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {K : E} {x y : E} (h : (v : K), ) :
x - y K
theorem submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) :

K and Kᗮ have trivial intersection.

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

K and Kᗮ have trivial intersection.

theorem submodule.orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) :

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.is_closed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) :

The orthogonal complement of any submodule K is closed.

@[protected, instance]
def submodule.orthogonal.complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E)  :

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

theorem submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [ E] :

orthogonal gives a galois_connection between submodule 𝕜 E and its order_dual.

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

orthogonal reverses the ≤ ordering of two subspaces.

theorem submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {K₁ K₂ : E} (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} [is_R_or_C 𝕜] [ E] (K : E) :

K is contained in Kᗮᗮ.

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

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

theorem submodule.infi_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} (K : ι E) :
( (i : ι), (K i)) = (supr K)

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

theorem submodule.Inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (s : set E)) :
( (K : E) (H : K s), K) = (has_Sup.Sup 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} [is_R_or_C 𝕜] [ E] :
@[simp]
theorem submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] :
@[simp]
theorem submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) :
theorem submodule.orthogonal_family_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (K : E) :
(λ (b : bool), (cond b K K)) (λ (b : bool), (cond b K K).subtypeₗᵢ)
@[simp]
theorem bilin_form_of_real_inner_orthogonal {E : Type u_1} (K : E) :

### Orthogonality of submodules #

In this section we define submodule.is_ortho U V, with notation U ⟂ V.

The API roughly matches that of disjoint.

def submodule.is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (U V : E) :
Prop

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

Equations
theorem submodule.is_ortho_iff_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} :
U V U V
@[symm]
theorem submodule.is_ortho.symm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} (h : U V) :
V U
theorem submodule.is_ortho_comm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} :
U V V U
theorem submodule.symmetric_is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] :
theorem submodule.is_ortho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} (h : U V) {u v : E} (hu : u U) (hv : v V) :
= 0
theorem submodule.is_ortho_iff_inner_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} :
U V (u : E), u U (v : E), v V = 0
@[simp]
theorem submodule.is_ortho_bot_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {V : E} :
@[simp]
theorem submodule.is_ortho_bot_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U : E} :
theorem submodule.is_ortho.mono_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U₁ U₂ V : E} (hU : U₂ U₁) (h : U₁ V) :
U₂ V
theorem submodule.is_ortho.mono_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V₁ V₂ : E} (hV : V₂ V₁) (h : U V₁) :
U V₂
theorem submodule.is_ortho.mono {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U₁ V₁ U₂ V₂ : E} (hU : U₂ U₁) (hV : V₂ V₁) (h : U₁ V₁) :
U₂ V₂
@[simp]
theorem submodule.is_ortho_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U : E} :
U U U =
@[simp]
theorem submodule.is_ortho_orthogonal_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (U : E) :
U U
@[simp]
theorem submodule.is_ortho_orthogonal_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (U : E) :
U U
theorem submodule.is_ortho.le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} (h : U V) :
U V
theorem submodule.is_ortho.ge {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} (h : U V) :
V U
@[simp]
theorem submodule.is_ortho_top_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U : E} :
@[simp]
theorem submodule.is_ortho_top_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {V : E} :
theorem submodule.is_ortho.disjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V : E} (h : U V) :
V

Orthogonal submodules are disjoint.

@[simp]
theorem submodule.is_ortho_sup_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U₁ U₂ V : E} :
U₁ U₂ V U₁ V U₂ V
@[simp]
theorem submodule.is_ortho_sup_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U V₁ V₂ : E} :
U V₁ V₂ U V₁ U V₂
@[simp]
theorem submodule.is_ortho_Sup_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U : set E)} {V : E} :
V (Uᵢ : E), Uᵢ U Uᵢ V
@[simp]
theorem submodule.is_ortho_Sup_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {U : E} {V : set E)} :
U (Vᵢ : E), Vᵢ V U Vᵢ
@[simp]
theorem submodule.is_ortho_supr_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Sort u_3} {U : ι E} {V : E} :
supr U V (i : ι), U i V
@[simp]
theorem submodule.is_ortho_supr_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Sort u_3} {U : E} {V : ι E} :
U supr V (i : ι), U V i
@[simp]
theorem submodule.is_ortho_span {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {s t : set E} :
⦃u : E⦄, u s ⦃v : E⦄, v t = 0
theorem submodule.is_ortho.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (f : E →ₗᵢ[𝕜] F) {U V : E} (h : U V) :
theorem submodule.is_ortho.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (f : E →ₗᵢ[𝕜] F) {U V : F} (h : U V) :
@[simp]
theorem submodule.is_ortho.map_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (f : E ≃ₗᵢ[𝕜] F) {U V : E} :
U V
@[simp]
theorem submodule.is_ortho.comap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (f : E ≃ₗᵢ[𝕜] F) {U V : F} :
U V
theorem orthogonal_family_iff_pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} {V : ι E} :
(λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)
theorem orthogonal_family.of_pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} {V : ι E} :
(λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)

Alias of the reverse direction of orthogonal_family_iff_pairwise.

theorem orthogonal_family.pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} {V : ι E} :
(λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)

Alias of the forward direction of orthogonal_family_iff_pairwise.

theorem orthogonal_family.is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} {V : ι E} (hV : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) {i j : ι} (hij : i j) :
V i V j

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