Compactification.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Compactification excision and ordinary relative section classes.

def OAI.Kaplansky.nonzeroBundle line 17
Source documentation
The ordinary total space with its entire zero section removed.
```
def nonzeroBundle : Set (TotalSpace V E) :=
…
```
theorem OAI.Kaplansky.mem_nonzeroBundle line 21
def OAI.Kaplansky.bundleCompactificationRelativeMap line 28
theorem OAI.Kaplansky.isOpen_compactifiedNonzeroBundle line 38
Source documentation
Compactness of the base makes the zero section closed even in the one-point total space. Infinity belongs to the removed open set.
```
theorem isOpen_compactifiedNonzeroBundle [CompactSpace B]
    [T2Space (OnePoint (TotalSpace V E))] :
    IsOpen (compactifiedNonzeroBundle (V := V) (E := E)) := by
…
```
Mentions: OAI.Kaplansky.compactifiedNonzeroBundle
theorem OAI.Kaplansky.bundleCompactificationRelativeMap_isIso line 46
Source documentation
Excision removes infinity from the actual target pair, in every degree. The whole zero section stays in the pair throughout.
```
theorem bundleCompactificationRelativeMap_isIso [CompactSpace B]
    [T2Space (OnePoint (TotalSpace V E))] (n : ℕ) :
    IsIso (bundleCompactificationRelativeMap (V := V) (E := E) n) := by
…
```
Mentions: OAI.Kaplansky.bundleCompactificationRelativeMap
def OAI.Kaplansky.bundleCompactificationRelativeIso line 57
def OAI.Kaplansky.canonicalProductOrdinaryRelativeMap line 69
theorem OAI.Kaplansky.canonicalProductRelativeMap_compactification line 80
theorem OAI.Kaplansky.canonicalProductRelativeMap_zero_iff line 88
def OAI.Kaplansky.ordinarySectionClassMap line 113
Source documentation
The section's absolute class followed by localization away from the whole zero section, in the original total space.
```
def ordinarySectionClassMap (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) (n : ℕ) :=
…
```
theorem OAI.Kaplansky.ordinarySectionClassMap_eq line 118
theorem OAI.Kaplansky.ordinarySectionClassMap_eq_zero line 130
Source documentation
A nowhere-zero section factors through the removed subspace, so its localized absolute map is zero in every degree.
```
theorem ordinarySectionClassMap_eq_zero (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (hne : ∀ b, s b ≠ 0) (n : ℕ) : ordinarySectionClassMap s hs n = 0 := by
…
```
Mentions: OAI.Kaplansky.ordinarySectionClassMap