HyperplaneFiber.lean`

67 declarations, 0 contain sorry, 0 declared as axioms

Hyperplane bundle charts, local-global comparison, and fiber normalization.

abbrev OAI.Kaplansky.canonicalBundleChartDomain line 19
theorem OAI.Kaplansky.canonical_chartBaseMap_eq line 23
def OAI.Kaplansky.canonicalGraphProjection line 27
theorem OAI.Kaplansky.canonicalGraphProjection_eq line 34
def OAI.Kaplansky.canonicalGraphVector line 39
theorem OAI.Kaplansky.canonicalGraphVector_mem line 42
theorem OAI.Kaplansky.canonicalGraphVector_ne_zero line 48
theorem OAI.Kaplansky.continuous_canonicalGraphVector line 52
def OAI.Kaplansky.canonicalBundleChartHomeomorph line 58
Source documentation
Actual bundle coordinates on the inverse image of the canonical base chart. This is a homeomorphism of the original total-space subspace.
```
def canonicalBundleChartHomeomorph : canonicalBundleChartDomain K ≃ₜ
    ProjectiveProductModel K × ((Σ i, Fin (K i)) → ℂ) :=
…
```
Mentions: OAI.Kaplansky.canonicalBundleChartDomain
theorem OAI.Kaplansky.canonicalBundleChartHomeomorph_base line 67
theorem OAI.Kaplansky.canonicalBundleChartHomeomorph_zero_iff line 71
def OAI.Kaplansky.canonicalRestrictedSection line 77
Source documentation
The restriction of the actual section, before applying bundle coordinates.
```
def canonicalRestrictedSection : C((canonicalProductGraphChart K).source, canonicalBundleChartDomain K) :=
…
```
Mentions: OAI.Kaplansky.canonicalProductGraphChart, OAI.Kaplansky.canonicalBundleChartDomain
theorem OAI.Kaplansky.canonicalBundleChartHomeomorph_section line 81
def OAI.Kaplansky.canonicalBundleChartNonzero line 118
def OAI.Kaplansky.canonicalBundleChartFiberIso line 122
Source documentation
Normalization of the genuine target over the canonical contractible chart. It is obtained from actual bundle evaluation and product projection.
```
def canonicalBundleChartFiberIso (n : ℕ) :
    relativeSingularHomology (subspaceInclusion (canonicalBundleChartNonzero K)) n ≅
      relativeSingularHomology
        (subspaceInclusion ({0}ᶜ : Set ((Σ i, Fin (K i)) → ℂ))) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.canonicalBundleChartNonzero
theorem OAI.Kaplansky.canonicalRestrictedSection_mapsTo_nonzero line 131
def OAI.Kaplansky.canonicalRestrictedSectionRelativeMap line 138
theorem OAI.Kaplansky.canonicalRestrictedSectionRelativeMap_normalization line 148
Source documentation
Compatibility of the ACTUAL restricted section with the preserved local coordinate homology isomorphism. This is not just a derivative sign.
```
theorem canonicalRestrictedSectionRelativeMap_normalization (n : ℕ) :
    canonicalRestrictedSectionRelativeMap K n ≫ (canonicalBundleChartFiberIso K n).hom =
      (canonicalLocalRelativeHomologyIso K n).hom := by
…
```
Mentions: OAI.Kaplansky.canonicalRestrictedSectionRelativeMap, OAI.Kaplansky.canonicalBundleChartFiberIso, OAI.Kaplansky.canonicalLocalRelativeHomologyIso
theorem OAI.Kaplansky.canonicalRestrictedSectionRelativeMap_isIso line 167
Source documentation
The actual section induces an isomorphism to the bundle relative homology OVER THIS CHART in every degree. Global inclusion is separate.
```
theorem canonicalRestrictedSectionRelativeMap_isIso (n : ℕ) :
    IsIso (canonicalRestrictedSectionRelativeMap K n) := by
…
```
Mentions: OAI.Kaplansky.canonicalRestrictedSectionRelativeMap
def OAI.Kaplansky.canonicalRestrictedSectionRelativeIso line 176
def OAI.Kaplansky.canonicalBundleChartTopHomologyIso line 182
Source documentation
Top relative homology over the actual bundle chart is ℤ, normalized using precisely the incoming recursive local generator.
```
def canonicalBundleChartTopHomologyIso (hp : 0 < ∑ i, K i) :
    relativeSingularHomology (subspaceInclusion (canonicalBundleChartNonzero K))
      (2*(∑ i, K i)) ≅ ModuleCat.of ℤ ℤ :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.canonicalBundleChartNonzero
def OAI.Kaplansky.canonicalBundleChartGenerator line 188
theorem OAI.Kaplansky.canonicalBundleChartGenerator_coordinate line 193
theorem OAI.Kaplansky.canonicalBundleChartGenerator_ne_zero line 202
def OAI.Kaplansky.canonicalBundleChartRelativeInclusion line 211
Source documentation
Actual inclusion of the bundle over the canonical chart into the whole ordinary bundle, always removing the entire respective zero section.
```
def canonicalBundleChartRelativeInclusion (n : ℕ) :=
…
```
theorem OAI.Kaplansky.canonicalRestrictedSection_global_square line 219
theorem OAI.Kaplansky.canonicalBundleChartGenerator_global_image line 228
theorem OAI.Kaplansky.canonicalBundleChartGenerator_compactified_image line 242
Source documentation
The same equality in the exact incoming compactified target pair.
```
theorem canonicalBundleChartGenerator_compactified_image (hp : 0 < ∑ i, K i) :
    bundleCompactificationRelativeMap (V := (hyperplaneProductStage K).Model)
…
```
Mentions: OAI.Kaplansky.bundleCompactificationRelativeMap, OAI.Kaplansky.hyperplaneProductStage
theorem OAI.Kaplansky.canonicalFundamentalClass_target_image line 254
Source documentation
Evaluation of the actual global section on the preserved fundamental class, after passing to target relative homology, is this precise chart image.
```
theorem canonicalFundamentalClass_target_image (hp : 0 < ∑ i, K i) :
    absoluteToRelative (subspaceInclusion
      (compactifiedNonzeroBundle (V := (hyperplaneProductStage K).Model)
…
```
Mentions: OAI.Kaplansky.absoluteToRelative, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.compactifiedNonzeroBundle, OAI.Kaplansky.hyperplaneProductStage
def OAI.Kaplansky.canonicalChartFiberEmbedding line 281
Source documentation
The actual fiber over the canonical point, embedded using the proved bundle coordinates. Only the base coordinate is fixed.
```
def canonicalChartFiberEmbedding :
    C(((Σ i, Fin (K i)) → ℂ), canonicalBundleChartDomain K) :=
…
```
Mentions: OAI.Kaplansky.canonicalBundleChartDomain
theorem OAI.Kaplansky.canonicalChartFiberEmbedding_base line 287
theorem OAI.Kaplansky.canonicalChartFiberEmbedding_mapsTo_nonzero line 294
def OAI.Kaplansky.canonicalChartFiberRelativeMap line 304
theorem OAI.Kaplansky.canonicalChartFiberRelativeMap_normalization line 312
Source documentation
Fiber inclusion is the inverse of the proved local bundle normalization. This identifies the normalization geometrically at chain-map level.
```
theorem canonicalChartFiberRelativeMap_normalization (n : ℕ) :
    canonicalChartFiberRelativeMap K n ≫ (canonicalBundleChartFiberIso K n).hom = 𝟙 _ := by
…
```
Mentions: OAI.Kaplansky.canonicalChartFiberRelativeMap, OAI.Kaplansky.canonicalBundleChartFiberIso
theorem OAI.Kaplansky.canonicalChartFiberRelativeMap_eq_inv line 324
theorem OAI.Kaplansky.canonicalChartFiberRelativeMap_isIso line 329
def OAI.Kaplansky.canonicalFiberGenerator line 336
Source documentation
The preserved recursive local class, now expressed in the actual fiber coordinate group. Its normalization is transported, never independently chosen.
```
def canonicalFiberGenerator (hp : 0 < ∑ i, K i) :
    relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set ((Σ i, Fin (K i)) → ℂ)))
      (2*(∑ i, K i)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.canonicalFiberGenerator_ne_zero line 341
theorem OAI.Kaplansky.canonicalFiberGenerator_chart_image line 348
def OAI.Kaplansky.canonicalWholeBundleFiberMap line 355
Source documentation
Actual inclusion of this one fiber into the ordinary whole-bundle pair.
```
def canonicalWholeBundleFiberMap (n : ℕ) :=
…
```
theorem OAI.Kaplansky.canonicalFiberGenerator_whole_image line 360
Source documentation
The incoming target obligation is the survival of the preserved class under inclusion of a single actual fiber. All local comparisons are proved.
```
theorem canonicalFiberGenerator_whole_image (hp : 0 < ∑ i, K i) :
    canonicalWholeBundleFiberMap K (2*(∑ i, K i)) (canonicalFiberGenerator K hp) =
      canonicalProductOrdinaryRelativeMap K (2*(∑ i, K i))
        (canonicalProductLocalGenerator K hp) := by
…
```
Mentions: OAI.Kaplansky.canonicalWholeBundleFiberMap, OAI.Kaplansky.canonicalFiberGenerator, OAI.Kaplansky.canonicalProductOrdinaryRelativeMap, OAI.Kaplansky.canonicalProductLocalGenerator
theorem OAI.Kaplansky.canonicalBundleChartHomology_isZero line 370
Source documentation
Homology of the actual chart target pair is concentrated in its fiber dimension. This includes vanishing in degrees zero and one when p>0.
```
theorem canonicalBundleChartHomology_isZero (hp : 0 < ∑ i, K i) (n : ℕ)
    (hn : n ≠ 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology (subspaceInclusion (canonicalBundleChartNonzero K)) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.canonicalBundleChartNonzero
theorem OAI.Kaplansky.canonicalBundleChartGenerator_spans line 379
def OAI.Kaplansky.canonicalPuncturedBundle line 388
Source documentation
The complement of the entire canonical fiber, an open subset of the actual hyperplane bundle total space.
```
def canonicalPuncturedBundle :
    Set (TotalSpace (hyperplaneProductStage K).Model (hyperplaneProductStage K).Fiber) :=
…
```
Mentions: OAI.Kaplansky.hyperplaneProductStage
theorem OAI.Kaplansky.canonicalBundleChartDomain_open line 392
theorem OAI.Kaplansky.canonicalPuncturedBundle_open line 395
theorem OAI.Kaplansky.canonicalBundle_chart_punctured_cover line 398
def OAI.Kaplansky.canonicalBundleCoverChartIso line 411
Source documentation
The removed-subspace convention in the general gluing theorem is identified with the preserved actual chart pair, with identity ambient map.
```
def canonicalBundleCoverChartIso (n : ℕ) :
    relativeSingularHomology (subspaceInclusion (canonicalBundleChartNonzero K)) n ≅
    relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' nonzeroBundle : Set (canonicalBundleChartDomain K))) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.canonicalBundleChartNonzero, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleChartDomain
theorem OAI.Kaplansky.canonicalBundleCoverChartIso_inclusion line 418
def OAI.Kaplansky.canonicalBundleCoverGenerator line 431
Source documentation
The incoming normalized generator, merely transported to the general relative-cover convention. No new generator or orientation is chosen.
```
def canonicalBundleCoverGenerator (hp : 0 < ∑ i, K i) :=
…
```
theorem OAI.Kaplansky.canonicalBundleCoverGenerator_ne_zero line 434
theorem OAI.Kaplansky.canonicalBundleCoverGenerator_whole_image line 441

theorem OAI.Kaplansky.canonicalFiberGenerator_zero_iff_overlap line 454

Source documentation

Exact global obstruction to survival, in the actual two-set bundle cover. Local nonvanishing alone does not exclude this overlap witness.

theorem canonicalFiberGenerator_zero_iff_overlap (hp : 0 < ∑ i, K i) :
    canonicalWholeBundleFiberMap K (2*(∑ i,K i)) (canonicalFiberGenerator K hp) = 0 ↔
    ∃ w : relativeSingularHomology (subspaceInclusion
        (Subtype.val ⁻¹' nonzeroBundle :
          Set ↥(canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K))) (2*(∑ i,K i)),
      restrictedPairHomologyMap (Set.inter_subset_left :
        canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K ⊆ canonicalBundleChartDomain K)
        nonzeroBundle (2*(∑ i,K i)) w = canonicalBundleCoverGenerator K hp ∧
      restrictedPairHomologyMap (Set.inter_subset_right :
        canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K ⊆ canonicalPuncturedBundle K)
        nonzeroBundle (2*(∑ i,K i)) w = 0 := by
…

Mentions: OAI.Kaplansky.canonicalWholeBundleFiberMap, OAI.Kaplansky.canonicalFiberGenerator, OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle, OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.canonicalBundleCoverGenerator

theorem OAI.Kaplansky.canonicalBundleChart_first_zero_iff line 470
def OAI.Kaplansky.firstCoordinateSubspaceHomeomorph line 479
def OAI.Kaplansky.canonicalBundleOverlapHomeomorph line 492
Source documentation
Actual coordinates on the overlap with the punctured bundle. Its base is punctured Euclidean space, not a contractible base.
```
def canonicalBundleOverlapHomeomorph :
    ↥(canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K) ≃ₜ
      ({0}ᶜ : Set (ProjectiveProductModel K)) × ((Σ i, Fin (K i)) → ℂ) :=
…
```
Mentions: OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle
theorem OAI.Kaplansky.canonicalBundleOverlapHomeomorph_fiber line 506
theorem OAI.Kaplansky.canonicalBundleOverlapHomeomorph_nonzero_iff line 511
def OAI.Kaplansky.canonicalBundleOverlapRelativeIso line 519
Source documentation
A pair homeomorphism, retaining both the punctured base and the punctured fiber. This supplies no unjustified projection isomorphism.
```
def canonicalBundleOverlapRelativeIso (n : ℕ) :
    relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' nonzeroBundle :
        Set ↥(canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K))) n ≅
    relativeSingularHomology (subspaceInclusion
      {z : ({0}ᶜ : Set (ProjectiveProductModel K)) × ((Σ i, Fin (K i)) → ℂ) | z.2 ≠ 0}) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle
theorem OAI.Kaplansky.canonicalBundleOverlap_fiber_comparison line 530
Source documentation
The overlap-to-chart map followed by chart normalization is exactly projection to the fiber in these genuine product coordinates.
```
theorem canonicalBundleOverlap_fiber_comparison (n : ℕ) :
    restrictedPairHomologyMap (Set.inter_subset_left :
      canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K ⊆ canonicalBundleChartDomain K)
      nonzeroBundle n ≫ (canonicalBundleCoverChartIso K n).inv ≫
        (canonicalBundleChartFiberIso K n).hom =
    (canonicalBundleOverlapRelativeIso K n).hom ≫
      productPairProjection (B := ({0}ᶜ : Set (ProjectiveProductModel K)))
…
```
Mentions: OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleCoverChartIso, OAI.Kaplansky.canonicalBundleChartFiberIso, OAI.Kaplansky.canonicalBundleOverlapRelativeIso, OAI.Kaplansky.productPairProjection
def OAI.Kaplansky.canonicalBundleCoverTopHomologyIso line 571
theorem OAI.Kaplansky.canonicalBundleCoverGenerator_coordinate line 578
def OAI.Kaplansky.canonicalOverlapChartMap line 585
def OAI.Kaplansky.canonicalOverlapPuncturedMap line 590
def OAI.Kaplansky.canonicalOverlapNormalization line 597
Source documentation
The preserved integer normalization measured through the actual overlap-to-chart map. It is not a global Thom class.
```
def canonicalOverlapNormalization (hp : 0 < ∑ i, K i) :=
…
```
theorem OAI.Kaplansky.canonicalOverlap_normalization_eq_one_iff line 600
theorem OAI.Kaplansky.canonicalFiberGenerator_zero_iff_normalized_overlap line 614
Source documentation
Exact test for failure of the incoming global survival obligation. Excluding this normalized overlap witness is still a genuine global problem.
```
theorem canonicalFiberGenerator_zero_iff_normalized_overlap (hp : 0 < ∑ i, K i) :
    canonicalWholeBundleFiberMap K (2*(∑ i,K i)) (canonicalFiberGenerator K hp) = 0 ↔
      ∃ w : relativeSingularHomology (subspaceInclusion
        (Subtype.val ⁻¹' nonzeroBundle :
          Set ↥(canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K))) (2*(∑ i,K i)),
        canonicalOverlapNormalization K hp w = (1 : ℤ) ∧
        canonicalOverlapPuncturedMap K (2*(∑ i,K i)) w = 0 := by
…
```
Mentions: OAI.Kaplansky.canonicalWholeBundleFiberMap, OAI.Kaplansky.canonicalFiberGenerator, OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle, OAI.Kaplansky.canonicalOverlapNormalization, OAI.Kaplansky.canonicalOverlapPuncturedMap