Partial isometries in a star semigroup

An element u of a star semigroup is a partial isometry when u * star u * u = u. For a bounded operator on a Hilbert space this is the usual notion: star u * u is then the orthogonal projection onto the initial space of u, and u is isometric there and zero on its orthogonal complement. The Hilbert-space characterizations are in TauCeti/Analysis/InnerProductSpace/PartialIsometry.lean; this file records the purely algebraic part of the theory.

Main definitions

• TauCeti.IsPartialIsometry u: the element u satisfies u * star u * u = u. The predicate only needs a multiplication and a star operation; the structural results below hold in any star semigroup, so in particular in non-unital star rings such as non-unital C⋆-algebras.

Main statements

• TauCeti.IsPartialIsometry.star: the adjoint of a partial isometry is a partial isometry.
• TauCeti.IsPartialIsometry.isStarProjection_star_mul_self: the initial projection star u * u of a partial isometry is a star projection; isStarProjection_mul_star_self is the corresponding statement for the final projection u * star u.
• TauCeti.IsPartialIsometry.of_star_mul_self_eq_one, TauCeti.IsPartialIsometry.of_mem_unitary, IsStarProjection.isPartialIsometry: isometries, unitaries and star projections are partial isometries.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), the treatment of partial isometries and the polar decomposition.

def TauCeti.IsPartialIsometry {R : Type u_1} [Mul R] [Star R] (u : R) : Prop

An element u of a type with a multiplication and a star operation is a partial isometry when u * star u * u = u.

theorem TauCeti.isPartialIsometry_iff {R : Type u_1} [Mul R] [Star R] {u : R} : IsPartialIsometry u ↔ u * star u * u = u

Unfold the definition of a partial isometry.

theorem TauCeti.IsPartialIsometry.mul_star_mul_self {R : Type u_1} [Mul R] [Star R] {u : R} (hu : IsPartialIsometry u) : u * star u * u = u

The defining equation u * star u * u = u of a partial isometry.

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

The adjoint of a partial isometry is a partial isometry.

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

The initial projection star u * u of a partial isometry is a star projection.

theorem TauCeti.IsPartialIsometry.isStarProjection_mul_star_self {R : Type u_1} [Semigroup R] [StarMul R] {u : R} (hu : IsPartialIsometry u) : IsStarProjection (u * star u)

The final projection u * star u of a partial isometry is a star projection.

@[simp]

theorem TauCeti.isPartialIsometry_star_iff {R : Type u_1} [Semigroup R] [StarMul R] {u : R} : IsPartialIsometry (star u) ↔ IsPartialIsometry u

An element is a partial isometry iff its adjoint is.

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

An isometry, that is an element with star u * u = 1, is a partial isometry.

theorem TauCeti.IsPartialIsometry.of_mul_star_self_eq_one {R : Type u_1} [MulOneClass R] [Star R] {u : R} (h : u * star u = 1) : IsPartialIsometry u

A coisometry, that is an element with u * star u = 1, is a partial isometry.

theorem TauCeti.IsPartialIsometry.of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u ∈ unitary R) : IsPartialIsometry u

A unitary element is a partial isometry.

theorem TauCeti.IsPartialIsometry.one {R : Type u_1} [MulOneClass R] [StarMul R] : IsPartialIsometry 1

The identity is a partial isometry.

theorem TauCeti.IsPartialIsometry.zero {R : Type u_1} [MulZeroClass R] [Star R] : IsPartialIsometry 0

Zero is a partial isometry.

theorem IsStarProjection.isPartialIsometry {R : Type u_1} [Mul R] [Star R] {p : R} (hp : IsStarProjection p) : TauCeti.IsPartialIsometry p

A star projection is a partial isometry.