1: \begin{definition}{\bf(Principal comodule algebras).}\label{DSHA16}\index{Algebra!Principal Comodule}

2: Let $H$ be a Hopf algebra with bijective antipode. A right $H$-comodule algebra $(A,\rho_A)$ satisfying the conditions of Theorem \ref{DSHA15} is called a \emph{principal comodule algebra}.

3: \end{definition}

4: