Unitary elements span C⋆-algebras

Main results

• CStarAlgebra.exists_sum_four_unitary: every element x in a unital C⋆-algebra is a linear combination of four unitary elements, and the norm of each coefficient does not exceed ‖x‖ / 2.
• CStarAlgebra.span_unitary: a unital C⋆-algebra is spanned by its unitary elements.

theorem IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : IsSelfAdjoint a) (ha_norm : ‖a‖ ≤ 1) : a + Complex.I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

If a : A is a selfadjoint element in a C⋆-algebra with ‖a‖ ≤ 1, then a + I • CFC.sqrt (1 - a ^ 2) is unitary.

This is the key tool to show that a C⋆-algebra is spanned by its unitary elements.

noncomputable def selfAdjoint.unitarySelfAddISMul {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : ↥(selfAdjoint A)) (ha_norm : ‖a‖ ≤ 1) : ↥(unitary A)

For a selfadjoint with ‖a‖ ≤ 1, this is the unitary a + I • √(1 - a ^ 2).

Equations

• selfAdjoint.unitarySelfAddISMul a ha_norm = ⟨↑a + Complex.I • CFC.sqrt (1 - ↑a ^ 2), ⋯⟩

@[simp]

theorem selfAdjoint.unitarySelfAddISMul_coe {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : ↥(selfAdjoint A)) (ha_norm : ‖a‖ ≤ 1) : ↑(unitarySelfAddISMul a ha_norm) = ↑a + Complex.I • CFC.sqrt (1 - ↑a ^ 2)

theorem selfAdjoint.star_coe_unitarySelfAddISMul {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : ↥(selfAdjoint A)) (ha_norm : ‖a‖ ≤ 1) : star ↑(unitarySelfAddISMul a ha_norm) = ↑a - Complex.I • CFC.sqrt (1 - ↑a ^ 2)

theorem selfAdjoint.realPart_unitarySelfAddISMul {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : ↥(selfAdjoint A)) (ha_norm : ‖a‖ ≤ 1) : realPart ↑(unitarySelfAddISMul a ha_norm) = a

theorem CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (x : A) (hx : x ≠ 0) : have u₁ := selfAdjoint.unitarySelfAddISMul (realPart (‖x‖⁻¹ • x)) ⋯; have u₂ := selfAdjoint.unitarySelfAddISMul (imaginaryPart (‖x‖⁻¹ • x)) ⋯; x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + Complex.I • (↑u₂ + ↑(star u₂)))

A stepping stone to CStarAlgebra.exists_sum_four_unitary that specifies the unitary elements precisely. The lets in the statement are intentional.

theorem CStarAlgebra.exists_sum_four_unitary {A : Type u_1} [CStarAlgebra A] (x : A) : ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Every element x in a unital C⋆-algebra is a linear combination of four unitary elements, and the norm of each coefficient does not exceed ‖x‖ / 2.

theorem CStarAlgebra.span_unitary (A : Type u_1) [CStarAlgebra A] : Submodule.span ℂ ↑(unitary A) = ⊤

A unital C⋆-algebra is spanned by its unitary elements.