HyperplaneLocal.lean`

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Relative section classes and local homology at hyperplane product zeros.

theorem OAI.Kaplansky.continuous_lineStage_totalNorm line 22
Source documentation
The norm on the actual line-stage total space is continuous. The proof uses its genuine continuous Hermitian metric, not fixed fiber coordinates.
```
theorem continuous_lineStage_totalNorm (a : LineStage K) :
    Continuous (fun z : TotalSpace a.Model a.Fiber => ‖z.2‖) := by
…
```
Mentions: OAI.Kaplansky.LineStage
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.sectionHomologyMap_eq_zero line 33
Source documentation
An arbitrary nonempty orthonormal frame forces all section-induced homology maps of its actual bundle to vanish in positive degree.
```
theorem ContinuousOrthonormalStageFrame.sectionHomologyMap_eq_zero
    {a : LineStage K} {d : ℕ} (f : ContinuousOrthonormalStageFrame a d) (hd : 0 < d)
    (s : ∀ y, a.Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' a.Model y (s y))) {n : ℕ} (hn : n ≠ 0) :
    sectionHomologyMap s hs n = 0 := by
…
```
Mentions: OAI.Kaplansky.LineStage, OAI.Kaplansky.ContinuousOrthonormalStageFrame, OAI.Kaplansky.sectionHomologyMap
def OAI.Kaplansky.canonicalProductHomologyMap line 48
Source documentation
The actual canonical hyperplane-product section induces this integral homology morphism. Its nonvanishing still requires a global calculation.
```
def canonicalProductHomologyMap (K : ι → ℕ) (n : ℕ) :=
…
```
theorem OAI.Kaplansky.canonicalProductHomologyMap_eq_section line 51
theorem OAI.Kaplansky.canonicalProductHomologyMap_eq_zero_of_nonvanishing line 62
Source documentation
Applied to the genuine hyperplane sum, a nowhere-zero continuous section would force the canonical map to vanish. No nonzero-map premise is introduced.
```
theorem canonicalProductHomologyMap_eq_zero_of_nonvanishing
    (s : ∀ y, (hyperplaneProductStage K).Fiber y)
    (hs : Continuous (fun y => TotalSpace.mk' (hyperplaneProductStage K).Model y (s y)))
    (hne : ∀ y, s y ≠ 0) {n : ℕ} (hn : n ≠ 0) :
    canonicalProductHomologyMap K n = 0 := by
…
```
Mentions: OAI.Kaplansky.hyperplaneProductStage, OAI.Kaplansky.canonicalProductHomologyMap
theorem OAI.Kaplansky.canonicalProductHomologyMap_eq_zero_of_frame line 74
theorem OAI.Kaplansky.hyperplaneProduct_nonzeroLocus line 84
theorem OAI.Kaplansky.canonicalProduct_mapsTo_nonzero line 90
def OAI.Kaplansky.canonicalProductRelativeHomologyMap line 100
Source documentation
Relative singular homology map on the genuinely punctured projective product.
```
def canonicalProductRelativeHomologyMap (n : ℕ) :=
…
```
theorem OAI.Kaplansky.canonicalProductRelativeHomology_comparison line 110
theorem OAI.Kaplansky.canonicalProductHomology_ne_zero_of_relativeClass line 122
Source documentation
Exact missing class obligation for the existing global map. This theorem is conditional and is not a proof of canonical nonvanishing.
```
theorem canonicalProductHomology_ne_zero_of_relativeClass (n : ℕ)
    (c : relativeSingularHomology
      (subspaceInclusion ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) (n+1))
    (hc : relativeHomologyBoundary
      (subspaceInclusion ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) n c = 0)
    (hne : canonicalProductRelativeHomologyMap K (n+1) c ≠ 0) :
    canonicalProductHomologyMap K (n+1) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.canonicalProductRelativeHomologyMap, OAI.Kaplansky.canonicalProductHomologyMap
def OAI.Kaplansky.canonicalProductCoordinateMap line 137
Source documentation
Actual section coordinate map as a continuous map on the full graph model.
```
def canonicalProductCoordinateMap :
    C(ProjectiveProductModel K, ((Σ i, Fin (K i)) → ℂ)) :=
…
```
theorem OAI.Kaplansky.canonicalProductCoordinateMap_nonzero line 145
def OAI.Kaplansky.canonicalProductCoordinateRelativeMap line 156
def OAI.Kaplansky.canonicalProductCoordinateRelativeIso line 165
Source documentation
The local coordinate map induces an isomorphism on genuine relative singular homology. This does not assert that these homology groups are nonzero.
```
def canonicalProductCoordinateRelativeIso (n : ℕ) :
    relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set (ProjectiveProductModel K))) n ≅
      relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set ((Σ i, Fin (K i)) → ℂ))) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.canonicalProductCoordinateRelativeIso_hom line 179
theorem OAI.Kaplansky.canonicalProductCoordinateRelativeMap_isIso line 190
theorem OAI.Kaplansky.canonicalProductGraphChart_target_univ line 202
def OAI.Kaplansky.canonicalProductChartHomeomorph line 209
Source documentation
The actual open neighborhood of the unique zero is homeomorphic to the full complex graph model, with the inherited topology on the neighborhood.
```
def canonicalProductChartHomeomorph :
    (canonicalProductGraphChart K).source ≃ₜ ProjectiveProductModel K :=
…
```
Mentions: OAI.Kaplansky.canonicalProductGraphChart
theorem OAI.Kaplansky.canonicalProductChartHomeomorph_apply line 215
theorem OAI.Kaplansky.canonicalProductChartHomeomorph_zero line 219
def OAI.Kaplansky.canonicalLocalSectionMap line 224
def OAI.Kaplansky.canonicalLocalSectionHomeomorph line 229
theorem OAI.Kaplansky.canonicalLocalSectionMap_eq line 233
theorem OAI.Kaplansky.canonicalLocalSectionHomeomorph_zero line 237
def OAI.Kaplansky.canonicalLocalRelativeHomologyIso line 246
Source documentation
Local section-coordinate isomorphism for the actual punctured chart, not just an abstract vector-space model. Excision into the full base is separate.
```
def canonicalLocalRelativeHomologyIso (n : ℕ) :
    relativeSingularHomology (subspaceInclusion
      ({⟨firstCoordinateProduct K, canonicalProduct_zero_in_chart K⟩}ᶜ :
        Set (canonicalProductGraphChart K).source)) n ≅
      relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set ((Σ i, Fin (K i)) → ℂ))) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.canonicalProduct_zero_in_chart, OAI.Kaplansky.canonicalProductGraphChart
def OAI.Kaplansky.canonicalChartRelativeInclusion line 259
Source documentation
Inclusion of the punctured chart into the punctured whole base. Its induced map is constructed; no excision isomorphism is asserted here.
```
def canonicalChartRelativeInclusion (n : ℕ) :=
…
```