RationalBettiZero.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The degree-zero rational Betti number of an actual connected four-manifold. This uses singular homology, with no Hodge-theoretic or characteristic-number premise.

def OAI.PositiveEinsteinFour.Topology.rationalHomologyZeroEquiv line 22
Source documentation
Augmentation identifies the singular zeroth homology with its coefficient field on a path-connected space.
```
def rationalHomologyZeroEquiv (X : Type u) [TopologicalSpace X] [PathConnectedSpace X] :
    rationalHomology X 0 ≃ₗ[ℚ] ULift.{u} ℚ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Topology.rationalHomology
theorem OAI.PositiveEinsteinFour.Topology.rationalBetti_zero_of_pathConnected line 26
theorem OAI.PositiveEinsteinFour.Topology.rationalBetti_zero_of_connected_manifold line 33
Source documentation
In particular, the manifold hypotheses in the classification problem give the actual zeroth Betti number. Compactness and curvature are not needed.
```
theorem rationalBetti_zero_of_connected_manifold (M : Type u)
    [TopologicalSpace M] [ChartedSpace FourSpace M] [ConnectedSpace M] :
    rationalBetti M 0 = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Topology.rationalBetti