Orthogonal complements and projections under restriction of scalars

A complex inner product space E is a real inner product space for the inner product re ⟪x, y⟫ (InnerProductSpace.complexToReal). This file compares the two orthogonality relations on complex subspaces. For a complex subspace K, a vector is real-orthogonal to K exactly when it is complex-orthogonal to K, since K is stable under multiplication by I. Consequently the real orthogonal complement of K is again a complex subspace, and the real and complex orthogonal projections onto K agree.

The real inner product is not a global instance in Mathlib, so it is enabled locally here; the statements below are about that real structure.

Main results

• Submodule.orthogonal_restrictScalars: (K.restrictScalars ℝ)ᗮ = Kᗮ.restrictScalars ℝ.
• Submodule.starProjection_restrictScalars_apply: the real orthogonal projection onto K is the complex one.

@[simp]

theorem Submodule.orthogonal_restrictScalars {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : Submodule ℂ E) : (restrictScalars ℝ K)ᗮ = restrictScalars ℝ Kᗮ

For the real inner product re ⟪x, y⟫, the orthogonal complement of a complex subspace is the complex orthogonal complement. In particular it is stable under multiplication by I.

instance Submodule.HasOrthogonalProjection.restrictScalars {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : Submodule ℂ E) [K.HasOrthogonalProjection] : (Submodule.restrictScalars ℝ K).HasOrthogonalProjection

A complex subspace admitting a complex orthogonal projection admits a real one.

@[simp]

theorem Submodule.starProjection_restrictScalars_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : Submodule ℂ E) [K.HasOrthogonalProjection] (v : E) : (restrictScalars ℝ K).starProjection v = K.starProjection v

The real orthogonal projection onto a complex subspace is the complex orthogonal projection.