theorem OrientationTheorem.compact_subset_complement_eventually {X : Type u_1} [TopologicalSpace X] (A : ℕ → Set X) (hA_closed : ∀ (i : ℕ), IsClosed (A i)) (hA_decreasing : ∀ (i : ℕ), A (i + 1) ⊆ A i) (K : Set X) (hK : IsCompact K) (hKA : K ⊆ (⋂ (i : ℕ), A i)ᶜ) : ∃ (i : ℕ), K ⊆ (A i)ᶜ

If A i is a decreasing sequence of closed sets and K is a compact set disjoint from ⋂ i, A i, then K is already disjoint from some A i.

structure OrientationTheorem.CompactlySupportedDiagram {X : Type u_1} [TopologicalSpace X] (A : ℕ → Set X) (G : Set X → Type u_2) [(K : Set X) → AddCommGroup (G K)] : Type u_2

Data packaging "compactly supported" surjectivity and injectivity hypotheses for the sequence of groups G (A i) mapping to G (⋂ A i). Each element of the limit group is represented modulo a compact support condition, and each kernel element vanishes after restricting to a compact support. This is the abstract input to the colimit step of the proof of Lemma 32.4.

• ρ (i : ℕ) : G (A i) →+ G (⋂ (j : ℕ), A j)
• φ (i j : ℕ) : i ≤ j → G (A i) →+ G (A j)
• compat (i j : ℕ) (hij : i ≤ j) : (self.ρ j).comp (self.φ i j hij) = self.ρ i
• surj_support (x : G (⋂ (j : ℕ), A j)) : ∃ (K : Set X), IsCompact K ∧ K ⊆ (⋂ (i : ℕ), A i)ᶜ ∧ ∀ (i : ℕ), K ⊆ (A i)ᶜ → ∃ (g : G (A i)), (self.ρ i) g = x
• inj_support (i : ℕ) (g : G (A i)) : (self.ρ i) g = 0 → ∃ (K : Set X), IsCompact K ∧ K ⊆ (⋂ (n : ℕ), A n)ᶜ ∧ ∀ (j : ℕ) (hij : i ≤ j), K ⊆ (A j)ᶜ → (self.φ i j hij) g = 0

def OrientationTheorem.RelativeHomologyColimitData.ofCompactDecreasing {X : Type u_1} [TopologicalSpace X] (A : ℕ → Set X) (_hA_compact : ∀ (i : ℕ), IsCompact (A i)) (hA_closed : ∀ (i : ℕ), IsClosed (A i)) (hA_decreasing : ∀ (i : ℕ), A (i + 1) ⊆ A i) (G : Set X → Type u_2) [(K : Set X) → AddCommGroup (G K)] (csd : CompactlySupportedDiagram A G) : RelativeHomologyColimitData A G

Construction of the RelativeHomologyColimitData from a CompactlySupportedDiagram on a decreasing sequence of compact closed subsets. The surjectivity and injectivity conditions of the colimit are extracted from the compactly-supported data by combining them with compact_subset_complement_eventually. This is the core lemma giving $\varinjlim_i H_q(X, X - A_i) \cong H_q(X, X - A)$ in Lemma 32.4.

theorem OrientationTheorem.orientation_theorem_compact_convex (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))) (hA_compact : IsCompact A) (hA_convex : Convex ℝ A) (hA_nonempty : A.Nonempty) (Hrel : ℕ → Set (EuclideanSpace ℝ (Fin n)) → Type u_1) [(q : ℕ) → (K : Set (EuclideanSpace ℝ (Fin n))) → AddCommGroup (Hrel q K)] (Γsec : Set (EuclideanSpace ℝ (Fin n)) → Type u_2) [(K : Set (EuclideanSpace ℝ (Fin n))) → AddCommGroup (Γsec K)] (jMap : (K : Set (EuclideanSpace ℝ (Fin n))) → Hrel n K →+ Γsec K) : OrientationTheoremResult n Hrel Γsec jMap A

The orientation theorem holds for compact convex nonempty subsets of Euclidean space: this is the geometric base case used together with RelativeHomologyColimitData.ofCompactDecreasing to extend the orientation theorem from balls to compact subsets via Lemma 32.4.