Integral and rational fundamental classes of an oriented manifold #
Let M be a Hausdorff space modelled on a real normed space E of finite dimension n, that is,
a topological n-manifold without boundary, and let o be an orientation of M
(TauCeti.HomologicalOrientation M E n).
For a compact subset A ⊆ M, the local orientations of o glue to a unique class
o.fundamentalClassOn hn hA of Hₙ(M, M ∖ A; ℤ) restricting to the local orientation o x at
each point x ∈ A. These classes are compatible with restriction to smaller compact subsets.
Along a finite set Z, the fundamental class is the sum over z ∈ Z of the local orientations
o z, each read through excision in an open neighbourhood of z containing no other point of
Z and pushed into Hₙ(M, M ∖ Z; ℤ).
For M compact, there is a unique class o.fundamentalClass hn of Hₙ(M; ℤ), the fundamental
class of M for the orientation o, whose image in Hₙ(M, M ∖ {x}; ℤ) is o x for every
x. Reversing the orientation negates it. Its image under the change of coefficients ℤ → ℝ is
the real fundamental class o.realFundamentalClass hn ∈ Hₙ(M; ℝ). If M is moreover connected,
the fundamental class generates Hₙ(M; ℤ) freely: c ↦ c • o.fundamentalClass hn is an
isomorphism from ℤ, so every class of Hₙ(M; ℤ) is an integer multiple of it.
A continuous map f : M → X carries the fundamental class to a class f_*[M] ∈ Hₙ(X; ℤ), which
is functorial in f and depends only on the homotopy class of f.
The fundamental class is what cohomology classes are evaluated on, through the Kronecker map
TopCat.singularKronecker, and what Poincaré duality caps with.
Main definitions #
TauCeti.HomologicalOrientation.fundamentalClassOn: the fundamental classμ_AofMalong a compact subsetA.TauCeti.HomologicalOrientation.localOrientationAlong: the local orientation atz, read through excision in an open neighbourhoodUofzand pushed intoHₙ(M, M ∖ Z; ℤ)for a setZmeetingUat most inz.TauCeti.HomologicalOrientation.fundamentalClass: the fundamental class of a compact oriented manifold.TauCeti.HomologicalOrientation.realFundamentalClass: the image of the fundamental class inHₙ(M; ℝ).TauCeti.HomologicalOrientation.fundamentalClassEquiv: for a compact connected oriented manifold, the isomorphismℤ ≃ₗ[ℤ] Hₙ(M; ℤ)sending1to the fundamental class.TauCeti.HomologicalOrientation.mapFundamentalClass: the imagef_*[M] ∈ Hₙ(X; ℤ)of the fundamental class under a continuous mapf : M → X.
For a compact connected oriented manifold, the integral top homology is freely generated by its
fundamental class. Extending scalars along the flat map ℤ → ℚ gives the normalized rational
fundamental-class equivalence HomologicalOrientation.rationalFundamentalClassEquiv. Its value
at 1 is the rational fundamental class; a rational coefficient c maps to c times this class.
The coefficient change uses Mathlib's native simplicial-chain comparison and exact-functor
homology isomorphism directly, without requiring Poincaré duality.
Main results #
TauCeti.HomologicalOrientation.rationalFundamentalClassEquiv: the normalized equivalenceℚ ≃ₗ[ℚ] Hₙ(M; ℚ)on a compact connected oriented manifold.TauCeti.HomologicalOrientation.fundamentalClassOn_eq_sum_localOrientationAlong: the fundamental class along a finite set is the sum of the local orientations at its points.TauCeti.HomologicalOrientation.eq_fundamentalClass: the fundamental class is the only class restricting to the orientation at every point.TauCeti.HomologicalOrientation.fundamentalClass_neg: the fundamental class of the reversed orientation is the negated fundamental class.TauCeti.HomologicalOrientation.mapFundamentalClass_eq_of_homotopic: homotopic maps carry the fundamental class to the same class.TauCeti.HomologicalOrientation.singularHomologyπ_mapFundamentalClass: the image off_*[M]inHₙ(X, X ∖ X; ℤ)is the image of the fundamental class alongMunder the map of pairsf.TauCeti.HomologicalOrientation.exists_eq_zsmul_fundamentalClass: on a compact connected oriented manifold, every top-dimensional class is a multiple of the fundamental class.
Implementation notes #
The manifold lives in Type. The gluing results this file rests on
(TauCeti.existsUnique_localHomologyRestriction_eq_of_invariant and the top homology of a compact
manifold) take coefficients in ModuleCat.{w} Λ for a ring Λ : Type w in the universe of M,
as Mathlib's exactness of filtered colimits of modules is stated in that generality; the integral
coefficients ModuleCat.of ℤ (ULift ℤ) of local orientations meet this condition in Type.
References #
- A. Hatcher, Algebraic Topology, Section 3.3, Lemma 3.27 and Theorem 3.26.
The coefficient map ℤ → ℝ, from the integral coefficients ULift ℤ of the fundamental class
to real coefficients, as a morphism of abelian groups.
Instances For
The coefficient map ℤ → ℝ is the cast of integers to reals.
The fundamental class of M along a compact subset A: the unique class of
Hₙ(M, M ∖ A; ℤ) whose restriction to Hₙ(M, M ∖ {x}; ℤ) is the local orientation o x at
every point x ∈ A.
Instances For
The fundamental class along A restricts to the local orientation at every point of A.
Uniqueness of the fundamental class along A: a class of Hₙ(M, M ∖ A; ℤ) restricting
to the local orientation at every point of A is the fundamental class along A.
The fundamental classes along compact subsets are compatible with restriction: for compact
B ⊆ A, the fundamental class along A restricts to the fundamental class along B.
The fundamental class along a point is the local orientation there.
Reversing the orientation negates the fundamental class along A.
The local orientation o z ∈ Hₙ(M, M ∖ {z}; ℤ), read in Hₙ(U, U ∖ {z}; ℤ) through excision
for an open neighbourhood U of z, and pushed into Hₙ(M, M ∖ Z; ℤ) along the inclusion of
U, for a set Z meeting U at most in z.
Instances For
The class o.localOrientationAlong is the image of the local orientation o z under the
inverse of the excision isomorphism of U, followed by the map induced by the inclusion of U.
The class o.localOrientationAlong at z ∈ Z restricts to the local orientation at z.
The class o.localOrientationAlong at z restricts to 0 at every point of Z other than
z.
The fundamental class along a finite set is a sum of local orientations. For a finite set
Z and open neighbourhoods U z ∋ z with U z ∩ Z ⊆ {z}, the fundamental class along Z is the
sum over z ∈ Z of the local orientations o z, read through excision in U z and pushed into
Hₙ(M, M ∖ Z; ℤ).
The fundamental class of a compact oriented manifold: the unique class of Hₙ(M; ℤ)
whose image in the local homology Hₙ(M, M ∖ {x}; ℤ) is the local orientation o x at every
point x. The image in local homology is the quotient map to Hₙ(M, M ∖ M; ℤ) followed by
restriction.
Instances For
The fundamental class restricts to the local orientation at every point.
Uniqueness of the fundamental class: a class of Hₙ(M; ℤ) whose image in the local
homology at every point is the local orientation there is the fundamental class.
The image of the fundamental class in Hₙ(M, M ∖ A; ℤ) is the fundamental class along the
compact set A.
Reversing the orientation negates the fundamental class.
The real fundamental class of a compact oriented manifold: the image of the fundamental
class in the real singular homology Hₙ(M; ℝ).
Instances For
The real fundamental class is the image of the fundamental class under the change of
coefficients ℤ → ℝ.
Reversing the orientation negates the real fundamental class.
The image f_*[M] ∈ Hₙ(X; ℤ) of the fundamental class of a compact oriented manifold M under
a continuous map f : M → X: the homology class carried by the singular manifold f.
Instances For
The image of the fundamental class under the identity is the fundamental class.
The image of the fundamental class under a composite g ∘ f is the image under g of its
image under f.
Homotopy invariance: homotopic maps carry the fundamental class to the same class.
Reversing the orientation negates the image of the fundamental class.
The image of f_*[M] in Hₙ(X, X ∖ X; ℤ) is the image of the fundamental class along the
whole of M under the map of pairs f : (M, M ∖ M) → (X, X ∖ X).
The fundamental class generates the top homology freely. For a compact connected oriented
manifold, c ↦ c • o.fundamentalClass hn is an isomorphism ℤ ≃ₗ[ℤ] Hₙ(M; ℤ).
Instances For
On a compact connected oriented manifold, every class of Hₙ(M; ℤ) is an integer multiple of
the fundamental class.
The rational fundamental class generates top homology freely. For a compact connected
oriented manifold, rational extension of its integral fundamental-class equivalence gives
ℚ ≃ₗ[ℚ] Hₙ(M; ℚ). No finite CW model is required.
Instances For
Reversing orientation negates every value of the normalized rational equivalence.
The rational fundamental class, normalized by rational extension of the integral fundamental
class. It is the image of 1 under rationalFundamentalClassEquiv.
Instances For
The rational fundamental class is the normalized equivalence evaluated at one.
Reversing orientation negates the rational fundamental class.
The rational fundamental-class equivalence sends c to c times the rational fundamental
class.