Zulip Chat Archive
Stream: Is there code for X?
Topic: Classification of Principal Bundles
Gad Wiseman (Dec 14 2025 at 14:50):
Is there code for the bijection between principal G-bundles and homotopy classes of maps to BG?
Michael Rothgang (Dec 14 2025 at 16:31):
Did you try searching for this yourself? What was the outcome of your attempts?
Junyan Xu (Dec 14 2025 at 16:51):
How do we define BG in mathlib? Probably this?
Dominic Steinitz (Dec 14 2025 at 17:04):
I didn't think we had a definition of a principal G-bundle?
Junyan Xu (Dec 14 2025 at 17:11):
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 (Dec 14 2025 at 22:04):
Dominic Steinitz said:
I didn't think we had a definition of a principal G-bundle?
But you're (loosely) working on this, right?
Last updated: Dec 20 2025 at 21:32 UTC