Sphere.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Suspension homology and integral top generators of spheres.

def OAI.Kaplansky.puncturedVectorSphereHomotopyEquiv line 20
Source documentation
Radial normalization gives a genuine homotopy equivalence of the punctured vector space with its unit sphere.
```
def puncturedVectorSphereHomotopyEquiv (V : Type)
    [NormedAddCommGroup V] [NormedSpace ℝ V] :
    ({0}ᶜ : Set V) ≃ₕ Metric.sphere (0 : V) 1 := by
…
```
def OAI.Kaplansky.localVectorSphereHomologyIso line 32
Source documentation
Relative homology at the origin, in degrees at least two, is identified with the preceding integral sphere homology. No sphere group calculation is assumed.
```
def localVectorSphereHomologyIso (V : Type)
    [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) (hn : n ≠ 0) :
    relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set V)) (n+1) ≅
      (integralSingularHomology n).obj (TopCat.of (Metric.sphere (0 : V) 1)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.integralSingularHomology
def OAI.Kaplansky.canonicalChartSphereHomologyIso line 44
Source documentation
The local relative homology of the actual projective chart at its canonical zero is now compared with ordinary sphere homology.
```
def canonicalChartSphereHomologyIso (n : ℕ) (hn : n ≠ 0) :
    relativeSingularHomology (subspaceInclusion
      ({⟨firstCoordinateProduct K, canonicalProduct_zero_in_chart K⟩}ᶜ :
        Set (canonicalProductGraphChart K).source)) (n+1) ≅
      (integralSingularHomology n).obj
        (TopCat.of (Metric.sphere (0 : ((Σ i, Fin (K i)) → ℂ)) 1)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.canonicalProduct_zero_in_chart, OAI.Kaplansky.canonicalProductGraphChart, OAI.Kaplansky.integralSingularHomology
def OAI.Kaplansky.spherePoleHomeomorph line 60
Source documentation
The sphere with one pole removed is the actual orthogonal hyperplane.
```
def spherePoleHomeomorph (v : sphere (0 : E) 1) :
    ({v}ᶜ : Set (sphere (0 : E) 1)) ≃ₜ (ℝ ∙ (v : E))ᗮ :=
…
```
theorem OAI.Kaplansky.spherePoleHomeomorph_apply line 65
theorem OAI.Kaplansky.sphere_pole_ne_neg line 69
theorem OAI.Kaplansky.sphere_poles_open_cover line 78
theorem OAI.Kaplansky.spherePole_contractible line 89
def OAI.Kaplansky.spherePoleOverlapHomeomorph line 95
Source documentation
Stereographic projection identifies the overlap of the two pole charts with the punctured orthogonal hyperplane.
```
def spherePoleOverlapHomeomorph (v : sphere (0 : E) 1) :
    ↥(({v}ᶜ : Set (sphere (0 : E) 1)) ∩ {-v}ᶜ) ≃ₜ
      ({0}ᶜ : Set (ℝ ∙ (v : E))ᗮ) := by
…
```

def OAI.Kaplansky.spherePoleOverlapHomotopyEquiv line 120

Source documentation

The overlap of opposite pole charts is homotopy equivalent to the equator.

def spherePoleOverlapHomotopyEquiv (v : sphere (0 : E) 1) :
    ↥(({v}ᶜ : Set (sphere (0 : E) 1)) ∩ {-v}ᶜ) ≃ₕ
      sphere (0 : (ℝ ∙ (v : E))ᗮ) 1 :=
…

def OAI.Kaplansky.sphereEquatorHomologyIso line 136

Source documentation

Actual integral homology suspension isomorphism for a unit sphere, obtained from its pole cover and the actual equator.

def sphereEquatorHomologyIso (v : sphere (0 : E) 1) (n : ℕ) (hn : n ≠ 0) :
    (integralSingularHomology (n+1)).obj (TopCat.of (sphere (0 : E) 1)) ≅
      (integralSingularHomology n).obj (TopCat.of (sphere (0 : (ℝ ∙ (v : E))ᗮ) 1)) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.linearIsometrySphereHomeomorph line 146

Source documentation

Restriction of a real linear isometry equivalence to actual unit spheres.

def linearIsometrySphereHomeomorph {F : Type} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) :
    sphere (0 : E) 1 ≃ₜ sphere (0 : F) 1 :=
…

def OAI.Kaplansky.sphereEquatorEuclideanHomeomorph line 152

Source documentation

The equator has the expected Euclidean dimension.

def sphereEquatorEuclideanHomeomorph (d : ℕ) [Fact (Module.finrank ℝ E = d+1)]
    (v : sphere (0 : E) 1) :
    sphere (0 : (ℝ ∙ (v : E))ᗮ) 1 ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin d)) 1 :=
…

def OAI.Kaplansky.sphereEuclideanHomologyStep line 164

Source documentation

Degree recursion to a sphere in one less real dimension. The base H₁ calculation is not included in this statement.

def sphereEuclideanHomologyStep (d : ℕ) [Fact (Module.finrank ℝ E = d+1)]
    (v : sphere (0 : E) 1) (n : ℕ) (hn : n ≠ 0) :
    (integralSingularHomology (n+1)).obj (TopCat.of (sphere (0 : E) 1)) ≅
      (integralSingularHomology n).obj (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin d)) 1)) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.continuousLinearEquivPuncturedHomeomorph line 174

Source documentation

Nonzero vectors transport under an actual continuous linear equivalence.

def continuousLinearEquivPuncturedHomeomorph {E F : Type}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) :
    ({0}ᶜ : Set E) ≃ₜ ({0}ᶜ : Set F) :=
…

def OAI.Kaplansky.spherePlaneOverlapRealHomeomorph line 181

Source documentation

In a real plane, the overlap of the two pole charts is the punctured real line.

def spherePlaneOverlapRealHomeomorph {E : Type} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 1+1)]
    (v : sphere (0 : E) 1) :
    ↥(({v}ᶜ : Set (sphere (0 : E) 1)) ∩ {-v}ᶜ) ≃ₜ ({0}ᶜ : Set ℝ) :=
…

theorem OAI.Kaplansky.puncturedReal_not_joined line 194
Source documentation
The signs lie in different path components of the actual punctured real line.
```
theorem puncturedReal_not_joined :
    ¬ Joined (⟨-1, by simp⟩ : ({0}ᶜ : Set ℝ)) ⟨1, by simp⟩ := by
…
```

theorem OAI.Kaplansky.planeSphere_homologyOne_nonzero line 204

Source documentation

Nonzero integral H₁ of the actual unit sphere of any real plane.

theorem planeSphere_homologyOne_nonzero {E : Type} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 1+1)]
    (v : sphere (0 : E) 1) :
    ∃ z : (integralSingularHomology 1).obj (TopCat.of (sphere (0 : E) 1)), z ≠ 0 := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.puncturedReal_two_components line 221

Source documentation

The punctured real line has exactly its negative and positive path components.

theorem puncturedReal_two_components (x : ({0}ᶜ : Set ℝ)) :
    Joined x (⟨-1, by simp⟩ : ({0}ᶜ : Set ℝ)) ∨ Joined x ⟨1, by simp⟩ := by
…

def OAI.Kaplansky.planeSphereHomologyOneIso line 236

Source documentation

Integral H₁ of a plane sphere, normalized by the ordered negative/positive components of its chosen stereographic overlap.

def planeSphereHomologyOneIso {E : Type} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 1+1)]
    (v : sphere (0 : E) 1) :
    (integralSingularHomology 1).obj (TopCat.of (sphere (0 : E) 1)) ≅ ModuleCat.of ℤ ℤ := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.euclideanSpherePole line 259
Source documentation
A fixed unit vector used to make the recursive sphere calculation a definition.
```
def euclideanSpherePole (n : ℕ) : sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 :=
…
```

def OAI.Kaplansky.euclideanSphereTopHomologyIso line 267

Source documentation

The full top integral homology calculation for every positive-dimensional Euclidean sphere. The recursive pole charts and ordered H₀ components fix a sign.

def euclideanSphereTopHomologyIso : (n : ℕ) →
    (integralSingularHomology (n+1)).obj
      (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin (n+2))) 1)) ≅ ModuleCat.of ℤ ℤ
  | 0 => by
      letI : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1+1) := ⟨by simp⟩
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.euclideanSphereTopGenerator line 279
Source documentation
The normalized integral class determined by the recursive orientation.
```
def euclideanSphereTopGenerator (n : ℕ) :
    (integralSingularHomology (n+1)).obj
      (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin (n+2))) 1)) :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.euclideanSphereTopGenerator_coordinate line 284
theorem OAI.Kaplansky.euclideanSphereTopGenerator_ne_zero line 288
theorem OAI.Kaplansky.nonzero_class_of_iso line 299
theorem OAI.Kaplansky.euclideanSphere_topHomology_nonzero line 310
Source documentation
Every positive-dimensional Euclidean sphere has a nonzero class in its top integral singular homology, with the circle base case proved.
```
theorem euclideanSphere_topHomology_nonzero (n : ℕ) :
    ∃ z : (integralSingularHomology (n+1)).obj
      (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin (n+2))) 1)), z ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
def OAI.Kaplansky.continuousLinearEquivSphereHomotopyEquiv line 327
theorem OAI.Kaplansky.finiteDimensionalSphere_topHomology_nonzero line 335
theorem OAI.Kaplansky.realSphere_positiveHomology_isZero line 351
Source documentation
The actual real zero-sphere has no positive integral homology.
```
theorem realSphere_positiveHomology_isZero (n : ℕ) (hn : n ≠ 0) :
    IsZero ((integralSingularHomology n).obj (TopCat.of (sphere (0 : ℝ) 1))) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.sphere_homologyOne_isZero line 361

Source documentation

The pole-chart intersection is connected in real ambient dimension at least three.

theorem sphere_homologyOne_isZero {E : Type} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (d : ℕ) (hd : 2 ≤ d)
    [Fact (Module.finrank ℝ E = d+1)] (v : sphere (0 : E) 1) :
    IsZero ((integralSingularHomology 1).obj (TopCat.of (sphere (0 : E) 1))) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.euclideanSphereHomology_isZero line 389
Source documentation
Integral sphere homology vanishes in every positive degree other than the sphere dimension. This includes both above- and below-dimension vanishing.
```
theorem euclideanSphereHomology_isZero (d n : ℕ) (hn : n ≠ 0) (hne : n ≠ d) :
    IsZero ((integralSingularHomology n).obj
      (TopCat.of (sphere (0 : EuclideanSpace ℝ (Fin (d+1))) 1))) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.finiteDimensionalSphereHomology_isZero line 410