Normalization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Twisted bundle graph normalization and its naturality.

theorem OAI.Kaplansky.twistedCoordinateSpace_real_finrank line 17
def OAI.Kaplansky.twistedGraphBundlePullbackRelativeIso line 22
theorem OAI.Kaplansky.twistedGraphBundleNormalization_pullback line 31
theorem OAI.Kaplansky.twistedGraphBundleNormalization_affine_eq line 57
theorem OAI.Kaplansky.twistedGraphBundleIntersection_below_isZero line 79
theorem OAI.Kaplansky.twistedGraphBundleCoordinates_restrict_fiber line 112
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 twistedGraphBundleCoordinates_restrict_fiber (z : twistedGraphBundleDomain K r U) :
    (twistedGraphBundleCoordinates K r V f F hF ⟨z.1,h z.2⟩).2 =
      (twistedGraphBundleCoordinates K r U e F (h.trans hF) z).2 := by
…
```
Mentions: OAI.Kaplansky.twistedGraphBundleDomain, OAI.Kaplansky.twistedGraphBundleCoordinates
theorem OAI.Kaplansky.twistedGraphBundleNormalization_restrict line 140
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 twistedGraphBundleNormalization_restrict (n : ℕ) :
    restrictedPairHomologyMap (fun _ hz => h hz : twistedGraphBundleDomain K r U ⊆ twistedGraphBundleDomain K r V)
        nonzeroBundle n ≫ twistedGraphBundleNormalization K r V f F hF n =
      twistedGraphBundleNormalization K r U e F (h.trans hF) n := by
…
```
Mentions: OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.twistedGraphBundleDomain, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.twistedGraphBundleNormalization
abbrev OAI.Kaplansky.twistedGraphBundleChartDomain line 166
def OAI.Kaplansky.twistedGraphBundleChartNormalization line 169

theorem OAI.Kaplansky.twistedGraphBundleChartNormalization_compatible line 175

Source documentation

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

theorem twistedGraphBundleChartNormalization_compatible
    (F G : ∀ i, GraphFrame 1 (twistedProjectiveDimensions K h i)) (hp : 0 < h+∑ i, K i) :
    restrictedPairHomologyMap (inter_subset_left :
      twistedGraphBundleChartDomain K h F ∩ twistedGraphBundleChartDomain K h G ⊆ twistedGraphBundleChartDomain K h F)
      nonzeroBundle (2*(h+∑ i, K i)) ≫ twistedGraphBundleChartNormalization K h F (2*(h+∑ i, K i)) =
    restrictedPairHomologyMap (inter_subset_right :
      twistedGraphBundleChartDomain K h F ∩ twistedGraphBundleChartDomain K h G ⊆ twistedGraphBundleChartDomain K h G)
      nonzeroBundle (2*(h+∑ i, K i)) ≫ twistedGraphBundleChartNormalization K h G (2*(h+∑ i, K i)) := by
…

Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.twistedGraphBundleChartDomain, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.twistedGraphBundleChartNormalization

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

theorem OAI.Kaplansky.twistedHyperplaneBundle_exists_global_normalization line 226

Source documentation

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

theorem twistedHyperplaneBundle_exists_global_normalization
    (F₀ : ∀ i, GraphFrame 1 (twistedProjectiveDimensions K h i)) (hp : 0 < h+∑ i, K i) :
    ∃ f : relativeSingularHomology
        (subspaceInclusion (nonzeroBundle : Set (TotalSpace (EuclideanSpace ℂ (TwistedHyperplaneSlot K h))
          (twistedHyperplaneSumCore K h).Fiber))) (2*(h+∑ i, K i)) ⟶
        relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set (TwistedHyperplaneSlot K h → ℂ)))
          (2*(h+∑ i, K i)),
      restrictedPairToAmbientHomologyMap (twistedGraphBundleChartDomain K h F₀) nonzeroBundle
          (2*(h+∑ i, K i)) ≫ f = twistedGraphBundleChartNormalization K h F₀ (2*(h+∑ i, K i)) := by
…

Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.nonzeroBundle, OAI.Kaplansky.TwistedHyperplaneSlot, OAI.Kaplansky.twistedHyperplaneSumCore, OAI.Kaplansky.restrictedPairToAmbientHomologyMap, OAI.Kaplansky.twistedGraphBundleChartDomain, OAI.Kaplansky.twistedGraphBundleChartNormalization