Registry · Definition IV.D85 tau-effective formalized

IV.D85 — EM Principal Bundle

The electromagnetic principal bundle P_EM = (tau^3, tau^1, S^1_gamma, pr_1) with structure group U(1) acting by phase rotation on the gamma-circle fiber.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

IV.D02

Depended on by (8)

IV.D86 IV.D88 IV.D89 IV.D94 IV.D98 IV.P37 IV.R23 IV.T37

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.EmPrincipalBundle