Classification of Principal Bundles

Stream: Is there code for X?

[Gad Wiseman]

Is there code for the bijection between principal G-bundles and homotopy classes of maps to BG?

[Michael Rothgang]

Did you try searching for this yourself? What was the outcome of your attempts?

[Junyan Xu]

How do we define BG in mathlib? Probably this?

[Dominic Steinitz]

I didn't think we had a definition of a principal G-bundle?

[Junyan Xu]

If G is discrete then we are about to have it: https://github.com/leanprover-community/mathlib4/pull/7596/files#r2616225613
The definition is close to this MO answer.

[Michael Rothgang]

Dominic Steinitz said:

I didn't think we had a definition of a principal G-bundle?

But you're (loosely) working on this, right?

[Dominic Steinitz]

Michael Rothgang said:

Dominic Steinitz said:

I didn't think we had a definition of a principal G-bundle?

But you're (loosely) working on this, right?

Yes and now that I have proved the existence of a Riemannian metric, I can give it my full attention. The first thing is to decide which definition we should use. Maybe I should make a list of the ones I know.