Registry · Proposition IV.P37 tau-effective formalized

IV.P37 — EM Bundle Topology

The EM principal bundle is classified by the first Chern class c_1 in H^2(tau^1; Z) = Z, corresponding to the winding number of the transition function.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.EmBundleTopology