Sections.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Section classes in one-point compactifications and their naturality.

theorem OAI.Kaplansky.tendsto_onePoint_of_measure line 21

Source documentation

A continuous real-valued measurement tending to infinity forces escape from every closed compact set. Properness of the measurement is not needed.

theorem tendsto_onePoint_of_measure {X Z : Type*} [TopologicalSpace Z]
    {l : Filter X} {f : X → Z} (q : Z → ℝ) (hq : Continuous q)
    (h : Tendsto (fun x => q (f x)) l atTop) :
    Tendsto (fun x => (f x : OnePoint Z)) l (𝓝 ∞) := by
…

def OAI.Kaplansky.sectionToInfinity line 38
Source documentation
Push a nowhere-zero section out along each fiber, ending at infinity.
```
def sectionToInfinity (s : ∀ b, E b) (z : unitInterval × B) :
    OnePoint (TotalSpace V E) :=
…
```
theorem OAI.Kaplansky.sectionToInfinity_continuousAt_end line 44
theorem OAI.Kaplansky.continuous_sectionToInfinity line 78

def OAI.Kaplansky.compactifiedSectionNullHomotopy line 112

Source documentation

A nowhere-zero section is null-homotopic in the one-point total space. Continuity at infinity is proved from the actual continuous fiber norm.

def compactifiedSectionNullHomotopy (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (hnorm : Continuous (fun z : TotalSpace V E => ‖z.2‖))
    (hne : ∀ b, s b ≠ 0) :
    ContinuousMap.Homotopy (compactifiedSection s hs) (ContinuousMap.const B ∞) where
…

Mentions: OAI.Kaplansky.compactifiedSection

def OAI.Kaplansky.integralSingularHomology line 128
Source documentation
Ordinary singular homology with integer coefficients.
```
def integralSingularHomology (n : ℕ) : TopCat.{0} ⥤ ModuleCat.{0} ℤ :=
…
```
theorem OAI.Kaplansky.integralSingularHomology_homotopy line 131

theorem OAI.Kaplansky.integralSingularHomology_const line 137

Source documentation

A constant map induces zero in every positive homological degree.

theorem integralSingularHomology_const {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    (y : Y) {n : ℕ} (hn : n ≠ 0) :
    (integralSingularHomology n).map (TopCat.ofHom (ContinuousMap.const X y)) = 0 := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.sectionHomologyMap line 156
Source documentation
The section-induced map into the homology of the one-point total space. This is an actual singular homology morphism, not a postulated characteristic class.
```
def sectionHomologyMap (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) (n : ℕ) :
    (integralSingularHomology n).obj (TopCat.of B) ⟶
      (integralSingularHomology n).obj (TopCat.of (OnePoint (TotalSpace V E))) :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.sectionHomologyMap_eq line 164
Source documentation
Every pair of continuous sections induces the same integral homology map, even if their zero sets have different dimensions or contain degenerate zeros.
```
theorem sectionHomologyMap_eq (s t : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' V b (t b))) (n : ℕ) :
    sectionHomologyMap s hs n = sectionHomologyMap t ht n :=
…
```
Mentions: OAI.Kaplansky.sectionHomologyMap

theorem OAI.Kaplansky.sectionHomologyMap_eq_zero line 172

Source documentation

A nowhere-zero section makes its actual section-induced map vanish in positive degree. This does not assert that the canonical map is nonzero.

theorem sectionHomologyMap_eq_zero (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (hnorm : Continuous (fun z : TotalSpace V E => ‖z.2‖))
    (hne : ∀ b, s b ≠ 0) {n : ℕ} (hn : n ≠ 0) :
    sectionHomologyMap s hs n = 0 := by
…

Mentions: OAI.Kaplansky.sectionHomologyMap

theorem OAI.Kaplansky.sectionHomologyMap_eq_zero_of_nonvanishing line 183

Source documentation

If any nowhere-zero section exists, all section-induced maps vanish in positive degree. All geometric hypotheses are explicit.

theorem sectionHomologyMap_eq_zero_of_nonvanishing (s t : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' V b (t b)))
    (hnorm : Continuous (fun z : TotalSpace V E => ‖z.2‖))
    (hne : ∀ b, t b ≠ 0) {n : ℕ} (hn : n ≠ 0) :
    sectionHomologyMap s hs n = 0 :=
…

Mentions: OAI.Kaplansky.sectionHomologyMap

def OAI.Kaplansky.compactificationHomologyIso line 198

Source documentation

A genuine homeomorphism of total spaces gives an isomorphism on the integral homology of their one-point compactifications.

def compactificationHomologyIso {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    (e : X ≃ₜ Y) (n : ℕ) :
    (integralSingularHomology n).obj (TopCat.of (OnePoint X)) ≅
      (integralSingularHomology n).obj (TopCat.of (OnePoint Y)) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.sectionHomologyMap_naturality line 210

Source documentation

Naturality under an actual homeomorphism carrying one section to another. The equality concerns constructed singular homology morphisms.

theorem sectionHomologyMap_naturality (e : TotalSpace V E ≃ₜ TotalSpace W F)
    (s : ∀ b, E b) (t : ∀ b, F b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' W b (t b)))
    (he : ∀ b, e (TotalSpace.mk' V b (s b)) = TotalSpace.mk' W b (t b)) (n : ℕ) :
    sectionHomologyMap s hs n ≫ (compactificationHomologyIso e n).hom =
      sectionHomologyMap t ht n := by
…

Mentions: OAI.Kaplansky.sectionHomologyMap, OAI.Kaplansky.compactificationHomologyIso

theorem OAI.Kaplansky.sectionHomologyMap_naturality_zero_iff line 225

Source documentation

Vanishing is preserved and reflected by genuine bundle isomorphisms that carry the chosen sections to one another.

theorem sectionHomologyMap_naturality_zero_iff (e : TotalSpace V E ≃ₜ TotalSpace W F)
    (s : ∀ b, E b) (t : ∀ b, F b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' W b (t b)))
    (he : ∀ b, e (TotalSpace.mk' V b (s b)) = TotalSpace.mk' W b (t b)) (n : ℕ) :
    sectionHomologyMap s hs n = 0 ↔ sectionHomologyMap t ht n = 0 := by
…

Mentions: OAI.Kaplansky.sectionHomologyMap