ProductCover.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Product-pair fiber normalization, punctured products, and overlap generators.

def OAI.Kaplansky.signedCoordinateHalfspace line 19
Source documentation
A finite signed halfspace cover, using actual continuous linear coordinates.
```
def signedCoordinateHalfspace (i : Fin (Module.finrank ℝ E) × Bool) : Set E :=
…
```
theorem OAI.Kaplansky.signedCoordinateHalfspace_open line 23
theorem OAI.Kaplansky.signedCoordinateHalfspace_convex line 29
theorem OAI.Kaplansky.signedCoordinateHalfspaces_cover line 40
Source documentation
The signed coordinate halfspaces cover exactly the punctured space.
```
theorem signedCoordinateHalfspaces_cover :
    (⋃ i : Fin (Module.finrank ℝ E) × Bool, signedCoordinateHalfspace i) = ({0}ᶜ : Set E) := by
…
```
Mentions: OAI.Kaplansky.signedCoordinateHalfspace
theorem OAI.Kaplansky.signedCoordinateIntersection_convex line 62
Source documentation
Every finite intersection is genuinely convex, hence contractible whenever it is nonempty.
```
theorem signedCoordinateIntersection_convex
    (T : Finset (Fin (Module.finrank ℝ E) × Bool)) :
    Convex ℝ (⋂ i ∈ T, signedCoordinateHalfspace (E := E) i) :=
…
```
Mentions: OAI.Kaplansky.signedCoordinateHalfspace

theorem OAI.Kaplansky.convexBaseProductPair_below_isZero line 78

Source documentation

A convex base, including the empty case, has no relative bundle homology below the fiber dimension.

theorem convexBaseProductPair_below_isZero (C : Set E) (hC : Convex ℝ C)
    (hd : 2 ≤ Module.finrank ℝ V) (n : ℕ) (hn : n < Module.finrank ℝ V) :
    IsZero (relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' {z : E × V | z.2 ≠ 0} : Set {z : E × V | z.1 ∈ C})) n) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion

theorem OAI.Kaplansky.puncturedBaseProductPair_below_isZero line 95
Source documentation
Actual relative homology over a punctured vector-space base vanishes below the fiber dimension. This does NOT identify its top group or assert that the punctured base is contractible.
```
theorem puncturedBaseProductPair_below_isZero
    (hd : 2 ≤ Module.finrank ℝ V) (n : ℕ) (hn : n < Module.finrank ℝ V) :
    IsZero (relativeSingularHomology (subspaceInclusion
      {z : ({0}ᶜ : Set E) × V | z.2 ≠ 0}) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.canonicalBundleOverlap_below_isZero line 132
Source documentation
The actual canonical overlap has zero homology below its real fiber rank. In particular this discharges the PRECEDING-overlap vanishing hypothesis in the preserved normalization-gluing theorem.
```
theorem canonicalBundleOverlap_below_isZero (hp : 0 < ∑ i, K i)
    (n : ℕ) (hn : n < 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' nonzeroBundle :
        Set ↥(canonicalBundleChartDomain K ∩ canonicalPuncturedBundle K))) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.canonicalBundleChartDomain, OAI.Kaplansky.canonicalPuncturedBundle
def OAI.Kaplansky.productPairBaseSubsetIso line 151
Source documentation
Relative product coordinates over an arbitrary subset of the base.
```
def productPairBaseSubsetIso (C : Set B) (W : Set V) (n : ℕ) :=
…
```
def OAI.Kaplansky.productPairChartFiberMap line 157
Source documentation
A fiber inside a restricted product chart.
```
def productPairChartFiberMap (C : Set B) (b : C) (W : Set V) (n : ℕ) :=
…
```
theorem OAI.Kaplansky.productPairChartFiberMap_coordinates line 166
theorem OAI.Kaplansky.productPairChartFiberMap_isIso line 175
theorem OAI.Kaplansky.productPairChartFiberMap_inclusion line 187
Source documentation
Inclusion of a chart fiber is literally the same global fiber inclusion.
```
theorem productPairChartFiberMap_inclusion (C : Set B) (b : C) (W : Set V) (n : ℕ) :
    productPairChartFiberMap C b W n ≫
      restrictedPairToAmbientHomologyMap {z : B × V | z.1 ∈ C} {z | z.2 ∈ W} n =
    productPairFiberMap b.1 W n := by
…
```
Mentions: OAI.Kaplansky.productPairChartFiberMap, OAI.Kaplansky.restrictedPairToAmbientHomologyMap, OAI.Kaplansky.productPairFiberMap

theorem OAI.Kaplansky.productPairProjection_fiber_of_finite_cover line 209

Source documentation

A finite cover by contractible base charts proves fiber generation in the first potentially nonzero relative degree, provided the preceding intersection groups vanish. All maps are the actual product projection and fiber inclusion; path connectedness fixes the SAME fiber class on all charts.

theorem productPairProjection_fiber_of_finite_cover (S : Finset ι) (U : ι → Set B)
    (hopen : ∀ i ∈ S, IsOpen (U i)) (hcover : (⋃ i ∈ S, U i) = Set.univ)
    (hchart : ∀ i ∈ S, (U i).Nonempty → ContractibleSpace (U i))
    (W : Set V) (n : ℕ)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion {z : (⋂ i ∈ T, U i) × V | z.2 ∈ W}) q))
    (b : B) :
    productPairProjection (B := B) W (n+1) ≫ productPairFiberMap b W (n+1) = 𝟙 _ := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.productPairProjection, OAI.Kaplansky.productPairFiberMap

theorem OAI.Kaplansky.productPairProjection_isIso_of_finite_cover line 249

Source documentation

In this degree the actual product projection is an isomorphism.

theorem productPairProjection_isIso_of_finite_cover (S : Finset ι) (U : ι → Set B)
    (hopen : ∀ i ∈ S, IsOpen (U i)) (hcover : (⋃ i ∈ S, U i) = Set.univ)
    (hchart : ∀ i ∈ S, (U i).Nonempty → ContractibleSpace (U i))
    (W : Set V) (n : ℕ)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion {z : (⋂ i ∈ T, U i) × V | z.2 ∈ W}) q)) :
    IsIso (productPairProjection (B := B) W (n+1)) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.productPairProjection

theorem OAI.Kaplansky.signedCoordinateHalfspace_subset_punctured line 269
Source documentation
Signed halfspaces avoid the origin.
```
theorem signedCoordinateHalfspace_subset_punctured
    (i : Fin (Module.finrank ℝ E) × Bool) :
    signedCoordinateHalfspace i ⊆ ({0}ᶜ : Set E) := by
…
```
Mentions: OAI.Kaplansky.signedCoordinateHalfspace
theorem OAI.Kaplansky.puncturedBaseProductPairProjection_isIso line 280
Source documentation
In the real fiber dimension, projection from the punctured-base product pair is an isomorphism. Both base and fiber have dimension at least two. This is proved by finite convex charts, relative vanishing and path transport of actual fiber inclusions, not by a Künneth or Thom assumption.
```
theorem puncturedBaseProductPairProjection_isIso
    (he : 2 ≤ Module.finrank ℝ E) (hv : 2 ≤ Module.finrank ℝ V) :
    IsIso (productPairProjection (B := ({0}ᶜ : Set E)) ({0}ᶜ : Set V)
…
```
Mentions: OAI.Kaplansky.productPairProjection
theorem OAI.Kaplansky.canonicalOverlapChartMap_isIso line 339
Source documentation
The ACTUAL overlap-to-chart map is an isomorphism in the fiber degree. This assertion is confined to that degree.
```
theorem canonicalOverlapChartMap_isIso (hp : 0 < ∑ i, K i) :
    IsIso (canonicalOverlapChartMap K (2*(∑ i, K i))) := by
…
```
Mentions: OAI.Kaplansky.canonicalOverlapChartMap
theorem OAI.Kaplansky.canonicalOverlapNormalization_isIso line 359
Source documentation
The overlap normalization is an actual isomorphism to ℤ, using the incoming chart generator, not an independently chosen orientation.
```
theorem canonicalOverlapNormalization_isIso (hp : 0 < ∑ i, K i) :
    IsIso (canonicalOverlapNormalization K hp) := by
…
```
Mentions: OAI.Kaplansky.canonicalOverlapNormalization
def OAI.Kaplansky.canonicalOverlapTopIso line 365
def OAI.Kaplansky.canonicalNormalizedOverlapGenerator line 369
Source documentation
The unique overlap class with preserved normalization one.
```
def canonicalNormalizedOverlapGenerator (hp : 0 < ∑ i, K i) :=
…
```
theorem OAI.Kaplansky.canonicalNormalizedOverlapGenerator_coordinate line 372
theorem OAI.Kaplansky.canonicalNormalizedOverlapGenerator_unique line 376
theorem OAI.Kaplansky.canonicalNormalizedOverlapGenerator_ne_zero line 385
theorem OAI.Kaplansky.canonicalNormalizedOverlapGenerator_spans line 392
theorem OAI.Kaplansky.canonicalFiberGenerator_zero_iff_overlapGenerator line 405
Source documentation
The incoming global survival problem reduces to the image of this ONE proved primitive overlap class. Its image in the punctured bundle is still a global obligation, not supplied by the overlap isomorphism.
```
theorem canonicalFiberGenerator_zero_iff_overlapGenerator (hp : 0 < ∑ i, K i) :
    canonicalWholeBundleFiberMap K (2*(∑ i, K i)) (canonicalFiberGenerator K hp) = 0 ↔
      canonicalOverlapPuncturedMap K (2*(∑ i, K i))
        (canonicalNormalizedOverlapGenerator K hp) = 0 := by
…
```
Mentions: OAI.Kaplansky.canonicalWholeBundleFiberMap, OAI.Kaplansky.canonicalFiberGenerator, OAI.Kaplansky.canonicalOverlapPuncturedMap, OAI.Kaplansky.canonicalNormalizedOverlapGenerator