In fact, a principal comodule algebra is the same as an \(H\) -equivariantly projective Hopf–Galois extension.
The projectivity property gives the notion of a principal comodule algebra full geometric meaning,
as it implies that \(A\)  admits a noncommutative connection in the sense of [1]}. This is in perfect concord with Cartan's definition of a principal action of a compact Lie group [2]}.
We return to these differential geometric aspects of principal comodule algebras in Section .
