Standard constructions on fiber bundles #
This file contains several standard constructions on fiber bundles:
-
Bundle.Trivial.fiberBundle π B F
: the trivial fiber bundle with model fiberF
over the baseB
-
FiberBundle.prod
: for fiber bundlesEβ
andEβ
over a common base, a fiber bundle structure on their fiberwise productEβ Γα΅ Eβ
(the notation stands forfun x β¦ Eβ x Γ Eβ x
). -
FiberBundle.pullback
: for a fiber bundleE
overB
, a fiber bundle structure on its pullbackf *α΅ E
by a mapf : B' β B
(the notation is a type synonym forE β f
).
Tags #
fiber bundle, fibre bundle, fiberwise product, pullback
The trivial bundle #
Homeomorphism between the total space of the trivial bundle and the Cartesian product.
Instances For
Local trivialization for trivial bundle.
Instances For
Fiber bundle instance on the trivial bundle.
Fibrewise product of two bundles #
Equip the total space of the fiberwise product of two fiber bundles Eβ
, Eβ
with
the induced topology from the diagonal embedding into TotalSpace Fβ Eβ Γ TotalSpace Fβ Eβ
.
The diagonal map from the total space of the fiberwise product of two fiber bundles
Eβ
, Eβ
into TotalSpace Fβ Eβ Γ TotalSpace Fβ Eβ
is Inducing
.
Given trivializations eβ
, eβ
for fiber bundles Eβ
, Eβ
over a base B
, the forward
function for the construction Trivialization.prod
, the induced
trivialization for the fiberwise product of Eβ
and Eβ
.
Instances For
Given trivializations eβ
, eβ
for fiber bundles Eβ
, Eβ
over a base B
, the inverse
function for the construction Trivialization.prod
, the induced
trivialization for the fiberwise product of Eβ
and Eβ
.
Instances For
Given trivializations eβ
, eβ
for bundle types Eβ
, Eβ
over a base B
, the induced
trivialization for the fiberwise product of Eβ
and Eβ
, whose base set is
eβ.baseSet β© eβ.baseSet
.
Instances For
The product of two fiber bundles is a fiber bundle.
Pullbacks of fiber bundles #
Definition of Pullback.TotalSpace.topologicalSpace
, which we make irreducible.
Instances For
The topology on the total space of a pullback bundle is the coarsest topology for which both the projections to the base and the map to the original bundle are continuous.
A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle.