TopologicalNumbers.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete rational Betti numbers and the four-dimensional Euler number. The finite-CW comparison and covering multiplicativity are classical inputs; the parity obstruction below uses their precise numerical specialization.

def OAI.PositiveEinsteinFour.Topology.rationalHomology line 22
def OAI.PositiveEinsteinFour.Topology.rationalBetti line 26
def OAI.PositiveEinsteinFour.Topology.eulerFour line 29
theorem OAI.PositiveEinsteinFour.Topology.no_double_cover_of_euler_three line 35
Source documentation
No space with Euler number three can be a two-sheeted cover of a finite four-dimensional CW space once the classical multiplicativity formula is instantiated. This is the CP² obstruction in the unoriented classification.
```
theorem no_double_cover_of_euler_three
    {X : Type u} {Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    (hthree : eulerFour X = 3) (hcover : eulerFour X = 2 * eulerFour Y) : False := by
…
```
Mentions: OAI.PositiveEinsteinFour.Topology.eulerFour