Thom.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Thom spaces of line stages, disk collapse, quotient maps, and homology.

theorem OAI.Kaplansky.bundleTotal_t2Space line 18

Source documentation

Hausdorffness of a genuine bundle total space, using separation in the base or in a common local trivialization.

theorem bundleTotal_t2Space {B V : Type*} [TopologicalSpace B] [T2Space B]
    [TopologicalSpace V] [T2Space V] (E : B → Type*)
    [∀ b, TopologicalSpace (E b)] [TopologicalSpace (TotalSpace V E)] [FiberBundle V E] :
    T2Space (TotalSpace V E) := by
…

instance OAI.Kaplansky.lineStageTotal_t2Space line 37
instance OAI.Kaplansky.lineStageTotal_locallyCompactSpace line 40
instance OAI.Kaplansky.lineStageThom_t2Space line 46
Source documentation
The one-point total space used by the homology construction is a compact Hausdorff space for the actual finite line bundle sum.
```
instance lineStageThom_t2Space (a : LineStage K) :
    T2Space (OnePoint (TotalSpace a.Model a.Fiber)) := inferInstance
…
```
Mentions: OAI.Kaplansky.LineStage
theorem OAI.Kaplansky.lineStage_chart_norm line 50
theorem OAI.Kaplansky.isCompact_lineStage_disk line 62
Source documentation
Closed bounded disk bundles over the compact projective base are compact. This uses a finite cover by actual unitary trivializations.
```
theorem isCompact_lineStage_disk (a : LineStage K) (r : ℝ) :
    IsCompact {z : TotalSpace a.Model a.Fiber | ‖z.2‖ ≤ r} := by
…
```
Mentions: OAI.Kaplansky.LineStage
abbrev OAI.Kaplansky.LineStageClosedDisk line 98
instance OAI.Kaplansky.lineStageClosedDisk_compact line 100
def OAI.Kaplansky.lineStageDiskCollapse line 104
Source documentation
Radial collapse of the entire unit sphere bundle to the point at infinity.
```
def lineStageDiskCollapse (z : LineStageClosedDisk a) : OnePoint (TotalSpace a.Model a.Fiber) :=
…
```
Mentions: OAI.Kaplansky.LineStageClosedDisk
theorem OAI.Kaplansky.lineStageDiskCollapse_boundary line 111
theorem OAI.Kaplansky.lineStageDiskCollapse_continuousAt_boundary line 114
theorem OAI.Kaplansky.continuous_lineStageDiskCollapse line 154
def OAI.Kaplansky.lineStageDiskInterior line 189
Source documentation
An actual vector has a canonical interior preimage under radial collapse.
```
def lineStageDiskInterior (z : TotalSpace a.Model a.Fiber) : LineStageClosedDisk a :=
…
```
Mentions: OAI.Kaplansky.LineStageClosedDisk
theorem OAI.Kaplansky.lineStageDiskCollapse_interior line 193
theorem OAI.Kaplansky.lineStageDiskCollapse_eq_infty_iff line 205
Source documentation
Only sphere-bundle vectors collapse to infinity.
```
theorem lineStageDiskCollapse_eq_infty_iff (z : LineStageClosedDisk a) :
    lineStageDiskCollapse a z = ∞ ↔ ‖z.val.2‖ = 1 := by
…
```
Mentions: OAI.Kaplansky.LineStageClosedDisk, OAI.Kaplansky.lineStageDiskCollapse
theorem OAI.Kaplansky.lineStageDiskInterior_expand line 217
theorem OAI.Kaplansky.lineStageDiskCollapse_eq_iff line 231
Source documentation
Exact quotient relation: collapse the sphere bundle and identify no distinct interior disk vectors.
```
theorem lineStageDiskCollapse_eq_iff (z w : LineStageClosedDisk a) :
    lineStageDiskCollapse a z = lineStageDiskCollapse a w ↔
      z = w ∨ (‖z.val.2‖ = 1 ∧ ‖w.val.2‖ = 1) := by
…
```
Mentions: OAI.Kaplansky.LineStageClosedDisk, OAI.Kaplansky.lineStageDiskCollapse
theorem OAI.Kaplansky.lineStage_sphere_nonempty line 253
Source documentation
Positive fiber rank supplies a genuine sphere-bundle point.
```
theorem lineStage_sphere_nonempty [Nonempty a.Slot] :
    ∃ z : LineStageClosedDisk a, ‖z.val.2‖ = 1 := by
…
```
Mentions: OAI.Kaplansky.LineStageClosedDisk
theorem OAI.Kaplansky.lineStageDiskCollapse_surjective line 260
theorem OAI.Kaplansky.lineStageDiskCollapse_isQuotientMap line 269
abbrev OAI.Kaplansky.LineStageThomQuotient line 276
Source documentation
The disk/sphere quotient, with its quotient topology. The exact relation is given by lineStageDiskCollapse_eq_iff.
```
abbrev LineStageThomQuotient := Quotient (Setoid.ker (lineStageDiskCollapse a))
```
Mentions: OAI.Kaplansky.lineStageDiskCollapse
def OAI.Kaplansky.lineStageThomQuotientHomeomorph line 281
Source documentation
The actual disk/sphere Thom quotient is homeomorphic to the one-point total space used in the singular homology construction. This assertion is for positive fiber rank; no characteristic class is assumed.
```
def lineStageThomQuotientHomeomorph [Nonempty a.Slot] :
    LineStageThomQuotient a ≃ₜ OnePoint (TotalSpace a.Model a.Fiber) :=
…
```
Mentions: OAI.Kaplansky.LineStageThomQuotient
theorem OAI.Kaplansky.lineStageThomQuotientHomeomorph_apply line 287

theorem OAI.Kaplansky.lineStageThomQuotientHomeomorph_zero line 292

Source documentation

The zero-section inclusion is carried to the actual zero-section map, so the quotient comparison respects the section used by the invariant.

theorem lineStageThomQuotientHomeomorph_zero [Nonempty a.Slot] (y : ProjectiveProduct K) :
    lineStageThomQuotientHomeomorph a
      (Quotient.mk _ (⟨TotalSpace.mk' a.Model y 0, by erw [norm_zero]; exact zero_le_one⟩ : LineStageClosedDisk a)) =
        (TotalSpace.mk' a.Model y (0 : a.Fiber y) : OnePoint (TotalSpace a.Model a.Fiber)) := by
…

Mentions: OAI.Kaplansky.lineStageThomQuotientHomeomorph, OAI.Kaplansky.LineStageClosedDisk

def OAI.Kaplansky.thomQuotientZeroSection line 310
Source documentation
The actual zero section into the disk/sphere quotient.
```
def thomQuotientZeroSection : C(ProjectiveProduct K, LineStageThomQuotient a) where
…
```
Mentions: OAI.Kaplansky.LineStageThomQuotient
def OAI.Kaplansky.thomZeroHomologyMap line 320
Source documentation
The integral homology morphism of the genuine Thom zero section. Its definition supplies no nonvanishing, Thom class, or Chern-class axiom.
```
def thomZeroHomologyMap (n : ℕ) :=
…
```
def OAI.Kaplansky.thomQuotientHomologyIso line 323
theorem OAI.Kaplansky.thomZeroHomologyMap_comparison line 329
theorem OAI.Kaplansky.thomZeroHomologyMap_eq_section line 340
Source documentation
Every continuous section computes the same map from the base into the homology of the genuine Thom space, under the proved comparison.
```
theorem thomZeroHomologyMap_eq_section [Nonempty a.Slot]
    (s : ∀ y, a.Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' a.Model y (s y))) (n : ℕ) :
    thomZeroHomologyMap a n ≫ (thomQuotientHomologyIso a n).hom = sectionHomologyMap s hs n :=
…
```
Mentions: OAI.Kaplansky.thomZeroHomologyMap, OAI.Kaplansky.thomQuotientHomologyIso, OAI.Kaplansky.sectionHomologyMap
theorem OAI.Kaplansky.thomZeroHomologyMap_eq_zero_of_nonvanishing line 351
Source documentation
A nowhere-zero section forces the Thom zero-section map itself to vanish, using the actual inverse of the homology comparison isomorphism.
```
theorem thomZeroHomologyMap_eq_zero_of_nonvanishing [Nonempty a.Slot]
    (s : ∀ y, a.Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' a.Model y (s y)))
    (hne : ∀ y, s y ≠ 0) {n : ℕ} (hn : n ≠ 0) : thomZeroHomologyMap a n = 0 := by
…
```
Mentions: OAI.Kaplansky.thomZeroHomologyMap
theorem OAI.Kaplansky.hyperplaneThomHomology_comparison line 366
Source documentation
Specialization to the exact canonical hyperplane-product section. This identifies two constructed global maps; it does not compute them.
```
theorem hyperplaneThomHomology_comparison
    [Nonempty (hyperplaneProductStage K).Slot] (n : ℕ) :
    thomZeroHomologyMap (hyperplaneProductStage K) n ≫
      (thomQuotientHomologyIso (hyperplaneProductStage K) n).hom =
        canonicalProductHomologyMap K n :=
…
```
Mentions: OAI.Kaplansky.hyperplaneProductStage, OAI.Kaplansky.thomZeroHomologyMap, OAI.Kaplansky.thomQuotientHomologyIso, OAI.Kaplansky.canonicalProductHomologyMap