GraphNormalization.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Bundle graph coordinates and natural finite-graph normalization.

abbrev OAI.Kaplansky.graphBundleDomain line 18
def OAI.Kaplansky.graphBundleBaseProjection line 21
def OAI.Kaplansky.graphBundleLineVector line 29
theorem OAI.Kaplansky.graphBundleLineVector_mem line 32
theorem OAI.Kaplansky.graphBundleLineVector_ne_zero line 45
theorem OAI.Kaplansky.continuous_graphBundleLineVector line 48
def OAI.Kaplansky.graphBundleCoordinates line 59
Source documentation
Coordinates on the ORIGINAL hyperplane-sum total space restricted to any subset of an actual graph chart. The fiber is evaluated on an explicit nonvanishing graph representative.
```
def graphBundleCoordinates : graphBundleDomain K U ≃ₜ A × ((Σ i, Fin (K i)) → ℂ) :=
…
```
Mentions: OAI.Kaplansky.graphBundleDomain
theorem OAI.Kaplansky.graphBundleCoordinates_base line 66
theorem OAI.Kaplansky.graphBundleCoordinates_zero_iff line 69
def OAI.Kaplansky.graphBundleRelativeIso line 75
def OAI.Kaplansky.graphBundleNormalization line 83
Source documentation
Local normalization in integral fiber homology of the actual bundle pair. Choice of graph frame and gluing are proved separately.
```
def graphBundleNormalization (n : ℕ) :=
…
```
def OAI.Kaplansky.graphBundlePullbackRelativeIso line 96
Source documentation
Pullback coordinates retain the same fiber and removed zero section.
```
def graphBundlePullbackRelativeIso (n : ℕ) :=
…
```
theorem OAI.Kaplansky.graphBundleNormalization_pullback line 108
Source documentation
This factorization uses the original restricted total space on its left and the actual evaluation-pullback bundle on its right.
```
theorem graphBundleNormalization_pullback (F : ∀ i, GraphFrame 1 (K i))
    (hF : U ⊆ (projectiveProductGraphChart K F).source) (n : ℕ) :
    graphBundleNormalization K U e F hF n =
      (graphBundlePullbackRelativeIso K U e n).hom ≫
        finiteLineEvaluationNormalization (graphBundleBaseProjection K U e)
          (graphBundleLineVector K U e F) (graphBundleLineVector_mem K U e F hF)
          (graphBundleLineVector_ne_zero K U e F) (continuous_graphBundleLineVector K U e F hF) n := by
…
```
Mentions: OAI.Kaplansky.graphBundleNormalization, OAI.Kaplansky.graphBundlePullbackRelativeIso, OAI.Kaplansky.finiteLineEvaluationNormalization, OAI.Kaplansky.graphBundleBaseProjection, OAI.Kaplansky.graphBundleLineVector, OAI.Kaplansky.graphBundleLineVector_mem, OAI.Kaplansky.graphBundleLineVector_ne_zero, OAI.Kaplansky.continuous_graphBundleLineVector

theorem OAI.Kaplansky.graphBundleNormalization_affine_eq line 135

Source documentation

Two graph frames give the SAME normalization of the actual restricted bundle whenever its base coordinates are a finite affine complement. All transition and lower-vanishing obligations are discharged.

theorem graphBundleNormalization_affine_eq
    (l : J → E →L[ℝ] F) (c : J → F) (a : U ≃ₜ affineAvoidanceSet l c)
    (F₁ F₂ : ∀ i, GraphFrame 1 (K i))
    (h₁ : U ⊆ (projectiveProductGraphChart K F₁).source)
    (h₂ : U ⊆ (projectiveProductGraphChart K F₂).source)
    (hp : 0 < ∑ i, K i) :
    graphBundleNormalization K U a F₁ h₁ (2*(∑ i, K i)) =
      graphBundleNormalization K U a F₂ h₂ (2*(∑ i, K i)) := by
…

Mentions: OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.graphBundleNormalization

theorem OAI.Kaplansky.graphBundleIntersection_below_isZero line 159

Source documentation

The original hyperplane bundle pair over any finite graph-chart intersection has no homology below its real fiber rank.

theorem graphBundleIntersection_below_isZero
    (F₀ : ∀ i, GraphFrame 1 (K i)) (G : L → ∀ i, GraphFrame 1 (K i))
    (hp : 0 < ∑ i, K i) (q : ℕ) (hq : q < 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' nonzeroBundle :
        Set (graphBundleDomain K (projectiveProductGraphIntersection K F₀ G)))) q) := by
…

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

theorem OAI.Kaplansky.graphBundleIntersection_normalization_eq line 175

Source documentation

On an actual finite graph-chart intersection the local normalization is independent of every graph frame containing that intersection.

theorem graphBundleIntersection_normalization_eq
    (F₀ : ∀ i, GraphFrame 1 (K i)) (G : L → ∀ i, GraphFrame 1 (K i))
    (F₁ F₂ : ∀ i, GraphFrame 1 (K i))
    (h₁ : projectiveProductGraphIntersection K F₀ G ⊆ (projectiveProductGraphChart K F₁).source)
    (h₂ : projectiveProductGraphIntersection K F₀ G ⊆ (projectiveProductGraphChart K F₂).source)
    (hp : 0 < ∑ i, K i) :
    graphBundleNormalization K (projectiveProductGraphIntersection K F₀ G)
        (projectiveProductGraphIntersectionHomeomorph K F₀ G) F₁ h₁ (2*(∑ i, K i)) =
      graphBundleNormalization K (projectiveProductGraphIntersection K F₀ G)
        (projectiveProductGraphIntersectionHomeomorph K F₀ G) F₂ h₂ (2*(∑ i, K i)) :=
…

Mentions: OAI.Kaplansky.graphBundleNormalization

theorem OAI.Kaplansky.graphBundleCoordinates_restrict_fiber line 201
Source documentation
The fiber coordinate depends only on the original base point, fiber vector and graph frame, and not on the chosen base coordinates.
```
theorem graphBundleCoordinates_restrict_fiber (z : graphBundleDomain K U) :
    (graphBundleCoordinates K V f F hF ⟨z.1,h z.2⟩).2 =
      (graphBundleCoordinates K U e F (h.trans hF) z).2 := by
…
```
Mentions: OAI.Kaplansky.graphBundleDomain, OAI.Kaplansky.graphBundleCoordinates
theorem OAI.Kaplansky.graphBundleNormalization_restrict line 220
Source documentation
Restriction of the normalization on a larger chart is exactly the normalization of the smaller actual bundle pair, in any base coordinates.
```
theorem graphBundleNormalization_restrict (n : ℕ) :
    restrictedPairHomologyMap (fun _ hz => h hz : graphBundleDomain K U ⊆ graphBundleDomain K V)
        nonzeroBundle n ≫ graphBundleNormalization K V f F hF n =
      graphBundleNormalization K U e F (h.trans hF) n := by
…
```
Mentions: OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.graphBundleDomain, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.graphBundleNormalization
abbrev OAI.Kaplansky.graphBundleChartDomain line 243
def OAI.Kaplansky.graphBundleChartNormalization line 246

theorem OAI.Kaplansky.graphBundleChartNormalization_compatible line 252

Source documentation

The local integral fiber normalizations agree after the actual inclusions from a pairwise intersection of total-space charts.

theorem graphBundleChartNormalization_compatible
    (F G : ∀ i, GraphFrame 1 (K i)) (hp : 0 < ∑ i, K i) :
    restrictedPairHomologyMap (inter_subset_left :
      graphBundleChartDomain K F ∩ graphBundleChartDomain K G ⊆ graphBundleChartDomain K F)
      nonzeroBundle (2*(∑ i, K i)) ≫ graphBundleChartNormalization K F (2*(∑ i, K i)) =
    restrictedPairHomologyMap (inter_subset_right :
      graphBundleChartDomain K F ∩ graphBundleChartDomain K G ⊆ graphBundleChartDomain K G)
      nonzeroBundle (2*(∑ i, K i)) ≫ graphBundleChartNormalization K G (2*(∑ i, K i)) := by
…

Mentions: OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.graphBundleChartDomain, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.graphBundleChartNormalization

theorem OAI.Kaplansky.graphBundleChartIntersection_below_isZero line 280
Source documentation
All finite nonempty intersections of the total-space graph charts have the required lower relative vanishing.
```
theorem graphBundleChartIntersection_below_isZero
    (T : Finset (∀ i, GraphFrame 1 (K i))) (ht : T.Nonempty)
    (hp : 0 < ∑ i, K i) (q : ℕ) (hq : q < 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' nonzeroBundle : Set ↥(⋂ F ∈ T, graphBundleChartDomain K F))) q) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.graphBundleChartDomain

theorem OAI.Kaplansky.hyperplaneBundle_exists_global_normalization line 303

Source documentation

A genuine normalization on the WHOLE actual hyperplane bundle pair, agreeing with the normalization on any preselected graph chart.

theorem hyperplaneBundle_exists_global_normalization
    (F₀ : ∀ i, GraphFrame 1 (K i)) (hp : 0 < ∑ i, K i) :
    ∃ f : relativeSingularHomology
        (subspaceInclusion (nonzeroBundle : Set (TotalSpace (hyperplaneProductStage K).Model
          (hyperplaneProductStage K).Fiber))) (2*(∑ i, K i)) ⟶
        relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set ((Σ i, Fin (K i)) → ℂ)))
          (2*(∑ i, K i)),
      restrictedPairToAmbientHomologyMap (graphBundleChartDomain K F₀) nonzeroBundle
          (2*(∑ i, K i)) ≫ f = graphBundleChartNormalization K F₀ (2*(∑ i, K i)) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.hyperplaneProductStage, OAI.Kaplansky.restrictedPairToAmbientHomologyMap, OAI.Kaplansky.graphBundleChartDomain, OAI.Kaplansky.graphBundleChartNormalization