Normalized Lusternik–Schnirelmann category

TauCeti.normalizedLSCategory X is the unnormalized categorical-cover count minus one. On nonempty spaces its cover characterization uses n + 1 categorical opens; in particular a contractible space has normalized category zero. Homotopy equivalences preserve this invariant. The definition is totalized to zero on empty spaces, whose unnormalized count remains zero: the formula recovering the unnormalized count by adding one requires nonemptiness.

Compact locally contractible spaces have finite normalized category, by finiteness of the categorical-cover count established in TauCeti.Topology.Homotopy.LusternikSchnirelmann.Basic.

References

• O. Cornea, G. Lupton, J. Oprea and D. Tanré, Lusternik–Schnirelmann Category, Mathematical Surveys and Monographs 103, AMS, 2003, Chapter 1.

noncomputable def TauCeti.normalizedLSCategory (X : Type u_1) [TopologicalSpace X] : ℕ∞

The normalized Lusternik–Schnirelmann category: one less than the least number of categorical opens covering the space, or infinity when there is no finite cover. Truncated subtraction gives zero for the empty space; the usual normalization equation holds only on nonempty spaces. In particular the normalized category of a point is zero.

theorem TauCeti.normalizedLSCategory_def (X : Type u_1) [TopologicalSpace X] : normalizedLSCategory X = lsCategoryCount X Set.univ - 1

The defining relation between normalized category and categorical-cover count.

theorem TauCeti.lsCategoryCount_univ_eq_normalizedLSCategory_add_one (X : Type u_1) [TopologicalSpace X] [Nonempty X] : lsCategoryCount X Set.univ = normalizedLSCategory X + 1

On nonempty spaces, the unnormalized count is the normalized category plus one.

theorem TauCeti.normalizedLSCategory_le_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ∞} : normalizedLSCategory X ≤ n ↔ lsCategoryCount X Set.univ ≤ n + 1

A bound on normalized category is exactly a bound one greater on the cover count.

theorem TauCeti.normalizedLSCategory_le_natCast_iff {X : Type u_1} [TopologicalSpace X] [Nonempty X] {n : ℕ} : normalizedLSCategory X ≤ ↑n ↔ Nonempty (LSCategoricalCover X Set.univ (n + 1))

Normalized category is at most n exactly when n + 1 categorical opens cover the space.

theorem TauCeti.nonempty_lsCategoricalCover_of_normalizedLSCategory_eq {X : Type u_1} [TopologicalSpace X] [Nonempty X] {n : ℕ} (h : normalizedLSCategory X = ↑n) : Nonempty (LSCategoricalCover X Set.univ (n + 1))

Every finite normalized category is attained by a cover with exactly one more open set.

@[simp]

theorem TauCeti.normalizedLSCategory_eq_top_iff {X : Type u_1} [TopologicalSpace X] : normalizedLSCategory X = ⊤ ↔ lsCategoryCount X Set.univ = ⊤

Normalized category is infinite exactly when the categorical-cover count is infinite.

theorem TauCeti.normalizedLSCategory_lt_top_iff {X : Type u_1} [TopologicalSpace X] : normalizedLSCategory X < ⊤ ↔ ∃ (n : ℕ), Nonempty (LSCategoricalCover X Set.univ n)

Normalized category is finite exactly when there is a finite categorical cover.

theorem TauCeti.normalizedLSCategory_lt_top {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (hX : LocallyContractibleSpace X) : normalizedLSCategory X < ⊤

A compact locally contractible space has finite normalized category.

@[simp]

theorem TauCeti.normalizedLSCategory_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [Nonempty X] : normalizedLSCategory X = 0 ↔ ContractibleSpace X

Normalized category zero characterizes contractibility of nonempty spaces.

@[simp]

theorem TauCeti.normalizedLSCategory_of_isEmpty {X : Type u_1} [TopologicalSpace X] [IsEmpty X] : normalizedLSCategory X = 0

The totalized normalized category of the empty space is zero. Its unnormalized count is also zero, so adding one does not recover that count.

@[simp]

theorem TauCeti.normalizedLSCategory_of_contractibleSpace {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] : normalizedLSCategory X = 0

Contractible spaces, including a point, have normalized category zero.

@[simp]

theorem TauCeti.normalizedLSCategory_of_discreteTopology {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : normalizedLSCategory X = Set.univ.encard - 1

On a discrete space normalized category is the number of points minus one, with infinity retained for infinite spaces.

theorem ContinuousMap.HomotopyEquiv.normalizedLSCategory_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : TauCeti.normalizedLSCategory X = TauCeti.normalizedLSCategory Y

Homotopy equivalences preserve normalized category.

theorem Homeomorph.normalizedLSCategory_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : TauCeti.normalizedLSCategory X = TauCeti.normalizedLSCategory Y

Homeomorphisms preserve normalized category.