ProjectiveLocal.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Nonzero local classes and local homology of projective spaces and products.

instance OAI.Kaplansky.ComplexGrassmann.grassmannZero_subsingleton line 16
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProduct_sum_one_factor line 27
Source documentation
If the dimensions sum to one, there is exactly one nontrivial factor.
```
theorem projectiveProduct_sum_one_factor (hK : ∑ i, K i = 1) :
    ∃ i, K i = 1 ∧ ∀ j, j ≠ i → K j = 0 := by
…
```
def OAI.Kaplansky.ComplexGrassmann.projectiveProductOneFactorHomeomorph line 43
Source documentation
Projection onto the unique positive-dimensional factor is a homeomorphism; all other actual Grassmann factors have one point.
```
def projectiveProductOneFactorHomeomorph (i : ι) (hrest : ∀ j, j ≠ i → K j = 0) :
    ProjectiveProduct K ≃ₜ Grassmann 1 (K i) := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.Grassmann
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProductPuncture_contractible_of_sum_one line 63
Source documentation
The punctured actual product of total complex dimension one is contractible, including products with any number of zero-dimensional factors.
```
theorem projectiveProductPuncture_contractible_of_sum_one (hK : ∑ i, K i = 1)
    (P : ProjectiveProduct K) : ContractibleSpace ({P}ᶜ : Set (ProjectiveProduct K)) := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct
theorem OAI.Kaplansky.canonicalCoordinateSpace_real_finrank line 85
Source documentation
Real dimension of the actual complex graph-coordinate space.
```
theorem canonicalCoordinateSpace_real_finrank :
    Module.finrank ℝ ((Σ i, Fin (K i)) → ℂ) = 2 * (∑ i, K i) := by
…
```
theorem OAI.Kaplansky.canonicalCoordinateSphere_topHomology_nonzero line 92
Source documentation
Nonzero integral top sphere class in the exact normed coordinate space used by the canonical section of the actual hyperplane product bundle.
```
theorem canonicalCoordinateSphere_topHomology_nonzero (hp : 0 < (∑ i, K i)) :
    ∃ z : (integralSingularHomology (2 * (∑ i, K i) - 1)).obj
      (TopCat.of (Metric.sphere (0 : ((Σ i, Fin (K i)) → ℂ)) 1)), z ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.canonicalChart_localRelative_nonzero line 105
Source documentation
A nonzero local relative class in the actual chart at the canonical zero.
```
theorem canonicalChart_localRelative_nonzero (hp : 0 < (∑ i, K i)) :
    ∃ z : relativeSingularHomology (subspaceInclusion
      ({⟨firstCoordinateProduct K, canonicalProduct_zero_in_chart K⟩}ᶜ :
        Set (canonicalProductGraphChart K).source)) (2 * (∑ i, K i)), z ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.canonicalProduct_zero_in_chart, OAI.Kaplansky.canonicalProductGraphChart
theorem OAI.Kaplansky.canonicalProduct_localRelative_nonzero line 116
def OAI.Kaplansky.finiteDimensionalSphereTopHomologyIso line 130
Source documentation
Top integral sphere homology for any finite-dimensional real normed space, using a chosen linear coordinate system and the recursive sphere normalization.
```
def finiteDimensionalSphereTopHomologyIso (E : Type)
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (n : ℕ) (hd : Module.finrank ℝ E = n+2) :
    (integralSingularHomology (n+1)).obj (TopCat.of (sphere (0 : E) 1)) ≅ ModuleCat.of ℤ ℤ :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
def OAI.Kaplansky.canonicalProductLocalHomologyIso line 144
Source documentation
Local relative integral homology at the canonical point of the full projective product is ℤ in its real dimension.
```
def canonicalProductLocalHomologyIso (hp : 0 < ∑ i, K i) :
    relativeSingularHomology (subspaceInclusion
      ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) (2 * (∑ i, K i)) ≅
        ModuleCat.of ℤ ℤ := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct
def OAI.Kaplansky.canonicalProductLocalGenerator line 163
Source documentation
A specific primitive integral local class, obtained from 1 under the proved local homology isomorphism. Its orientation is the chosen recursive coordinate orientation; comparison with the standard complex orientation is separate.
```
def canonicalProductLocalGenerator (hp : 0 < ∑ i, K i) :
    relativeSingularHomology (subspaceInclusion
      ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) (2 * (∑ i, K i)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct
theorem OAI.Kaplansky.canonicalProductLocalGenerator_coordinate line 168
theorem OAI.Kaplansky.canonicalProductLocalGenerator_ne_zero line 172
theorem OAI.Kaplansky.canonicalProductLocalGenerator_spans line 180
Source documentation
Every local relative class is the unique integral multiple of this generator.
```
theorem canonicalProductLocalGenerator_spans (hp : 0 < ∑ i, K i)
    (z : relativeSingularHomology (subspaceInclusion
      ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) (2 * (∑ i, K i))) :
    ((canonicalProductLocalHomologyIso K hp).hom z : ℤ) • canonicalProductLocalGenerator K hp = z := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.canonicalProductLocalHomologyIso, OAI.Kaplansky.canonicalProductLocalGenerator
theorem OAI.Kaplansky.puncturedVector_pathConnected_of_finrank line 201
Source documentation
Punctured finite-dimensional real coordinate spaces of dimension at least two are path connected, with their actual norm topology.
```
theorem puncturedVector_pathConnected_of_finrank (E : Type)
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (hd : 2 ≤ Module.finrank ℝ E) : PathConnectedSpace ({0}ᶜ : Set E) := by
…
```

theorem OAI.Kaplansky.localVectorHomology_isZero line 211

Source documentation

Actual local relative homology of a real vector space vanishes in every non-top degree, including the low degrees zero and one.

theorem localVectorHomology_isZero (E : Type)
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (hd : 2 ≤ Module.finrank ℝ E) (n : ℕ) (hn : n ≠ Module.finrank ℝ E) :
    IsZero (relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set E)) n) := by
…

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

theorem OAI.Kaplansky.canonicalProductLocalHomology_isZero line 232
Source documentation
Local integral homology of the actual projective product at its canonical point is concentrated in its real dimension. Combined with the preserved local ℤ isomorphism, this supplies the complete local group calculation.
```
theorem canonicalProductLocalHomology_isZero (hp : 0 < ∑ i, K i)
    (n : ℕ) (hn : n ≠ 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology (subspaceInclusion
      ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct
def OAI.Kaplansky.projectivePointChart line 250
Source documentation
An actual full product graph chart containing any specified projective point.
```
def projectivePointChart (P : ProjectiveProduct K) :
    OpenPartialHomeomorph (ProjectiveProduct K) (ProjectiveProductModel K) :=
…
```
theorem OAI.Kaplansky.projectivePointChart_mem line 255
theorem OAI.Kaplansky.projectivePointChart_target line 259
def OAI.Kaplansky.projectivePointChartHomeomorph line 264
def OAI.Kaplansky.projectivePointLocalCoordinateIso line 271
Source documentation
Local homology at every point of the actual projective product, rather than only at the canonical section zero, has the genuine coordinate comparison.
```
def projectivePointLocalCoordinateIso (P : ProjectiveProduct K) (n : ℕ) :
    relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K))) n ≅
      relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set (ProjectiveProductModel K))) n :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.projectivePointLocalHomology_isZero line 279
Source documentation
Every actual projective point has local integral homology concentrated in the real dimension of the product.
```
theorem projectivePointLocalHomology_isZero (hp : 0 < ∑ i, K i)
    (P : ProjectiveProduct K) (n : ℕ) (hn : n ≠ 2*(∑ i, K i)) :
    IsZero (relativeSingularHomology
      (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K))) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
def OAI.Kaplansky.projectivePointLocalTopHomologyIso line 293
Source documentation
At every projective point the top local integral group is ℤ. Choices of charts and bases give separate generators; their orientation coherence is not asserted.
```
def projectivePointLocalTopHomologyIso (hp : 0 < ∑ i, K i) (P : ProjectiveProduct K) :
    relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K)))
      (2*(∑ i, K i)) ≅ ModuleCat.of ℤ ℤ := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
def OAI.Kaplansky.projectivePointLocalGenerator line 310
Source documentation
A primitive local class at every point, with no claim of a coherent orientation or a global lift when the total complex dimension exceeds one.
```
def projectivePointLocalGenerator (hp : 0 < ∑ i, K i) (P : ProjectiveProduct K) :
    relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K)))
      (2*(∑ i, K i)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.projectivePointLocalGenerator_coordinate line 315
theorem OAI.Kaplansky.projectivePointLocalGenerator_ne_zero line 320

def OAI.Kaplansky.projectiveSpaceLocalCoordinateIso line 334

Source documentation

Local homology of a single projective space in actual graph coordinates.

def projectiveSpaceLocalCoordinateIso {k : ℕ} (P : Grassmann 1 k) (n : ℕ) :
    relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (Grassmann 1 k))) n ≅
      relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set (GraphSlope 1 k))) n := by
…

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

theorem OAI.Kaplansky.projectiveSpaceLocalHomology_isZero line 343

def OAI.Kaplansky.projectiveSpacePunctureHomologyIso line 354

Source documentation

The actual punctured-space homology reduces to the lower projective space.

def projectiveSpacePunctureHomologyIso {k : ℕ} (P : Grassmann 1 (k+1)) (n : ℕ) :
    (integralSingularHomology n).obj (TopCat.of ({P}ᶜ : Set (Grassmann 1 (k+1)))) ≅
      (integralSingularHomology n).obj (TopCat.of (Grassmann 1 k)) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology