Conclusion of Theorem 32.1 for a compact subset K. Packages the
two assertions of the orientation theorem for an n-manifold M and a
compact set K ⊆ M: the relative homology groups Hrel q K vanish for
q > n, and the comparison map jMap K : Hrel n K → Γsec K to sections
of the orientation sheaf is a bijection. Stated abstractly so that the
proof structure of Section 32 can be reused for any homology theory
Hrel/section functor Γsec satisfying the appropriate axioms.
- isomorphism : Function.Bijective ⇑(jMap K)
Instances For
Mayer–Vietoris ladder data for Proposition 32.2. Records the
relevant portion of the commutative diagram with exact rows used to prove
that if the orientation theorem holds for A, B, and A ∩ B, then it
holds for A ∪ B: the top row is the relative-homology Mayer–Vietoris
sequence at degrees n and q > n, the bottom row is the
Mayer–Vietoris sequence for sections of the orientation sheaf, and
jMap provides the comparison map between them.
- mv_exact : Function.Exact ⇑self.mvα ⇑self.mvβ
- sec_exact : Function.Exact ⇑self.secα ⇑self.secβ
Instances For
Build a MayerVietorisLadder from the full Mayer–Vietoris long exact
sequences in Hrel and Γsec together with the commutation hypotheses.
Uses the vanishing part of the orientation theorem on A ∩ B to derive
injectivity of mvα and of the higher-degree maps mvα_q for q > n,
since their kernels lie in Hrel (q+1) (A ∩ B) = 0.
Instances For
Proposition 32.2, ladder form. Given the orientation theorem on
A, B, and A ∩ B, together with a Mayer–Vietoris ladder relating
their relative homologies and section groups, deduce the orientation
theorem on A ∪ B. The vanishing part follows from injectivity of mvα
in degrees q > n, and the bijectivity of jMap (A ∪ B) is obtained by
the five-lemma applied to the ladder.
Abstract data of the relative Mayer–Vietoris long exact sequences in
all degrees together with the section-sequence and compatibility
conditions, packaged so that MayerVietorisLadder.ofExactSequences can
be invoked from a single bundle.
- mv_exact_δα (q : ℕ) : Function.Exact ⇑(self.mvδ_q q) ⇑(self.mvα_q q)
- mv_exact_αβ (q : ℕ) : Function.Exact ⇑(self.mvα_q q) ⇑(self.mvβ_q q)
- sec_exact : Function.Exact ⇑self.secα ⇑self.secβ
Instances For
Manifold-level construction of the Mayer–Vietoris data for closed
subsets A, B ⊆ M of a topological n-manifold. Currently a placeholder
referring to the underlying Mayer–Vietoris machinery for the homology of
closed pairs in a manifold.
Instances For
Specialises relativeMVSequenceData_from_manifold and feeds it
through MayerVietorisLadder.ofExactSequences to produce the
Mayer–Vietoris ladder needed by orientation_theorem_union_of_ladder.
Instances For
Proposition 32.2. If M is a topological n-manifold and the
orientation theorem holds for each of the closed subsets A, B, and
A ∩ B of M, then it holds for the union A ∪ B.
Lemma 32.5. In a Hausdorff space, given a decreasing sequence
A₀ ⊇ A₁ ⊇ ⋯ of compact subsets and an open set U containing the
intersection ⋂ i, A i, some term A i is already contained in U.
Proved by contradiction using compactness of the nonempty closed sets
A i \ U.
Iterated form of the union step (Proposition 32.2): if the
union_step hypothesis is available, then the orientation theorem
propagates from intersections ⋂ i ∈ S, D i along nonempty finite
families to the union ⋃ i ∈ T, D i over any nonempty finite index set
T with T.card ≤ k. Proved by induction on k, peeling off one
element at a time and applying union_step.
Reduces the orientation theorem for a compact A ⊆ M to the case of
intersections A ∩ ⋂ i ∈ S, D i where D : Fin m → Set M is a finite
closed cover of A. Combines result_finset_biUnion with the
decomposition A = ⋃ i, A ∩ D i.
Abstract data witnessing that G (⋂ j, A j) is the colimit of the
sequence G (A i) along the inclusions A (i+1) ⊆ A i: restriction
maps ρ i to the intersection, transition maps φ i j compatible with
them, and the two filtered-colimit conditions (every element of the
limit comes from some G (A i), and an element vanishing in the limit
already vanishes at some larger stage).
Instances For
If every group G (A i) vanishes, the colimit G (⋂ j, A j) also
vanishes. Used to propagate the vanishing part of the orientation
theorem from a decreasing sequence of compact sets to their
intersection.
If a natural transformation f : G ⟶ H of colimit data induces a
bijection at each stage A i, then the induced map on colimits
f (⋂ j, A j) is also bijective. This is the standard fact that
filtered colimits of bijections are bijections, packaged in the form
needed to upgrade the orientation-theorem isomorphism from each A i to
their intersection.
Proposition 32.3, abstract form. For a decreasing sequence
A₀ ⊇ A₁ ⊇ ⋯ of compact subsets of a Hausdorff n-manifold-like
space, given colimit data witnessing that Hrel q (⋂ i, A i) and
Γsec (⋂ i, A i) are colimits of Hrel q (A i) and Γsec (A i), the
orientation theorem on each A i implies the orientation theorem on
the intersection ⋂ i, A i.
Bundle of all colimit data needed for the orientation_theorem_iInter
proof at a single decreasing compact sequence: per-degree
RelativeHomologyColimitData for Hrel q, one for Γsec, and the
compatibility of jMap with the restriction and transition maps.
- colH (q : ℕ) : RelativeHomologyColimitData A (Hrel q)
- colΓ : RelativeHomologyColimitData A Γsec
Instances For
Companion to compact_decreasing_sequence_subset_open rephrased in
complement form: if K is a compact subset of the complement of
⋂ i, A i where A i is a decreasing sequence of closed sets, then
K ⊆ (A i)ᶜ already for some i. Proved using the directed-cover
formulation of compactness.
Manifold-flavoured constructor for
ColimitDataForDecreasingCompact: assembles the colimit data from the
manifold versions of the surjectivity and injectivity assertions, where
witnesses are presented as compact subsets of the complement of
⋂ i, A i and are converted to indices using
compact_subset_complement_eventually_aux.
Instances For
Existence of the ColimitDataForDecreasingCompact for any
decreasing sequence of compact subsets of a topological n-manifold;
placeholder for the underlying construction that produces the relative
homology and section colimit data from the manifold's Mayer–Vietoris /
excision machinery.
Instances For
Proposition 32.3. For a decreasing sequence of compact subsets
of a topological n-manifold, given the colimit data from
ColimitDataForDecreasingCompact, the orientation theorem propagates
from each A i to their intersection ⋂ i, A i.
Lemma 32.4-style auxiliary. Any compact subset A of a
topological n-manifold can be covered by finitely many closed sets
D i, each contained in the source of an atlas chart. This is the
reduction step that brings the proof of Theorem 32.1 to the
Euclidean-chart base case.
Theorem 32.1, abstract reduction. The orientation theorem holds
for any compact subset A of a topological n-manifold, provided one
supplies the chart-level base case (orientation theorem on any compact
subset of a single chart) and the Mayer–Vietoris-style union_step
(Proposition 32.2). The proof covers A by finitely many closed
chart-contained sets via compact_finite_closed_chart_cover and then
invokes orientation_theorem_from_cover.