The Euler characteristic of a space of finite CW type

The Euler characteristic of a finite CW complex is the alternating count of its cells (TauCeti.cwEulerChar). By singular Euler--Poincaré it is the alternating sum of the dimensions of the singular homology over any division ring, and singular homology is a homotopy invariant, so it depends only on the homotopy type of the complex. This file transports it to spaces of finite CW type.

• TauCeti.eulerChar X: the Euler characteristic of a space X of finite CW type, the alternating cell count of a finite CW complex homotopy equivalent to X.
• TauCeti.eulerChar_eq_cwEulerChar: independence of the model; every finite CW complex homotopy equivalent to X has alternating cell count eulerChar X.
• TauCeti.eulerChar_eq_finsum_finrank_singularHomology: eulerChar X is the alternating sum of the dimensions of the singular homology of X over any division ring.
• ContinuousMap.HomotopyEquiv.eulerChar_eq: homotopy invariance of the Euler characteristic.
• TauCeti.eulerChar_of_discreteTopology and TauCeti.eulerChar_of_contractibleSpace: a finite discrete space has Euler characteristic its cardinality, and a contractible space has Euler characteristic one.

References

• A. Hatcher, Algebraic Topology, Section 2.2, Theorem 2.44.

theorem TauCeti.cwEulerChar_eq_finsum_finrank_singularHomology {Y : Type w} [TopologicalSpace Y] [T2Space Y] (C : Set Y) [Topology.CWComplex C] [Topology.RelCWComplex.Finite C] {X : Type w} [TopologicalSpace X] (e : ContinuousMap.HomotopyEquiv X ↑C) (k : Type w) [DivisionRing k] : cwEulerChar C = ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj ↧k).obj ↧X))

The alternating cell count of a finite CW complex is the alternating sum of the dimensions of the singular homology, over any division ring, of any space homotopy equivalent to the complex.

@[simp]

theorem TauCeti.cwEulerChar_univ_of_discreteTopology {X : Type w} [TopologicalSpace X] [DiscreteTopology X] : cwEulerChar Set.univ = ↑(Nat.card X)

The discrete CW structure on a finite discrete space has Euler characteristic the number of points.

noncomputable def TauCeti.eulerChar (X : Type w) [TopologicalSpace X] [FiniteCWType X] : ℤ

The Euler characteristic of a space of finite CW type: the alternating count of the cells of a finite CW complex homotopy equivalent to it. It does not depend on the chosen complex (TauCeti.eulerChar_eq_cwEulerChar).

Equations

• TauCeti.eulerChar X = ⋯.choose

theorem TauCeti.eulerChar_eq_finsum_finrank_singularHomology (X : Type w) [TopologicalSpace X] [FiniteCWType X] (k : Type w) [DivisionRing k] : eulerChar X = ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj ↧k).obj ↧X))

Euler--Poincaré for a space of finite CW type: its Euler characteristic is the alternating sum of the dimensions of its singular homology over any division ring.

theorem TauCeti.eulerChar_eq_cwEulerChar {X : Type w} [TopologicalSpace X] [FiniteCWType X] {Y : Type w} [TopologicalSpace Y] [T2Space Y] {C : Set Y} [Topology.CWComplex C] [Topology.RelCWComplex.Finite C] (e : ContinuousMap.HomotopyEquiv X ↑C) : eulerChar X = cwEulerChar C

Independence of the model. Every finite CW complex homotopy equivalent to a space has alternating cell count equal to the Euler characteristic of the space.

@[simp]

theorem TauCeti.eulerChar_cwComplex {Y : Type w} [TopologicalSpace Y] [T2Space Y] (C : Set Y) [Topology.CWComplex C] [Topology.RelCWComplex.Finite C] : eulerChar ↑C = cwEulerChar C

The Euler characteristic of a finite CW complex is its alternating cell count.

theorem ContinuousMap.HomotopyEquiv.eulerChar_eq {X : Type w} [TopologicalSpace X] [TauCeti.FiniteCWType X] {Y : Type w} [TopologicalSpace Y] [h : TauCeti.FiniteCWType Y] (e : HomotopyEquiv X Y) : TauCeti.eulerChar X = TauCeti.eulerChar Y

Homotopy invariance of the Euler characteristic: homotopy equivalent spaces of finite CW type have the same Euler characteristic.

theorem Homeomorph.eulerChar_eq {X : Type w} [TopologicalSpace X] [TauCeti.FiniteCWType X] {Y : Type w} [TopologicalSpace Y] [TauCeti.FiniteCWType Y] (e : X ≃ₜ Y) : TauCeti.eulerChar X = TauCeti.eulerChar Y

Homeomorphic spaces of finite CW type have the same Euler characteristic.

theorem TauCeti.eulerChar_of_discreteTopology {X : Type w} [TopologicalSpace X] [DiscreteTopology X] [Finite X] : eulerChar X = ↑(Nat.card X)

A finite discrete space has Euler characteristic its number of points.

theorem TauCeti.eulerChar_of_contractibleSpace {X : Type w} [TopologicalSpace X] [ContractibleSpace X] : eulerChar X = 1

A contractible space has Euler characteristic one.