Thom classes and Euler classes of vector bundles #
Let E → B be a real vector bundle with finite-dimensional model fibre F of rank r, and let
E₀ ⊆ E be the complement of the zero section (TauCeti.zeroSectionCompl). The Thom pair of
the bundle is the topological pair (E, E₀) (TauCeti.thomPair). A Thom class is a relative
class u ∈ Hʳ(E, E₀) whose restriction to every fibre pair (E_b, E_b ∖ {0}) generates the
cohomology of that pair (TauCeti.IsThomClass). With ordinary integral coefficients (specified
below) this is a cohomological orientation of the bundle; by the Thom isomorphism theorem, which
is not formalized here, every orientation determines a unique Thom class, and -u belongs to the
opposite orientation.
The Euler class of a relative class u ∈ Hⁿ(E, E₀) is its image in Hⁿ(B) under the
restriction Hⁿ(E, E₀) ⟶ Hⁿ(E) followed by pullback along the zero section
(TauCeti.eulerClass). With ordinary integral coefficients, for a Thom class this is the Euler
class of the oriented bundle, the characteristic class whose evaluation on surfaces appears in
the Euler class inequalities for foliations.
The Euler class is natural under maps of Thom pairs covering a map of bases
(TauCeti.eulerClass_naturality), in particular under pullback of bundles
(TauCeti.eulerClass_pullback). A map of Thom pairs restricting to isomorphisms of fibre pairs
carries Thom classes to Thom classes (TauCeti.IsThomClass.singularCohomologyMap); in particular,
pullback of bundles does (TauCeti.IsThomClass.pullback). The zero section is homotopic, through
t • s, to any continuous section s (TauCeti.zeroSectionHomotopy). So if s is nonzero off a
set S, the Euler class of u is the image of the pull-back s^* u ∈ Hⁿ(B, B ∖ S)
(TauCeti.eulerClass_eq_singularCohomologyMap_thomPairMapOfNeZero). In particular, a bundle with a
nowhere-vanishing continuous section has zero Euler class
(TauCeti.eulerClass_eq_zero_of_forall_ne_zero): every relative class restricts to zero on E₀.
So a trivial bundle of positive rank has zero Euler class (TauCeti.eulerClass_trivial_eq_zero).
Cohomology is the singular cohomology of TauCeti/AlgebraicTopology/Cohomology/, with the same
general coefficients: Hom(C(X; R), M) in a k-linear abelian category C. Integral cohomology
uses C := ModuleCat ℤ, k := ℤ, and R = M = ModuleCat.of ℤ ℤ.
Main definitions #
TauCeti.zeroSectionCompl: the nonzero vectorsE₀of a bundle.TauCeti.thomPair: the Thom pair(E, E₀).TauCeti.thomPairOver: the Thom pair(E|_W, E₀|_W)of the restriction to a subsetWof the base; over the whole base it is the Thom pair(E, E₀)(TauCeti.thomPairOverUnivIso).TauCeti.thomPairOverMap: the restriction map(E|_W, E₀|_W) ⟶ (E|_{W'}, E₀|_{W'})forW ⊆ W'.TauCeti.fiberThomPairMap,TauCeti.fiberThomPairOverMap: the inclusions of the fibre pair(E_b, E_b ∖ {0})into the Thom pair and into the Thom pair over a set containingb.TauCeti.thomPairMapOfNeZero: a continuous mapf : X → Etaking nonzero values off a setS, as a map of pairs(X, X ∖ S) ⟶ (E, E₀).TauCeti.thomPairProj: the projection of the total space to the base, as a morphism of topological spaces out of the ambient space of the Thom pair.TauCeti.IsThomClass: a relative class restricting to a generator on every fibre.TauCeti.zeroSectionHomotopy: the straight-line homotopyt • sfrom the zero section to a continuous sections.TauCeti.eulerClass: the Euler classHⁿ(E, E₀) ⟶ Hⁿ(B).TauCeti.negTotalSpace,TauCeti.negThomPairMap: fibrewise negation, as a self-map of the total space and of the Thom pair; it does not change Euler classes (TauCeti.singularCohomologyMap_negThomPairMap_comp_eulerClass). On a fibre it is conjugate to negation ofF(TauCeti.fiberThomPairMap_comp_negThomPairMap).
References #
- J. W. Milnor, J. D. Stasheff, Characteristic Classes, Annals of Mathematics Studies 76,
Princeton (1974), §9 (the fundamental class
u ∈ Hⁿ(E, E₀; ℤ)of an oriented bundle, the Euler class, its naturality and its vanishing for a bundle with a nowhere-zero section) and §10 (the Thom isomorphism). - A. Hatcher, Vector Bundles and K-Theory, §4.D (Thom classes).
The complement E₀ of the zero section in the total space of a bundle: its nonzero
vectors.
Instances For
The nonzero vectors are the complement of the range of the zero section.
The Thom pair (E, E₀) of a bundle: its total space relative to the complement of the zero
section.
Instances For
The Thom pair (E|_W, E₀|_W) of the restriction of a bundle to a subset W of its base: the
vectors over W, relative to the nonzero ones, as subspaces of the total space.
Instances For
Over the whole base, the Thom pair (E|_B, E₀|_B) of the restriction is the Thom pair
(E, E₀).
Instances For
For W ⊆ W', the map of Thom pairs (E|_W, E₀|_W) ⟶ (E|_{W'}, E₀|_{W'}) induced by the
inclusion.
Instances For
The map of pairs (X, X ∖ S) ⟶ (E, E₀) into the Thom pair of a bundle given by a continuous
map f : X → E which takes nonzero values off S. For a section s and S its zero set, this is
s as a map of pairs.
Instances For
Precomposing thomPairMapOfNeZero f with the map of pairs induced by a continuous map g
gives thomPairMapOfNeZero of any map equal to f ∘ g.
The inclusion (E_b, E_b ∖ {0}) ⟶ (E, E₀) of the fibre over b into the Thom pair.
Instances For
The projection π : E ⟶ B of a fibre bundle, as a morphism of topological spaces out of the
ambient space of its Thom pair.
Instances For
The fibre inclusion over b followed by the projection is constant at b.
The inclusion (E_b, E_b ∖ {0}) ⟶ (E|_W, E₀|_W) of the fibre over a point b ∈ W into the
Thom pair of the restriction to W.
Instances For
The fibre inclusions commute with the restriction maps of Thom pairs.
The fibre inclusions commute with the restriction maps of Thom pairs.
Over the whole base, the fibre inclusion into (E|_B, E₀|_B) is the fibre inclusion into the
Thom pair (E, E₀).
Over the whole base, the fibre inclusion into (E|_B, E₀|_B) is the fibre inclusion into the
Thom pair (E, E₀).
The fibre inclusion over b into the Thom pair (E, E₀), followed by the inclusion of the
pair over the whole base into the pair over a set W' covering the base, is the fibre inclusion
into the pair over any W ⊆ W' containing b, followed by the inclusion of the pair over W
into the pair over W'.
A Thom class of a real vector bundle with finite-dimensional model fibre F of rank
r = finrank ℝ F: a relative class u ∈ Hʳ(E, E₀) whose restriction to the fibre pair
(E_b, E_b ∖ {0}) over every point b generates the k-module Hʳ(E_b, E_b ∖ {0}). With ordinary
integral coefficients (C := ModuleCat ℤ, k := ℤ, R = M = ModuleCat.of ℤ ℤ) this is the notion
of a cohomological orientation of the bundle.
Finite-dimensionality of F is part of the predicate: otherwise finrank ℝ F = 0 and the
degree-zero condition would hold vacuously, so a bundle with infinite-dimensional fibres has no
Thom class.
Instances For
Negation preserves the fibrewise generator condition, so the negative of a Thom class is a Thom class.
Thom classes pull back along fibrewise isomorphisms. Let φ : (E', E'₀) ⟶ (E, E₀) be a map
of Thom pairs which, over a map of bases g : B' → B, restricts on the fibre over every b' to an
isomorphism ψ b' of fibre pairs (E'_{b'}, E'_{b'} ∖ {0}) ≅ (E_{g b'}, E_{g b'} ∖ {0}). Then φ
pulls Thom classes of E back to Thom classes of E'.
The zero of a fibre of the pullback f*E is the zero of the corresponding fibre of E.
Instances For
The map (f*E, (f*E)₀) ⟶ (E, E₀) of Thom pairs covering a continuous map f : B' → B.
Instances For
The fibre of the Thom pair of f*E over b' is included in the Thom pair of E as the fibre
over f b'.
The canonical map from the total space of a pull-back bundle covers the map of bases.
The pullback of a Thom class of E along a continuous map f is a Thom class of f*E.
The zero section B ⟶ E of a real vector bundle, as a morphism of topological spaces into
the ambient space of the Thom pair.
Instances For
Fibrewise negation v ↦ -v of a real vector bundle, written v ↦ (-1) • v, as a self-map of
its total space.
Instances For
Fibrewise negation v ↦ -v, as a self-map of the Thom pair (E, E₀).
Instances For
Fibrewise negation fixes the zero section.
The straight-line homotopy t • s from the zero section to a continuous section s.
Instances For
The Euler class e(u) ∈ Hⁿ(B) of a relative class u ∈ Hⁿ(E, E₀) of a real vector bundle, as
a morphism Hⁿ(E, E₀) ⟶ Hⁿ(B): restriction from the Thom pair to the total space, followed by
pullback along the zero section. With ordinary integral coefficients (C := ModuleCat ℤ,
k := ℤ, R = M = ModuleCat.of ℤ ℤ), the Euler class of an oriented bundle is the image of its
Thom class (TauCeti.IsThomClass).
Instances For
Naturality of the Euler class. A map of Thom pairs φ : (E', E'₀) ⟶ (E, E₀) which carries
the zero section over a map of bases f : B' ⟶ B to the zero section intertwines the Euler
classes.
The Euler class through a section. If a real vector bundle has a continuous section s
which is nonzero off a set S ⊆ B, then the Euler class of a relative class u ∈ Hⁿ(E, E₀) is the
image in Hⁿ(B) of its pull-back s^* u ∈ Hⁿ(B, B ∖ S) along s : (B, B ∖ S) ⟶ (E, E₀): the zero
section is homotopic to s through t • s.
A nowhere-vanishing section kills the Euler class. If a real vector bundle has a continuous
section s with s b ≠ 0 for every b, then its Euler class vanishes in every degree: the zero
section is homotopic through t • s to s, which takes values in E₀, and every relative class
restricts to zero on E₀.
The Euler class is invariant under fibrewise negation: pulling a relative class back along
v ↦ -v does not change its Euler class, since negation fixes the zero section.
The Euler class of a pullback bundle f*E is the pullback along f of the Euler class of
E.
Fibrewise negation is conjugate to negation of F. On the fibre over b, read through a
continuous linear equivalence t : E b ≃L[ℝ] F, the map negThomPairMap is
t⁻¹ ∘ (x ↦ -x) ∘ t.
A trivial real vector bundle B × V of positive rank has zero Euler class in every degree.