Principal G-bundle

Stream: Is there code for X?

[Dominic Steinitz]

In the category of smooth manifolds with $G$ being a Lie group.

[Winston Yin (尹維晨)]

Hi @Dominic Steinitz, I realised nobody's been responding to your messages. Sorry! The manifold library is currently at the forefront of mathlib development, and I don't think principal G-bundle for Lie group G is in mathlib yet. I saw your other recent thread, so let me follow up with you there.