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 #
Equations
- Bundle.Trivial.topologicalSpace B F = TopologicalSpace.induced Bundle.TotalSpace.proj tβ β TopologicalSpace.induced (Bundle.TotalSpace.trivialSnd B F) tβ
Alias of Bundle.Trivial.isInducing_toProd
.
Homeomorphism between the total space of the trivial bundle and the Cartesian product.
Equations
- Bundle.Trivial.homeomorphProd B F = (Bundle.TotalSpace.toProd B F).toHomeomorphOfIsInducing β―
Instances For
Local trivialization for trivial bundle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fiber bundle instance on the trivial bundle.
Equations
- One or more equations did not get rendered due to their size.
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β
.
Equations
- One or more equations did not get rendered due to their size.
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 an inducing map.
Alias of FiberBundle.Prod.isInducing_diag
.
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 an inducing map.
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β
.
Equations
- Trivialization.Prod.toFun' eβ eβ p = (p.proj, (βeβ { proj := p.proj, snd := p.snd.1 }).2, (βeβ { proj := p.proj, snd := p.snd.2 }).2)
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β
.
Equations
- Trivialization.Prod.invFun' eβ eβ p = { proj := p.1, snd := (eβ.symm p.1 p.2.1, eβ.symm p.1 p.2.2) }
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of two fiber bundles is a fiber bundle.
Equations
- One or more equations did not get rendered due to their size.
Pullbacks of fiber bundles #
Equations
- instTopologicalSpacePullback E f = inferInstanceAs ((x : B') β TopologicalSpace (E (f x)))
Definition of Pullback.TotalSpace.topologicalSpace
, which we make irreducible.
Equations
- pullbackTopology F E f = TopologicalSpace.induced Bundle.TotalSpace.proj instβ β TopologicalSpace.induced (Bundle.Pullback.lift f) inst
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.
Equations
- Pullback.TotalSpace.topologicalSpace F E f = pullbackTopology F E f
A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.