ProjectiveClass.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

Localization, top homology, and the fundamental class of projective products.

instance OAI.Kaplansky.projectiveSpaceZero_nonempty line 16
theorem OAI.Kaplansky.projectiveSpaceHomology_isZero line 22
Source documentation
Complex projective space has no positive odd homology and no homology above its real dimension. The induction uses the proved puncture retraction and actual local relative homology, with no cell or orientation premise.
```
theorem projectiveSpaceHomology_isZero (k n : ℕ) (hn : n ≠ 0)
    (hdegree : Odd n ∨ 2*k < n) :
    IsZero ((integralSingularHomology n).obj (TopCat.of (Grassmann 1 k))) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveSpacePunctureHomology_isZero line 44

Source documentation

Punctured CP^k has no homology in degrees above 2k-2.

theorem projectiveSpacePunctureHomology_isZero {k : ℕ} (P : Grassmann 1 (k+1))
    (n : ℕ) (hn : 2*k < n) :
    IsZero ((integralSingularHomology n).obj (TopCat.of ({P}ᶜ : Set (Grassmann 1 (k+1))))) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveSpaceTopBoundary_zero line 51
Source documentation
The top-degree local connecting map is zero at every point of CP^k.
```
theorem projectiveSpaceTopBoundary_zero {k : ℕ} (hk : 0 < k) (P : Grassmann 1 k) :
    relativeHomologyBoundary (subspaceInclusion ({P}ᶜ : Set (Grassmann 1 k))) (2*k-1) = 0 := by
…
```
Mentions: OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.subspaceInclusion
def OAI.Kaplansky.projectiveSpaceTopLocalizationIso line 59
Source documentation
Absolute-to-local homology is an isomorphism in the real top dimension of every positive-dimensional single complex projective space.
```
def projectiveSpaceTopLocalizationIso {k : ℕ} (hk : 0 < k) (P : Grassmann 1 k) :
    (integralSingularHomology (2*k)).obj (TopCat.of (Grassmann 1 k)) ≅
      relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (Grassmann 1 k))) (2*k) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.projectiveSpaceTopLocalizationIso_hom line 84
theorem OAI.Kaplansky.projectiveProduct_one_factor_dimension line 92
Source documentation
The dimension of a product with at most one nontrivial factor.
```
theorem projectiveProduct_one_factor_dimension (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) : ∑ j, K j = K i := by
…
```

def OAI.Kaplansky.projectiveOneFactorPunctureHomeomorph line 98

Source documentation

Puncturing commutes with the actual one-factor product homeomorphism.

def projectiveOneFactorPunctureHomeomorph (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (P : ProjectiveProduct K) :
    ({P}ᶜ : Set (ProjectiveProduct K)) ≃ₜ ({P i}ᶜ : Set (Grassmann 1 (K i))) :=
…

theorem OAI.Kaplansky.projectiveOneFactorPunctureHomology_isZero line 106

Source documentation

The top two punctured homology groups vanish for a product supported at one factor, with no restriction that this factor be a projective line.

theorem projectiveOneFactorPunctureHomology_isZero (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (hp : 0 < ∑ j, K j)
    (P : ProjectiveProduct K) (n : ℕ) (hn : 2*(∑ j, K j)-2 < n) :
    IsZero ((integralSingularHomology n).obj
      (TopCat.of ({P}ᶜ : Set (ProjectiveProduct K)))) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveOneFactorTopBoundary_zero line 123
Source documentation
The requested top-degree connecting map vanishes for every product with one positive-dimensional factor, even when its total dimension exceeds one.
```
theorem projectiveOneFactorTopBoundary_zero (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (hp : 0 < ∑ j, K j) (P : ProjectiveProduct K) :
    relativeHomologyBoundary (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K)))
      (2*(∑ j, K j)-1) = 0 :=
…
```
Mentions: OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.subspaceInclusion

def OAI.Kaplansky.projectiveOneFactorTopLocalizationIso line 130

Source documentation

The actual absolute-to-relative map, proved bijective in top degree.

def projectiveOneFactorTopLocalizationIso (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (hp : 0 < ∑ j, K j) (P : ProjectiveProduct K) :
    (integralSingularHomology (2*(∑ j, K j))).obj (TopCat.of (ProjectiveProduct K)) ≅
      relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K)))
        (2*(∑ j, K j)) := by
…

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

theorem OAI.Kaplansky.projectiveOneFactorTopLocalizationIso_hom line 152

def OAI.Kaplansky.projectiveOneFactorTopHomologyIso line 159

Source documentation

Global top homology is ℤ, normalized by the preserved canonical local class.

def projectiveOneFactorTopHomologyIso (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (hp : 0 < ∑ j, K j) :
    (integralSingularHomology (2*(∑ j, K j))).obj (TopCat.of (ProjectiveProduct K)) ≅
      ModuleCat.of ℤ ℤ :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.projectiveOneFactorFundamentalClass line 168
Source documentation
An actual global lift of the preserved generator for an arbitrary-dimensional one-factor product. The multi-factor case is not assumed.
```
def projectiveOneFactorFundamentalClass (i : ι)
    (hrest : ∀ j, j ≠ i → K j = 0) (hp : 0 < ∑ j, K j) :
    (integralSingularHomology (2*(∑ j, K j))).obj (TopCat.of (ProjectiveProduct K)) :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.projectiveOneFactorFundamentalClass_localizes line 174
theorem OAI.Kaplansky.projectiveOneFactorFundamentalClass_ne_zero line 183
theorem OAI.Kaplansky.projectiveOneFactorFundamentalClass_coordinate line 191
def OAI.Kaplansky.ComplexGrassmann.projectiveCoordinatePuncture line 208
Source documentation
The coordinate puncture is open in the actual compact projective product.
```
def projectiveCoordinatePuncture (P : ProjectiveProduct K) (i : ι) : Set (ProjectiveProduct K) :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct
theorem OAI.Kaplansky.ComplexGrassmann.projectiveCoordinatePuncture_open line 211
def OAI.Kaplansky.ComplexGrassmann.coordinatePunctureFactor line 215
instance OAI.Kaplansky.ComplexGrassmann.(instance at line 218) line 218
def OAI.Kaplansky.ComplexGrassmann.coordinatePunctureIntersectionHomeomorph line 222
def OAI.Kaplansky.ComplexGrassmann.coordinatePunctureDimensions line 234
def OAI.Kaplansky.ComplexGrassmann.coordinatePunctureFactorHomotopyEquiv line 238
def OAI.Kaplansky.ComplexGrassmann.coordinatePunctureIntersectionHomotopyEquiv line 266
Source documentation
Every nonempty coordinate-puncture intersection retracts to the actual projective product with one dimension removed in each punctured factor.
```
def coordinatePunctureIntersectionHomotopyEquiv (P : ProjectiveProduct K) (T : Finset ι)
    (hT : ∀ i ∈ T, 0 < K i) :
    (⋂ i ∈ T, projectiveCoordinatePuncture K P i) ≃ₕ
      ProjectiveProduct (coordinatePunctureDimensions K T) :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.projectiveCoordinatePuncture, OAI.Kaplansky.ComplexGrassmann.coordinatePunctureDimensions
theorem OAI.Kaplansky.ComplexGrassmann.coordinatePunctureDimensions_sum line 275
theorem OAI.Kaplansky.ComplexGrassmann.projectiveCoordinatePunctures_cover line 293
Source documentation
Positive-dimensional coordinate punctures cover the complement of any point.
```
theorem projectiveCoordinatePunctures_cover (P : ProjectiveProduct K) :
    (⋃ i ∈ Finset.univ.filter (fun i => 0 < K i), projectiveCoordinatePuncture K P i) = {P}ᶜ := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.projectiveCoordinatePuncture
theorem OAI.Kaplansky.projectiveProductZero_contractible line 325
Source documentation
A zero-dimensional projective product is a single point, including an empty index type.
```
theorem projectiveProductZero_contractible (K : ι → ℕ) (hK : ∑ i, K i = 0) :
    ContractibleSpace (ProjectiveProduct K) := by
…
```

theorem OAI.Kaplansky.projectiveProductPunctureHomology_from_lower line 338

Source documentation

A coordinate-puncture cover converts already-proved lower-dimensional absolute vanishing into puncture vanishing two degrees below the real dimension.

theorem projectiveProductPunctureHomology_from_lower (K : ι → ℕ)
    (hp : 0 < ∑ i, K i)
    (hlower : ∀ L : ι → ℕ, (∑ i, L i) < ∑ i, K i → ∀ q : ℕ, 2*(∑ i, L i) < q →
      IsZero ((integralSingularHomology q).obj (TopCat.of (ProjectiveProduct L))))
    (P : ProjectiveProduct K) (n : ℕ) (hn : 2*(∑ i, K i)-2 < n) :
    IsZero ((integralSingularHomology n).obj (TopCat.of ({P}ᶜ : Set (ProjectiveProduct K)))) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveProductHomology_above_dimension line 368
Source documentation
Genuine integral homology of every finite projective product vanishes above its real dimension. The strong induction uses the coordinate-puncture cover, the proved puncture retractions, and the actual relative exact sequence.
```
theorem projectiveProductHomology_above_dimension (K : ι → ℕ)
    (n : ℕ) (hn : 2*(∑ i, K i) < n) :
    IsZero ((integralSingularHomology n).obj (TopCat.of (ProjectiveProduct K))) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveProductPunctureHomology_isZero line 392

Source documentation

Removing any point from any positive-dimensional projective product kills homology above real dimension minus two.

theorem projectiveProductPunctureHomology_isZero (K : ι → ℕ) (hp : 0 < ∑ i, K i)
    (P : ProjectiveProduct K) (n : ℕ) (hn : 2*(∑ i, K i)-2 < n) :
    IsZero ((integralSingularHomology n).obj (TopCat.of ({P}ᶜ : Set (ProjectiveProduct K)))) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.projectiveProductTopBoundary_zero line 398
def OAI.Kaplansky.projectiveProductTopLocalizationIso line 413
Source documentation
Top-degree localization is the actual absolute-to-relative map and is invertible at every point of every positive-dimensional projective product.
```
def projectiveProductTopLocalizationIso (hp : 0 < ∑ i, K i) (P : ProjectiveProduct K) :
    (integralSingularHomology (2*(∑ i, K i))).obj (TopCat.of (ProjectiveProduct K)) ≅
      relativeSingularHomology (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K)))
        (2*(∑ i, K i)) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.projectiveProductTopLocalizationIso_hom line 434
def OAI.Kaplansky.projectiveProductTopHomologyIso line 440
Source documentation
Global integral top homology is ℤ with the exact preserved local normalization.
```
def projectiveProductTopHomologyIso (hp : 0 < ∑ i, K i) :
    (integralSingularHomology (2*(∑ i, K i))).obj (TopCat.of (ProjectiveProduct K)) ≅
      ModuleCat.of ℤ ℤ :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
def OAI.Kaplansky.projectiveProductFundamentalClass line 448
Source documentation
The unique actual global lift of the PRESERVED canonical local generator. This construction is unconditional apart from positive total dimension.
```
def projectiveProductFundamentalClass (hp : 0 < ∑ i, K i) :
    (integralSingularHomology (2*(∑ i, K i))).obj (TopCat.of (ProjectiveProduct K)) :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.projectiveProductFundamentalClass_localizes line 453
theorem OAI.Kaplansky.projectiveProductFundamentalClass_coordinate line 461
theorem OAI.Kaplansky.projectiveProductFundamentalClass_ne_zero line 468
theorem OAI.Kaplansky.projectiveProductFundamentalClass_unique line 475
theorem OAI.Kaplansky.projectiveProductFundamentalClass_spans line 485
Source documentation
Every absolute top class is an integral multiple of the specified global class.
```
theorem projectiveProductFundamentalClass_spans (hp : 0 < ∑ i, K i)
    (z : (integralSingularHomology (2*(∑ i, K i))).obj (TopCat.of (ProjectiveProduct K))) :
    ((projectiveProductTopHomologyIso K hp).hom z : ℤ) • projectiveProductFundamentalClass K hp = z := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.projectiveProductTopHomologyIso, OAI.Kaplansky.projectiveProductFundamentalClass
theorem OAI.Kaplansky.projectiveProductFundamentalClass_localizes_ne_zero line 494
Source documentation
The same global class localizes nontrivially at EVERY projective point; these are restrictions of a single class, not independently chosen generators.
```
theorem projectiveProductFundamentalClass_localizes_ne_zero (hp : 0 < ∑ i, K i)
    (P : ProjectiveProduct K) :
    absoluteToRelative (subspaceInclusion ({P}ᶜ : Set (ProjectiveProduct K))) (2*(∑ i, K i))
      (projectiveProductFundamentalClass K hp) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.absoluteToRelative, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.projectiveProductFundamentalClass

theorem OAI.Kaplansky.canonicalProductLocalGenerator_boundary_zero line 505

Source documentation

The exact old boundary obligation, with the degree cast made explicit.

theorem canonicalProductLocalGenerator_boundary_zero (hp : 0 < ∑ i, K i) :
    relativeHomologyBoundary (subspaceInclusion
      ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) (2*(∑ i, K i)-1)
      ((show 2*(∑ i, K i) = (2*(∑ i, K i)-1)+1 by omega) ▸
        canonicalProductLocalGenerator K hp) = 0 := by
…

Mentions: OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.firstCoordinateProduct, OAI.Kaplansky.canonicalProductLocalGenerator