The canonical finite-dimensional polar factor

Every linear map A between finite-dimensional real or complex inner product spaces factors as A = U |A|, where |A| is its positive modulus and U is a partial isometry. The canonical factor A.polarFactor extends the isometric rule |A| x ↦ A x by zero on ker A. It has the same kernel and range as A, and is the unique factor through the modulus that vanishes on ker A. This normalization distinguishes it from unitary extensions of the polar factor.

The construction uses ContinuousLinearMap.factorThru and the finite-dimensional modulus; it applies to rectangular maps, including maps with nontrivial kernel. Its initial space is (ker A)ᗮ and its final space is range A.

The adjoint of the polar factor inverts it on the modulus, U† A = |A|, and conjugates the two moduli into each other, |A†| = A U† = U |A| U†. Consequently the canonical polar factor of A† is U†, and A = |A†| U is the left polar decomposition. Between spaces of the same dimension, U agrees on (ker A)ᗮ with a linear isometric equivalence, and it is one when A is injective.

The modulus and the polar factor are natural for isometries: |W A| = |A| and the polar factor of W A is W U for an isometric embedding W, and conjugating A by a linear isometric equivalence conjugates |A| and U. When an endomorphism A commutes with |A|, for example when A is normal, its polar factor commutes with both |A| and A.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Theorem 7.3.1.
• J. B. Conway, A Course in Functional Analysis, second edition, Springer, 1990, §VI.3.

noncomputable def LinearMap.polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : E →ₗ[𝕜] F

The canonical polar partial isometry of a finite-dimensional linear map. It sends |A| x to A x and vanishes on ker A.

theorem LinearMap.toContinuousLinearMap_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : have this := ⋯; have this_1 := ⋯; toContinuousLinearMap A.polarFactor = (toContinuousLinearMap A).factorThru (toContinuousLinearMap A.operatorAbs)

The polar factor as a bounded operator is the canonical factor through the modulus.

@[simp]

theorem LinearMap.polarFactor_operatorAbs_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : A.polarFactor (A.operatorAbs x) = A x

The polar factor carries the modulus of a vector to its image under the original map.

@[simp]

theorem LinearMap.polarFactor_comp_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.polarFactor ∘ₗ A.operatorAbs = A

Finite-dimensional polar decomposition: A = U |A| for its canonical polar factor.

@[simp]

theorem LinearMap.polarFactor_apply_of_mem_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {x : E} (hx : x ∈ A.ker) : A.polarFactor x = 0

The polar factor vanishes on the kernel of the original map.

theorem LinearMap.norm_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {x : E} (hx : x ∈ A.kerᗮ) : ‖A.polarFactor x‖ = ‖x‖

The canonical polar factor preserves norms on the initial space (ker A)ᗮ.

@[simp]

theorem LinearMap.ker_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.polarFactor.ker = A.ker

The canonical polar factor has exactly the same kernel as the original map.

@[simp]

theorem LinearMap.isPartialIsometry_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.polarFactor.IsPartialIsometry

The canonical polar factor is a partial isometry.

@[simp]

theorem LinearMap.range_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.polarFactor.range = A.range

The canonical polar factor has exactly the same range as the original map.

theorem LinearMap.eq_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {V : E →ₗ[𝕜] F} (hV : V ∘ₗ A.operatorAbs = A) (hV₀ : ∀ x ∈ A.ker, V x = 0) : V = A.polarFactor

The factorization through the modulus and vanishing on ker A characterize the canonical polar factor, without assuming that the competing factor is a partial isometry.

theorem LinearMap.eq_polarFactor_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {V : E →ₗ[𝕜] F} : V = A.polarFactor ↔ V ∘ₗ A.operatorAbs = A ∧ ∀ x ∈ A.ker, V x = 0

A map is the canonical polar factor exactly when it factors the original map through its modulus and vanishes on its kernel.

@[simp]

theorem LinearMap.polarFactor_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] : polarFactor 0 = 0

The canonical polar factor of the zero map is zero.

The adjoint of the polar factor

@[simp]

theorem LinearMap.adjoint_polarFactor_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : (adjoint A.polarFactor) (A x) = A.operatorAbs x

The adjoint of the canonical polar factor carries the image of a vector back to its modulus: U† (A x) = |A| x.

@[simp]

theorem LinearMap.adjoint_polarFactor_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : adjoint A.polarFactor ∘ₗ A = A.operatorAbs

The adjoint of the canonical polar factor carries the original map back to its modulus: U† A = |A|.

@[simp]

theorem LinearMap.operatorAbs_comp_adjoint_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs ∘ₗ adjoint A.polarFactor = adjoint A

The adjoint of the polar decomposition: A† = |A| U†.

@[simp]

theorem LinearMap.operatorAbs_apply_adjoint_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (y : F) : A.operatorAbs ((adjoint A.polarFactor) y) = (adjoint A) y

The adjoint of the polar decomposition, applied to a vector: |A| (U† y) = A† y.

theorem LinearMap.operatorAbs_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).operatorAbs = A ∘ₗ adjoint A.polarFactor

The modulus of the adjoint is the original map composed with the adjoint of its canonical polar factor: |A†| = A U†, equivalently |A†| = U |A| U†.

@[simp]

theorem LinearMap.polarFactor_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).polarFactor = adjoint A.polarFactor

The canonical polar factor of the adjoint is the adjoint of the canonical polar factor.

@[simp]

theorem LinearMap.adjoint_polarFactor_comp_operatorAbs_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : adjoint A.polarFactor ∘ₗ (adjoint A).operatorAbs = adjoint A

The polar decomposition of the adjoint, in terms of the adjoint of the polar factor: A† = U† |A†|.

@[simp]

theorem LinearMap.adjoint_polarFactor_apply_operatorAbs_adjoint_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (y : F) : (adjoint A.polarFactor) ((adjoint A).operatorAbs y) = (adjoint A) y

The polar decomposition of the adjoint, applied to a vector: U† (|A†| y) = A† y.

@[simp]

theorem LinearMap.ker_adjoint_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A.polarFactor).ker = (adjoint A).ker

The adjoint of the canonical polar factor has the same kernel as the adjoint.

@[simp]

theorem LinearMap.range_adjoint_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A.polarFactor).range = (adjoint A).range

The adjoint of the canonical polar factor has the same range as the adjoint.

@[simp]

theorem LinearMap.operatorAbs_adjoint_comp_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).operatorAbs ∘ₗ A.polarFactor = A

Left polar decomposition: A = |A†| U for the canonical polar factor U of A.

@[simp]

theorem LinearMap.operatorAbs_adjoint_apply_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : (adjoint A).operatorAbs (A.polarFactor x) = A x

The left polar decomposition, applied to a vector: |A†| (U x) = A x.

Commutation with the modulus

theorem LinearMap.commute_polarFactor_operatorAbs_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (h : Commute A A.operatorAbs) : Commute A.polarFactor A.operatorAbs

If an endomorphism commutes with its modulus, for example a normal one (LinearMap.commute_operatorAbs), then so does its canonical polar factor.

theorem LinearMap.commute_polarFactor_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (h : Commute A A.operatorAbs) : Commute A.polarFactor A

If an endomorphism commutes with its modulus, for example a normal one (LinearMap.commute_operatorAbs), then it commutes with its canonical polar factor.

Isometric changes of coordinates

@[simp]

theorem LinearMap.operatorAbs_linearIsometry_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (W : F →ₗᵢ[𝕜] G) (A : E →ₗ[𝕜] F) : (W.toLinearMap ∘ₗ A).operatorAbs = A.operatorAbs

Composing with an isometric embedding on the left does not change the modulus: |W A| = |A|.

theorem LinearMap.operatorAbs_comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (A : F →ₗ[𝕜] G) (e : E ≃ₗᵢ[𝕜] F) : (A ∘ₗ ↑e.toLinearEquiv).operatorAbs = ↑e.symm.toLinearEquiv ∘ₗ A.operatorAbs ∘ₗ ↑e.toLinearEquiv

Composing with a linear isometric equivalence on the right conjugates the modulus: |A e| = e⁻¹ |A| e.

@[simp]

theorem LinearMap.polarFactor_linearIsometry_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (W : F →ₗᵢ[𝕜] G) (A : E →ₗ[𝕜] F) : (W.toLinearMap ∘ₗ A).polarFactor = W.toLinearMap ∘ₗ A.polarFactor

Composing with an isometric embedding on the left composes the canonical polar factor: the polar factor of W A is W U.

@[simp]

theorem LinearMap.polarFactor_comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (A : F →ₗ[𝕜] G) (e : E ≃ₗᵢ[𝕜] F) : (A ∘ₗ ↑e.toLinearEquiv).polarFactor = A.polarFactor ∘ₗ ↑e.toLinearEquiv

Composing with a linear isometric equivalence on the right composes the canonical polar factor: the polar factor of A e is U e.

theorem LinearMap.operatorAbs_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (e : E ≃ₗᵢ[𝕜] F) (T : E →ₗ[𝕜] E) : operatorAbs (e.conj T) = e.conj T.operatorAbs

The modulus is natural under conjugation by a linear isometric equivalence.

theorem LinearMap.polarFactor_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (e : E ≃ₗᵢ[𝕜] F) (T : E →ₗ[𝕜] E) : polarFactor (e.conj T) = e.conj T.polarFactor

The canonical polar factor is natural under conjugation by a linear isometric equivalence.

Unitary extensions

theorem LinearMap.exists_linearIsometryEquiv_eqOn_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (h : Module.finrank 𝕜 E = Module.finrank 𝕜 F) : ∃ (U : E ≃ₗᵢ[𝕜] F), Set.EqOn ⇑U ⇑A.polarFactor ↑A.kerᗮ

Unitary extension of the polar factor. Between spaces of the same dimension, the canonical polar factor agrees on its initial space (ker A)ᗮ with a linear isometric equivalence.

theorem LinearMap.exists_linearIsometryEquiv_eq_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} (hA : Function.Injective ⇑A) (h : Module.finrank 𝕜 E = Module.finrank 𝕜 F) : ∃ (U : E ≃ₗᵢ[𝕜] F), ↑↑↑U = A.polarFactor

Invertible polar unitary. Between spaces of the same dimension, the canonical polar factor of an injective map is a linear isometric equivalence.