Partial isometries (Sub-dev II)

A partial isometry in a star-monoid is an element u with u * star u * u = u; equivalently star u * u is a projection (IsStarProjection). For operators on an inner product space this is the classical notion: u restricts to an isometry on (ker u)ᗮ and vanishes on ker u.

Mathlib currently has no partial-isometry API (grep-confirmed). This packages the unitary factor of the polar decomposition A = U |A|.

Source: Conway, A Course in Functional Analysis, 2nd ed., §VI.3 (partial isometries and the polar decomposition); Reed–Simon, Methods of Modern Mathematical Physics I, §VI (before Thm VI.10).

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.PartialIsometry, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 3676b55.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Opus 4.8; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

def IsPartialIsometry {R : Type u_1} [Monoid R] [StarMul R] (u : R) : Prop

Partial isometry (algebraic form): u * star u * u = u.

Equations

• IsPartialIsometry u = (u * star u * u = u)

theorem IsPartialIsometry.isStarProjection_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsPartialIsometry u) : IsStarProjection (star u * u)

For a partial isometry, star u * u is a projection. Conway VI.3.2.

theorem IsPartialIsometry.star_star {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsPartialIsometry u) : IsPartialIsometry (star u)

star u is a partial isometry when u is.

theorem IsPartialIsometry.of_star_mul_self_eq_one {R : Type u_1} [Monoid R] [StarMul R] {u : R} (h : star u * u = 1) : IsPartialIsometry u

A unitary element is a partial isometry (star u * u = 1).

theorem IsPartialIsometry.star_mul_self_eq_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {u : E →ₗ[𝕜] E} (hu : IsPartialIsometry u) : star u * u = ↑u.kerᗮ.starProjection

The initial projection of a partial isometry is the orthogonal projection onto (ker u)ᗮ: star u * u = P_{(ker u)ᗮ}. Conway VI.3.2.

theorem isPartialIsometry_iff_norm_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {u : E →ₗ[𝕜] E} : IsPartialIsometry u ↔ ∀ x ∈ u.kerᗮ, ‖u x‖ = ‖x‖

Operator characterization: u is a partial isometry iff it is norm-preserving on the orthogonal complement of its kernel. Conway VI.3.2.

theorem isPartialIsometry_of_isometryOn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {u : E →ₗ[𝕜] E} {K : Submodule 𝕜 E} (hker : u.ker = Kᗮ) (hiso : ∀ x ∈ K, ‖u x‖ = ‖x‖) : IsPartialIsometry u

Constructor used by the polar decomposition: a linear map that is isometric on a submodule K and vanishes on Kᗮ is a partial isometry with initial space K. Conway VI.3.9.