Rectangular corner algebra from a partial isometry (source code)

= Rectangular corner algebra from a partial isometry
{title2=$pAq\cong qAq,\quad a\cdot b=au^*b,\quad a^\dagger=ua^*u$}

For a nonzero <partial isometry> $u$ in a <C-star algebra>, put $p=uu^*$ and $q=u^*u$. The closed linear space $pAq$ becomes a unital <C-star algebra> with the displayed operations and inherited <norm>, with unit $u$. The map $a\mapsto u^*a$ is an isometric \i[-isomorphism onto the ordinary corner $qAq$, with inverse $b\mapsto ub$. The identities $uu^*a=a$ and $u^*ub=b$ verify the inverse maps, while contractivity of both multiplications gives <isometry>. Products and involutions transfer directly, giving all algebra and C]-<norm> axioms. This construction turns a rectangular operator corner into a square algebra by using the <partial isometry> as its unit.