Homological orientations of manifolds #
Let M be a Hausdorff space modelled on a finite-dimensional real normed space E, that is, a
topological manifold without boundary. A homological orientation of M in degree d
(TauCeti.HomologicalOrientation M E d) is a choice of local orientation, a generator of the
integral local homology H_d(M, M ∖ {x}; ℤ), at every point x of M, which is carried to itself
by the transport of local homology along paths. In the dimension d = finrank ℝ E of the
manifold, this is Hatcher's orientation of M: transport is computed through balls in charts
(TauCeti.localHomologyRestriction_comp_localHomologyTransport), so invariance under transport is
his local consistency condition. In other degrees the local homology vanishes, so the structure is
only of interest in the dimension of the manifold, where every statement below assumes it.
Orientations are the input of the integral fundamental class of a compact manifold
(TauCeti.HomologicalOrientation.fundamentalClass).
On a connected manifold an orientation is determined by its value at a single point
(TauCeti.HomologicalOrientation.eq_of_apply_eq), so a connected manifold has either no
orientation or exactly the two orientations o and -o
(TauCeti.HomologicalOrientation.eq_or_eq_neg, TauCeti.HomologicalOrientation.neg_ne). A
simply connected manifold is orientable: a local orientation at one point extends uniquely to an
orientation (TauCeti.HomologicalOrientation.ofSimplyConnectedSpace).
Main definitions #
TauCeti.HomologicalOrientation M E d: a transport-invariant family of local orientations.-o: the reversed orientation.TauCeti.HomologicalOrientation.ofSimplyConnectedSpace: the orientation of a simply connected manifold extending a given local orientation.
Main results #
TauCeti.HomologicalOrientation.eq_of_apply_eq: on a connected manifold, two orientations agreeing at one point are equal.TauCeti.HomologicalOrientation.eq_or_eq_neg: on a connected manifold, any two orientations agree up to reversal.TauCeti.HomologicalOrientation.neg_ne: on a nonempty manifold, an orientation differs from its reversal.TauCeti.HomologicalOrientation.nonempty_of_simplyConnectedSpace: a simply connected manifold has an orientation.
References #
- A. Hatcher, Algebraic Topology, Section 3.3.
A homological orientation of M in degree d: a local orientation at every point, that is a
generator of the integral local homology H_d(M, M ∖ {x}; ℤ), such that transport along every path
class carries the local orientation at its start to the local orientation at its end. In the
dimension of M this is an orientation of the manifold M in the sense of Hatcher.
- toFun (x : M) : LocalOrientation M x d
The local orientation at each point.
- localOrientationTransport_toFun' {x y : FundamentalGroupoid M} (f : x ⟶ y) : (localOrientationTransport M E d f) (self.toFun x.as) = self.toFun y.as
Transport along a path class carries the local orientation at its start to the local orientation at its end.
Instances For
Transport along a path class carries the local orientation at its start to the local orientation at its end.
The reversed orientation, reversing the local orientation at every point.
An orientation of a connected manifold is determined by its value at one point.
A connected manifold has at most two orientations: in the dimension of the manifold, any two orientations of a connected manifold agree up to reversal.
In the dimension of a nonempty manifold, an orientation differs from its reversal.
In the dimension of the manifold, a local orientation has infinite order: integral multiples
of o x with distinct coefficients are distinct.
Orientations of a simply connected manifold. A local orientation at one point extends, by transport along paths, to an orientation; all paths between two points are homotopic, so the transport does not depend on the path.
Instances For
The orientation extending a local orientation z at x is, at y, the transport of z
along any path from x to y.
The orientation extending a local orientation z at x is z at x.
A simply connected manifold is orientable.