Obstruction.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Survival of hyperplane fiber classes and nonvanishing Thom obstructions.

theorem OAI.Kaplansky.graphBundleChartNormalization_isIso line 17
theorem OAI.Kaplansky.graphBundleChartToAmbient_mono line 28
Source documentation
Every graph-chart fiber class survives inclusion into the whole actual bundle pair in fiber degree. The global normalization provides a left inverse up to the proved local isomorphism.
```
theorem graphBundleChartToAmbient_mono (F : ∀ i, GraphFrame 1 (K i))
    (hp : 0 < ∑ i, K i) :
    Mono (restrictedPairToAmbientHomologyMap (graphBundleChartDomain K F)
      nonzeroBundle (2*(∑ i, K i))) := by
…
```
Mentions: OAI.Kaplansky.restrictedPairToAmbientHomologyMap, OAI.Kaplansky.graphBundleChartDomain, OAI.Kaplansky.nonzeroBundle
theorem OAI.Kaplansky.canonicalFiberGenerator_whole_ne_zero line 42
Source documentation
The original, preserved integral fiber generator has nonzero image in the whole hyperplane bundle. No choice of a new generator is involved.
```
theorem canonicalFiberGenerator_whole_ne_zero (hp : 0 < ∑ i, K i) :
    canonicalWholeBundleFiberMap K (2*(∑ i, K i)) (canonicalFiberGenerator K hp) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.canonicalWholeBundleFiberMap, OAI.Kaplansky.canonicalFiberGenerator
theorem OAI.Kaplansky.canonicalNormalizedOverlapGenerator_punctured_ne_zero line 56
Source documentation
The exact dependency recorded in Preserve376: the specified primitive overlap generator survives the ACTUAL punctured-bundle map.
```
theorem canonicalNormalizedOverlapGenerator_punctured_ne_zero (hp : 0 < ∑ i, K i) :
    canonicalOverlapPuncturedMap K (2*(∑ i, K i))
      (canonicalNormalizedOverlapGenerator K hp) ≠ 0 :=
…
```
Mentions: OAI.Kaplansky.canonicalOverlapPuncturedMap, OAI.Kaplansky.canonicalNormalizedOverlapGenerator
theorem OAI.Kaplansky.canonicalProductOrdinaryRelativeGenerator_ne_zero line 62
theorem OAI.Kaplansky.canonicalProductRelativeGenerator_ne_zero line 68
theorem OAI.Kaplansky.canonicalProductHomology_fundamental_ne_zero line 76
Source documentation
The canonical section sends the preserved integral fundamental class to a nonzero absolute homology class of the actual compactification.
```
theorem canonicalProductHomology_fundamental_ne_zero (hp : 0 < ∑ i, K i) :
    canonicalProductHomologyMap K (2*(∑ i, K i))
      (projectiveProductFundamentalClass K hp) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.canonicalProductHomologyMap, OAI.Kaplansky.projectiveProductFundamentalClass
theorem OAI.Kaplansky.canonicalProductHomologyMap_ne_zero line 89
theorem OAI.Kaplansky.hyperplaneProduct_sectionHomology_ne_zero line 105
Source documentation
Every continuous section of the actual hyperplane sum induces a nonzero homology map in degree 2 sum(K), including degenerate sections.
```
theorem hyperplaneProduct_sectionHomology_ne_zero (hp : 0 < ∑ i, K i)
    (s : ∀ y, (hyperplaneProductStage K).Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' (hyperplaneProductStage K).Model y (s y))) :
    sectionHomologyMap s hs (2*(∑ i, K i)) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.hyperplaneProductStage, OAI.Kaplansky.sectionHomologyMap
theorem OAI.Kaplansky.hyperplaneProduct_every_section_has_zero line 114
Source documentation
A genuine section obstruction for H, the rank-sum(K) hyperplane sum. It makes no assertion about H with additional trivial summands.
```
theorem hyperplaneProduct_every_section_has_zero (hp : 0 < ∑ i, K i)
    (s : ∀ y, (hyperplaneProductStage K).Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' (hyperplaneProductStage K).Model y (s y))) :
    ∃ y, s y = 0 := by
…
```
Mentions: OAI.Kaplansky.hyperplaneProductStage
theorem OAI.Kaplansky.hyperplaneProduct_no_positive_frame line 123

theorem OAI.Kaplansky.hyperplaneProduct_transported_sectionHomology_ne_zero line 132

Source documentation

Nonvanishing survives an actual total-space homeomorphism carrying a section to a section, by the already proved compactification naturality.

theorem hyperplaneProduct_transported_sectionHomology_ne_zero
    {W : Type} [NormedAddCommGroup W] [NormedSpace ℂ W]
    {E : ProjectiveProduct K → Type}
    [∀ y, NormedAddCommGroup (E y)] [∀ y, NormedSpace ℂ (E y)]
    [TopologicalSpace (TotalSpace W E)] [FiberBundle W E] [VectorBundle ℂ W E]
    (hp : 0 < ∑ i, K i)
    (e : TotalSpace (hyperplaneProductStage K).Model (hyperplaneProductStage K).Fiber ≃ₜ TotalSpace W E)
    (t : ∀ y, E y) (ht : Continuous (fun y => TotalSpace.mk' W y (t y)))
    (he : ∀ y, e (TotalSpace.mk' (hyperplaneProductStage K).Model y (hyperplaneProductSection K y)) =
      TotalSpace.mk' W y (t y)) :
    sectionHomologyMap t ht (2*(∑ i, K i)) ≠ 0 :=
…

Mentions: OAI.Kaplansky.hyperplaneProductStage, OAI.Kaplansky.hyperplaneProductSection, OAI.Kaplansky.sectionHomologyMap

theorem OAI.Kaplansky.hyperplaneThomZeroHomologyMap_ne_zero line 156
Source documentation
Nonvanishing in the genuine disk/sphere Thom quotient, with no assumed Thom class or characteristic-class identification.
```
theorem hyperplaneThomZeroHomologyMap_ne_zero (hp : 0 < ∑ i, K i) :
    thomZeroHomologyMap (hyperplaneProductStage K) (2*(∑ i, K i)) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.thomZeroHomologyMap, OAI.Kaplansky.hyperplaneProductStage
theorem OAI.Kaplansky.retainedTest_hyperplaneDegree_pos line 167
theorem OAI.Kaplansky.retainedTest_hyperplaneThom_ne_zero line 172
theorem OAI.Kaplansky.retainedTest_hyperplane_every_section_has_zero line 177