Linear isometries, orthogonal complements, and product decompositions #
A linear isometry f : E →ₗᵢ[ℝ] F into a finite-dimensional inner product space identifies F
with the product of E and the orthogonal complement of the range of f, by
(u, w) ↦ f u + w. Read through this identification, f itself is the inclusion u ↦ (u, 0) of
the first factor. This is the normal form in which Mathlib's Manifold.IsImmersionAt asks for a
map to be written in charts, so this decomposition is what exhibits a linear isometry, and the maps
of spheres and balls it induces, as immersions.
A linear isometry also carries the orthogonal complement of a vector into the orthogonal complement of its image; this is how it transports the stereographic charts of unit spheres. For Euclidean spaces, a linear isometry matching a pair of standard basis vectors matches the corresponding coordinates; this is how it transports the half-space charts of closed balls.
An isometry between the orthogonal complements of two unit vectors extends uniquely to an ambient isometry sending one vector to the other. This extension works over both real and complex inner product spaces, without completeness or dimension assumptions.
Main definitions #
LinearIsometry.prodOrthogonalRangeEquiv: the continuous linear equivalenceE × (range f)ᗮ ≃L[ℝ] Fgiven by(u, w) ↦ f u + w.LinearIsometry.orthogonalComplementSingletonMap: the restriction of a linear isometry to a map(ℝ ∙ v)ᗮ →ₗᵢ[ℝ] (ℝ ∙ w)ᗮ, wherewis the image ofv.LinearIsometryEquiv.extendOrthogonalComplement: extend an isometry of orthogonal complements by its prescribed action on the radial line.
Main results #
LinearIsometry.apply_eq_of_map_single: a linear isometry of Euclidean spaces sending thei-th standard basis vector to thej-th one reads thei-th coordinate off as thej-th coordinate of the image.LinearMap.eq_of_apply_eq_of_eqOn_orthogonal: linear maps agreeing on a vector and its orthogonal complement are equal, without a unit-norm assumption.LinearIsometryEquiv.eq_extendOrthogonalComplement: a linear isometry equals the extension if it agrees on the unit vector and its orthogonal complement.
A linear isometry f maps the orthogonal complement of v into the orthogonal complement of
f v.
The restriction of a linear isometry f to a linear isometry from the orthogonal complement
of v to the orthogonal complement of its image w.
Equations
- f.orthogonalComplementSingletonMap hw = { toLinearMap := LinearMap.codRestrict (ℝ ∙ w)ᗮ (f.domRestrict (ℝ ∙ v)ᗮ) ⋯, norm_map' := ⋯ }
Instances For
A linear isometry f : E →ₗᵢ[ℝ] F into a finite-dimensional space identifies the product of
E with the orthogonal complement of the range of f with F, by (u, w) ↦ f u + w.
Equations
- f.prodOrthogonalRangeEquiv = ((f.equivRange.prodCongr (LinearEquiv.refl ℝ ↥f.rangeᗮ)).trans (f.range.prodEquivOfIsCompl f.rangeᗮ ⋯)).toContinuousLinearEquiv
Instances For
Through LinearIsometry.prodOrthogonalRangeEquiv, the linear isometry f is the inclusion of
the first factor.
A linear isometry of Euclidean spaces sending the i-th standard basis vector to the j-th
one reads the i-th coordinate of its argument off as the j-th coordinate of the image.
Linear maps are determined by their value on a vector and their restriction to its orthogonal complement. The vector need not be a unit vector or even nonzero.
Extend an isometry between the orthogonal complements of two unit vectors by sending
one unit vector to the other. The extension uses Mathlib's
Submodule.orthogonalDecomposition and LinearIsometryEquiv.toSpanUnitSingleton.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the orthogonal direct sum, the extension acts on the radial and transverse components separately.
The extension sends the distinguished unit vector to the distinguished target vector.
The extension agrees with the original isometry on the orthogonal complement.
An ambient linear isometry is uniquely determined by its value on a unit vector and its restriction to the orthogonal complement.