# Orthogonal projections in finite-dimensional spaces #

This file contains results about orthogonal projections in finite-dimensional spaces.

## Main results #

- `Submodule.det_reflection`: The determinant of `K.reflection` is `(-1) ^ finrank 𝕜 Kᗮ`.
- `LinearIsometryEquiv.reflections_generate`: The orthogonal group of `F` is generated by reflections.

## Results that do not use finite dimensionality: #

- `OrthogonalFamily.isInternal_iff_of_isComplete`
- `OrthogonalFamily.sum_projection_of_mem_iSup`
- `OrthogonalFamily.projection_directSum_coeAddHom`
- `OrthogonalFamily.decomposition`
- `maximal_orthonormal_iff_orthogonalComplement_eq_bot`

source
@[simp]
theorem Submodule.topologicalClosure_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] :
K.topologicalClosure = K
source
@[simp]
theorem Submodule.det_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] :
LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥K ᗮ
source
@[simp]
theorem Submodule.linearEquiv_det_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] :
LinearEquiv.det K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥K ᗮ
source
theorem Submodule.finrank_add_inf_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) :
Module.finrank 𝕜 ↥K₁ + Module.finrank 𝕜 ↥(K₁ ᗮ ⊓ K₂) = Module.finrank 𝕜 ↥K₂

Given a finite-dimensional subspace `K₂`, and a subspace `K₁` contained in it, the dimensions of `K₁` and the intersection of its orthogonal subspace with `K₂` add to that of `K₂`.

source
theorem Submodule.finrank_add_inf_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : Module.finrank 𝕜 ↥K₁ + n = Module.finrank 𝕜 ↥K₂) :
Module.finrank 𝕜 ↥(K₁ ᗮ ⊓ K₂) = n

Given a finite-dimensional subspace `K₂`, and a subspace `K₁` contained in it, the dimensions of `K₁` and the intersection of its orthogonal subspace with `K₂` add to that of `K₂`.

source
theorem Submodule.finrank_add_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) :
Module.finrank 𝕜 ↥K + Module.finrank 𝕜 ↥K ᗮ = Module.finrank 𝕜 E

Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to that of `E`.

source
theorem Submodule.finrank_add_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {K : Submodule 𝕜 E} {n : ℕ} (h_dim : Module.finrank 𝕜 ↥K + n = Module.finrank 𝕜 E) :
Module.finrank 𝕜 ↥K ᗮ = n

Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to that of `E`.

source
theorem Submodule.finrank_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [_i : Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
Module.finrank 𝕜 ↥(span 𝕜 {v})ᗮ = n

In a finite-dimensional inner product space, the dimension of the orthogonal complement of the span of a nonzero vector is one less than the dimension of the space.

source
theorem LinearIsometryEquiv.reflections_generate_dim_aux {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ} (φ : F ≃ₗᵢ[ℝ] F) (hn : Module.finrank ℝ ↥(LinearMap.ker (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤ n) :
∃ (l : List F), l.length ≤ n ∧ φ = (List.map (fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) l).prod

An element `φ` of the orthogonal group of `F` can be factored as a product of reflections, and specifically at most as many reflections as the dimension of the complement of the fixed subspace of `φ`.

source
theorem LinearIsometryEquiv.reflections_generate_dim {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (φ : F ≃ₗᵢ[ℝ] F) :
∃ (l : List F), l.length ≤ Module.finrank ℝ F ∧ φ = (List.map (fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) l).prod

The orthogonal group of `F` is generated by reflections; specifically each element `φ` of the orthogonal group is a product of at most as many reflections as the dimension of `F`.

Special case of the Cartan–Dieudonné theorem.

source
theorem LinearIsometryEquiv.reflections_generate {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] :
Subgroup.closure (Set.range fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) = ⊤

The orthogonal group of `F` is generated by reflections.

source
theorem OrthogonalFamily.isInternal_iff_of_isComplete {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (hc : IsComplete ↑(iSup V)) :
DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

An orthogonal family of subspaces of `E` satisfies `DirectSum.IsInternal` (that is, they provide an internal direct sum decomposition of `E`) if and only if their span has trivial orthogonal complement.

source
theorem OrthogonalFamily.isInternal_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] [FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

An orthogonal family of subspaces of `E` satisfies `DirectSum.IsInternal` (that is, they provide an internal direct sum decomposition of `E`) if and only if their span has trivial orthogonal complement.

source
theorem OrthogonalFamily.sum_projection_of_mem_iSup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ (i : ι), CompleteSpace ↥(V i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (x : E) (hx : x ∈ iSup V) :
∑ i : ι, (V i).starProjection x = x

If `x` lies within an orthogonal family `v`, it can be expressed as a sum of projections.

source
theorem OrthogonalFamily.projection_directSum_coeAddHom {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (x : DirectSum ι fun (i : ι) => ↥(V i)) (i : ι) [CompleteSpace ↥(V i)] :
(V i).orthogonalProjection ((DirectSum.coeAddMonoidHom V) x) = x i

If a family of submodules is orthogonal, then the `orthogonalProjection` on a direct sum is just the coefficient of that direct sum.

source
@[reducible, inline]
noncomputable abbrev OrthogonalFamily.decomposition {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ (i : ι), CompleteSpace ↥(V i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (h : iSup V = ⊤) :
DirectSum.Decomposition V

If a family of submodules is orthogonal and they span the whole space, then the orthogonal projection provides a means to decompose the space into its submodules.

The projection function is `decompose V x i = (V i).orthogonalProjection x`.

See note [reducible non-instances].

Equations

- hV.decomposition h = { decompose' := fun (x : E) => DFinsupp.equivFunOnFintype.symm fun (i : ι) => (V i).orthogonalProjection x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} (hv : Orthonormal 𝕜 Subtype.val) :
(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (Submodule.span 𝕜 v)ᗮ = ⊥

An orthonormal set in an `InnerProductSpace` is maximal, if and only if the orthogonal complement of its span is empty.

source
theorem maximal_orthonormal_iff_basis_of_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) :
(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ (b : Module.Basis (↑v) 𝕜 E), ⇑b = Subtype.val

An orthonormal set in a finite-dimensional `InnerProductSpace` is maximal, if and only if it is a basis.