Lusternik–Schnirelmann categorical covers

An open subset U of a topological space X is categorical if its inclusion into X is nullhomotopic. Only the inclusion has to contract inside X: U itself need not be contractible. A categorical cover of A ⊆ X of size n is a family of n categorical open subsets of X whose union contains A (TauCeti.LSCategoricalCover), and the unnormalized Lusternik–Schnirelmann category TauCeti.lsCategoryCount X A : ℕ∞ is the least size of such a cover, or ⊤ if there is none. With this unnormalized convention the empty subset has count 0 and a contractible space, such as a one-point space, has count 1 on univ.

The count is monotone in A, subadditive on finite unions, and does not increase under deformations: if g : X → X is homotopic to the identity and maps A into B, then lsCategoryCount X A ≤ lsCategoryCount X B (TauCeti.lsCategoryCount_le_of_homotopic_id). The general form pulls covers back along any map with a left homotopy inverse (TauCeti.LSCategoricalCover.comap); it gives homotopy invariance of the count of the whole space and invariance under homeomorphisms. The deformation inequality is what bounds the category by the number of critical points of a smooth function on a compact manifold: deforming a sublevel down past a critical level along the gradient flow costs at most one categorical open per critical point on that level.

The count is additive on finite disjoint unions. A nullhomotopy of the inclusion joins every point of a categorical open set to a single point, so such a set meets at most one summand, and the count of the whole union is the sum of the counts of the summands. On a manifold with several components, this lets the critical-point bound be computed one component at a time.

Compact subsets of locally contractible spaces have finite categorical-cover count, even on an open neighborhood. Here local contractibility has Mathlib's meaning: small neighborhoods contract inside larger neighborhoods, not necessarily inside themselves. The finite count and its attainment give actual finite categorical covers of compact locally contractible spaces.

Main declarations

• TauCeti.LSCategoricalCover X A n: a cover of A by n open subsets of X with nullhomotopic inclusions, with restriction mono, concatenation append, padding by empty opens pad, pullback comap, and pushforward map along open embeddings.
• TauCeti.lsCategoryCount X A: the least size of a categorical cover of A, attained when finite (TauCeti.nonempty_lsCategoricalCover_of_lsCategoryCount_eq).
• TauCeti.lsCategoryCount_le_iff: lsCategoryCount X A ≤ n exactly when A has a categorical cover of size at most n, and TauCeti.lsCategoryCount_lt_top_iff: the count is finite exactly when A has a categorical cover.
• TauCeti.lsCategoryCount_union_le and TauCeti.lsCategoryCount_biUnion_le: subadditivity.
• TauCeti.lsCategoryCount_le_of_homotopic_id and TauCeti.lsCategoryCount_le_of_deformation: the deformation inequality, for a map homotopic to the identity and for the endpoint of a deformation [0, 1] × X → X starting at the identity.
• TauCeti.exists_isOpen_superset_lsCategoryCount_le_encard: in a locally contractible space every set has an open neighbourhood whose count is at most its cardinality.
• ContinuousMap.HomotopyEquiv.lsCategoryCount_univ_eq and Homeomorph.lsCategoryCount_image: invariance under homotopy equivalences and homeomorphisms.
• TauCeti.lsCategoryCount_eq_zero and TauCeti.lsCategoryCount_pos: the count vanishes exactly on the empty set.
• TauCeti.lsCategoryCount_eq_sum_inter: additivity over finitely many pairwise disjoint clopen sets, and TauCeti.lsCategoryCount_sigma, TauCeti.lsCategoryCount_univ_sigma: the count of a finite disjoint union is the sum of the counts of its summands.
• TauCeti.lsCategoryCount_univ_eq_finsum_connectedComponents: the count of a space with finitely many components is the sum of the counts of its components.
• TauCeti.lsCategoryCount_preimage_subtypeVal: a clopen subspace computes the counts of its subsets as the ambient space does, and TauCeti.lsCategoryCount_eq_sum_preimage_subtypeVal, TauCeti.lsCategoryCount_univ_eq_sum_connectedComponents: the count is the sum of the counts in the subspaces of a finite clopen partition, for instance the connected components.
• TauCeti.lsCategoryCount_univ_of_contractibleSpace and TauCeti.lsCategoryCount_eq_encard: a contractible space has count 1, and in a discrete space the count of a set is its cardinality.

References

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

structure TauCeti.LSCategoricalCover (X : Type u_1) [TopologicalSpace X] (A : Set X) (n : ℕ) : Type u_1

A categorical cover of a subset A of a topological space X of size n: n open subsets of X covering A, each of whose inclusions into X is nullhomotopic. The open sets themselves need not be contractible.

• opens : Fin n → TopologicalSpace.Opens X

  The open sets of the cover.

• subset_iUnion : A ⊆ ⋃ (i : Fin n), ↑(self.opens i)

  The open sets of the cover contain A.

• nullhomotopic (i : Fin n) : (ContinuousMap.subtypeVal ↑(self.opens i)).Nullhomotopic

  The inclusion of each open set of the cover into X is nullhomotopic.

theorem TauCeti.LSCategoricalCover.ext_iff {X : Type u_1} {inst✝ : TopologicalSpace X} {A : Set X} {n : ℕ} {x y : LSCategoricalCover X A n} : x = y ↔ x.opens = y.opens

theorem TauCeti.LSCategoricalCover.ext {X : Type u_1} {inst✝ : TopologicalSpace X} {A : Set X} {n : ℕ} {x y : LSCategoricalCover X A n} (opens : x.opens = y.opens) : x = y

theorem TauCeti.nullhomotopic_subtypeVal_of_subset_singleton {X : Type u_1} [TopologicalSpace X] {U : Set X} {x : X} (h : U ⊆ {x}) : (ContinuousMap.subtypeVal U).Nullhomotopic

The inclusion of a subset of a singleton is nullhomotopic, since it is constant.

theorem TauCeti.subset_of_nullhomotopic_of_isClopen {X : Type u_1} [TopologicalSpace X] {U C : Set X} (h : (ContinuousMap.subtypeVal U).Nullhomotopic) (hC : IsClopen C) (hUC : (U ∩ C).Nonempty) : U ⊆ C

A set with nullhomotopic inclusion that meets a clopen set is contained in it: under a nullhomotopy of the inclusion, the track of each point is a path to the common endpoint, so every point lies in exactly the same clopen sets as that endpoint. In particular a categorical open set meets at most one component of a disjoint union.

theorem TauCeti.exists_subset_singleton_of_nullhomotopic {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] {U : Set X} (h : (ContinuousMap.subtypeVal U).Nullhomotopic) : ∃ (x : X), U ⊆ {x}

In a discrete space a set with nullhomotopic inclusion has at most one point, since every singleton is clopen.

def TauCeti.LSCategoricalCover.mono {X : Type u_1} [TopologicalSpace X] {A B : Set X} {n : ℕ} (c : LSCategoricalCover X B n) (h : A ⊆ B) : LSCategoricalCover X A n

A categorical cover of B is a categorical cover of every subset of B.

@[simp]

theorem TauCeti.LSCategoricalCover.mono_opens {X : Type u_1} [TopologicalSpace X] {A B : Set X} {n : ℕ} (c : LSCategoricalCover X B n) (h : A ⊆ B) : (c.mono h).opens = c.opens

def TauCeti.LSCategoricalCover.empty {X : Type u_1} [TopologicalSpace X] : LSCategoricalCover X ∅ 0

The empty cover of the empty set.

theorem TauCeti.LSCategoricalCover.nonempty_zero_iff {X : Type u_1} [TopologicalSpace X] {A : Set X} : Nonempty (LSCategoricalCover X A 0) ↔ A = ∅

A set has a categorical cover of size 0 exactly when it is empty.

def TauCeti.LSCategoricalCover.single {X : Type u_1} [TopologicalSpace X] {A : Set X} (U : TopologicalSpace.Opens X) (hA : A ⊆ ↑U) (hU : (ContinuousMap.subtypeVal ↑U).Nullhomotopic) : LSCategoricalCover X A 1

A single open set with nullhomotopic inclusion containing A is a categorical cover of A of size 1.

@[simp]

theorem TauCeti.LSCategoricalCover.single_opens {X : Type u_1} [TopologicalSpace X] {A : Set X} (U : TopologicalSpace.Opens X) (hA : A ⊆ ↑U) (hU : (ContinuousMap.subtypeVal ↑U).Nullhomotopic) (i : Fin 1) : (single U hA hU).opens i = U

def TauCeti.LSCategoricalCover.append {X : Type u_1} [TopologicalSpace X] {A B : Set X} {m n : ℕ} (c : LSCategoricalCover X A m) (d : LSCategoricalCover X B n) : LSCategoricalCover X (A ∪ B) (m + n)

The concatenation of categorical covers of A and B is a categorical cover of A ∪ B.

@[simp]

theorem TauCeti.LSCategoricalCover.append_opens {X : Type u_1} [TopologicalSpace X] {A B : Set X} {m n : ℕ} (c : LSCategoricalCover X A m) (d : LSCategoricalCover X B n) : (c.append d).opens = Fin.append c.opens d.opens

def TauCeti.LSCategoricalCover.pad {X : Type u_1} [TopologicalSpace X] {A : Set X} {m n : ℕ} [Nonempty X] (c : LSCategoricalCover X A m) (h : m ≤ n) : LSCategoricalCover X A n

On a nonempty space a categorical cover can be enlarged to any larger size by adding empty open sets, whose inclusions are nullhomotopic.

theorem TauCeti.LSCategoricalCover.pad_opens_of_lt {X : Type u_1} [TopologicalSpace X] {A : Set X} {m n : ℕ} [Nonempty X] (c : LSCategoricalCover X A m) (h : m ≤ n) {i : Fin n} (hi : ↑i < m) : (c.pad h).opens i = c.opens ⟨↑i, hi⟩

theorem TauCeti.LSCategoricalCover.pad_opens_of_le {X : Type u_1} [TopologicalSpace X] {A : Set X} {m n : ℕ} [Nonempty X] (c : LSCategoricalCover X A m) (h : m ≤ n) {i : Fin n} (hi : m ≤ ↑i) : (c.pad h).opens i = ⊥

def TauCeti.LSCategoricalCover.comap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {B : Set X} {n : ℕ} {A : Set Y} (c : LSCategoricalCover X B n) (g : C(Y, X)) (r : C(X, Y)) (hrg : (r.comp g).Homotopic (ContinuousMap.id Y)) (hA : Set.MapsTo (⇑g) A B) : LSCategoricalCover Y A n

Pullback of categorical covers. Let g : Y → X have a left homotopy inverse r : X → Y, so that r ∘ g is homotopic to the identity of Y. If g maps A ⊆ Y into B ⊆ X, the preimages under g of a categorical cover of B form a categorical cover of A.

@[simp]

theorem TauCeti.LSCategoricalCover.comap_opens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {B : Set X} {n : ℕ} {A : Set Y} (c : LSCategoricalCover X B n) (g : C(Y, X)) (r : C(X, Y)) (hrg : (r.comp g).Homotopic (ContinuousMap.id Y)) (hA : Set.MapsTo (⇑g) A B) (i : Fin n) : (c.comap g r hrg hA).opens i = (TopologicalSpace.Opens.comap g) (c.opens i)

def TauCeti.LSCategoricalCover.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {A : Set Y} (c : LSCategoricalCover Y A n) {e : Y → X} (he : Topology.IsOpenEmbedding e) : LSCategoricalCover X (e '' A) n

Pushforward of categorical covers along an open embedding e : Y → X: the images under e of a categorical cover of A ⊆ Y form a categorical cover of e '' A.

@[simp]

theorem TauCeti.LSCategoricalCover.map_opens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {A : Set Y} (c : LSCategoricalCover Y A n) {e : Y → X} (he : Topology.IsOpenEmbedding e) (i : Fin n) : ↑((c.map he).opens i) = e '' ↑(c.opens i)

noncomputable def TauCeti.lsCategoryCount (X : Type u_1) [TopologicalSpace X] (A : Set X) : ℕ∞

The unnormalized Lusternik–Schnirelmann category of a subset A of X: the least size of a categorical cover of A, or ⊤ if A has no finite categorical cover. The empty set has count 0, and a contractible space, such as a one-point space, has count 1 on univ.

theorem TauCeti.LSCategoricalCover.lsCategoryCount_le {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ} (c : LSCategoricalCover X A n) : lsCategoryCount X A ≤ ↑n

A categorical cover of size n bounds the Lusternik–Schnirelmann count by n.

theorem TauCeti.nonempty_lsCategoricalCover_of_lsCategoryCount_eq {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ} (h : lsCategoryCount X A = ↑n) : Nonempty (LSCategoricalCover X A n)

A finite Lusternik–Schnirelmann count is attained by a categorical cover.

theorem TauCeti.lsCategoryCount_le_iff {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ} : lsCategoryCount X A ≤ ↑n ↔ ∃ m ≤ n, Nonempty (LSCategoricalCover X A m)

The Lusternik–Schnirelmann count of A is at most n exactly when A has a categorical cover of size at most n.

theorem TauCeti.nonempty_lsCategoricalCover_iff {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ} [Nonempty X] : Nonempty (LSCategoricalCover X A n) ↔ lsCategoryCount X A ≤ ↑n

On a nonempty space, A has a categorical cover of size n exactly when its Lusternik–Schnirelmann count is at most n. On an empty space only the size 0 occurs.

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

The Lusternik–Schnirelmann count of A is finite exactly when A has a categorical cover.

theorem TauCeti.lsCategoryCount_eq_top_iff {X : Type u_1} [TopologicalSpace X] {A : Set X} : lsCategoryCount X A = ⊤ ↔ ∀ (n : ℕ), IsEmpty (LSCategoricalCover X A n)

The Lusternik–Schnirelmann count of A is ⊤ exactly when A has no categorical cover.

theorem TauCeti.lsCategoryCount_mono {X : Type u_1} [TopologicalSpace X] {A B : Set X} (h : A ⊆ B) : lsCategoryCount X A ≤ lsCategoryCount X B

The Lusternik–Schnirelmann count is monotone in the subset.

@[simp]

theorem TauCeti.lsCategoryCount_empty {X : Type u_1} [TopologicalSpace X] : lsCategoryCount X ∅ = 0

@[simp]

theorem TauCeti.lsCategoryCount_eq_zero {X : Type u_1} [TopologicalSpace X] {A : Set X} : lsCategoryCount X A = 0 ↔ A = ∅

Only the empty set has Lusternik–Schnirelmann count 0.

theorem TauCeti.lsCategoryCount_pos {X : Type u_1} [TopologicalSpace X] {A : Set X} : 0 < lsCategoryCount X A ↔ A.Nonempty

A nonempty set has positive Lusternik–Schnirelmann count.

theorem TauCeti.lsCategoryCount_union_le {X : Type u_1} [TopologicalSpace X] {A B : Set X} : lsCategoryCount X (A ∪ B) ≤ lsCategoryCount X A + lsCategoryCount X B

Subadditivity of the Lusternik–Schnirelmann count on unions.

theorem TauCeti.lsCategoryCount_biUnion_le {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} (s : Finset ι) (A : ι → Set X) : lsCategoryCount X (⋃ i ∈ s, A i) ≤ ∑ i ∈ s, lsCategoryCount X (A i)

Subadditivity of the Lusternik–Schnirelmann count on finite unions.

theorem TauCeti.lsCategoryCount_le_of_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {B : Set X} {A : Set Y} (g : C(Y, X)) (r : C(X, Y)) (hrg : (r.comp g).Homotopic (ContinuousMap.id Y)) (hA : Set.MapsTo (⇑g) A B) : lsCategoryCount Y A ≤ lsCategoryCount X B

Pullback inequality for the Lusternik–Schnirelmann count. If g : Y → X has a left homotopy inverse and maps A into B, then the count of A in Y is at most the count of B in X.

theorem Topology.IsOpenEmbedding.lsCategoryCount_image_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : Y → X} (he : IsOpenEmbedding e) (A : Set Y) : TauCeti.lsCategoryCount X (e '' A) ≤ TauCeti.lsCategoryCount Y A

Pushforward inequality for the Lusternik–Schnirelmann count along an open embedding e : Y → X: the count of e '' A in X is at most the count of A in Y.

theorem TauCeti.lsCategoryCount_le_of_homotopic_id {X : Type u_1} [TopologicalSpace X] {A B : Set X} (g : C(X, X)) (hg : g.Homotopic (ContinuousMap.id X)) (hA : Set.MapsTo (⇑g) A B) : lsCategoryCount X A ≤ lsCategoryCount X B

The deformation inequality: if g : X → X is homotopic to the identity and maps A into B, then the Lusternik–Schnirelmann count of A is at most that of B.

theorem TauCeti.lsCategoryCount_le_of_deformation {X : Type u_1} [TopologicalSpace X] {A B : Set X} (Φ : C(↑unitInterval × X, X)) (h0 : ∀ (x : X), Φ (0, x) = x) (hA : Set.MapsTo (fun (x : X) => Φ (1, x)) A B) : lsCategoryCount X A ≤ lsCategoryCount X B

The deformation inequality for a deformation Φ : [0, 1] × X → X starting at the identity: if its endpoint Φ (1, ·) maps A into B, then the Lusternik–Schnirelmann count of A is at most that of B.

theorem TauCeti.lsCategoryCount_le_one {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] (A : Set X) : lsCategoryCount X A ≤ 1

In a contractible space every open set is categorical, so every subset has count at most 1.

theorem TauCeti.lsCategoryCount_univ_le_one_iff {X : Type u_1} [TopologicalSpace X] [Nonempty X] : lsCategoryCount X Set.univ ≤ 1 ↔ ContractibleSpace X

On a nonempty space, a cover by one categorical open exists exactly when the space is contractible.

theorem TauCeti.exists_isOpen_mem_lsCategoryCount_le_one {X : Type u_1} [TopologicalSpace X] (hX : LocallyContractibleSpace X) (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ lsCategoryCount X U ≤ 1

In a locally contractible space every point has an open neighbourhood of Lusternik–Schnirelmann count at most 1: the interior of a neighbourhood whose inclusion is nullhomotopic.

theorem TauCeti.exists_isOpen_superset_lsCategoryCount_le_encard {X : Type u_1} [TopologicalSpace X] (hX : LocallyContractibleSpace X) (S : Set X) : ∃ (U : Set X), IsOpen U ∧ S ⊆ U ∧ lsCategoryCount X U ≤ S.encard

In a locally contractible space every set S has an open neighbourhood whose Lusternik–Schnirelmann count is at most the cardinality of S: for finite S, the union of neighbourhoods of count at most 1 of its points.

theorem TauCeti.exists_isOpen_superset_lsCategoryCount_lt_top {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (hX : LocallyContractibleSpace X) : ∃ (U : Set X), IsOpen U ∧ K ⊆ U ∧ lsCategoryCount X U < ⊤

A compact subset of a locally contractible space has an open neighborhood with finite categorical-cover count.

theorem IsCompact.lsCategoryCount_lt_top {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (hX : LocallyContractibleSpace X) : TauCeti.lsCategoryCount X K < ⊤

Compact subsets of locally contractible spaces have finite categorical-cover count.

theorem TauCeti.lsCategoryCount_univ_lt_top {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (hX : LocallyContractibleSpace X) : lsCategoryCount X Set.univ < ⊤

A compact locally contractible space has finite categorical-cover count, including when it is empty.

@[simp]

theorem TauCeti.lsCategoryCount_univ_of_contractibleSpace {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] : lsCategoryCount X Set.univ = 1

A contractible space, in particular a point, has Lusternik–Schnirelmann count 1.

@[simp]

theorem TauCeti.lsCategoryCount_eq_encard {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (A : Set X) : lsCategoryCount X A = A.encard

In a discrete space the Lusternik–Schnirelmann count of a set is its cardinality: a categorical open set has at most one point, and points are open.

theorem TauCeti.lsCategoryCount_eq_sum_inter {X : Type u_1} [TopologicalSpace X] {A : Set X} {ι : Type u_3} [Fintype ι] {C : ι → Set X} (hC : ∀ (i : ι), IsClopen (C i)) (hd : Pairwise (Function.onFun Disjoint C)) (hA : A ⊆ ⋃ (i : ι), C i) : lsCategoryCount X A = ∑ i : ι, lsCategoryCount X (A ∩ C i)

The Lusternik–Schnirelmann count is additive over a finite family of pairwise disjoint clopen sets covering A. A categorical open set meeting one of these clopen sets lies inside it (TauCeti.subset_of_nullhomotopic_of_isClopen), so no open set of a categorical cover of A serves two of them.

@[simp]

theorem TauCeti.lsCategoryCount_image_sigmaMk {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (Y i)] (i : ι) (A : Set (Y i)) : lsCategoryCount ((i : ι) × Y i) (Sigma.mk i '' A) = lsCategoryCount (Y i) A

A summand of a disjoint union has the same Lusternik–Schnirelmann counts in the disjoint union as in itself.

theorem TauCeti.lsCategoryCount_sigma {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (Y i)] [Fintype ι] (A : Set ((i : ι) × Y i)) : lsCategoryCount ((i : ι) × Y i) A = ∑ i : ι, lsCategoryCount (Y i) (Sigma.mk i ⁻¹' A)

The Lusternik–Schnirelmann count of a subset of a finite disjoint union is the sum of the counts of its parts in the summands. Empty summands contribute 0, and the sum is ⊤ as soon as one part has no finite categorical cover.

@[simp]

theorem TauCeti.lsCategoryCount_univ_sigma {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (Y i)] [Fintype ι] : lsCategoryCount ((i : ι) × Y i) Set.univ = ∑ i : ι, lsCategoryCount (Y i) Set.univ

The Lusternik–Schnirelmann count of a finite disjoint union is the sum of the counts of its summands.

theorem TauCeti.lsCategoryCount_preimage_subtypeVal {X : Type u_1} [TopologicalSpace X] {A C : Set X} (hC : IsClopen C) (hA : A ⊆ C) : lsCategoryCount (↑C) (Subtype.val ⁻¹' A) = lsCategoryCount X A

On a clopen set C, the Lusternik–Schnirelmann count of a subset A ⊆ C is the same whether it is computed in the subspace C or in X.

theorem TauCeti.lsCategoryCount_eq_sum_preimage_subtypeVal {X : Type u_1} [TopologicalSpace X] {A : Set X} {ι : Type u_3} [Fintype ι] {C : ι → Set X} (hC : ∀ (i : ι), IsClopen (C i)) (hd : Pairwise (Function.onFun Disjoint C)) (hA : A ⊆ ⋃ (i : ι), C i) : lsCategoryCount X A = ∑ i : ι, lsCategoryCount (↑(C i)) (Subtype.val ⁻¹' A)

Additivity over a finite clopen partition. If finitely many pairwise disjoint clopen sets C i cover A, the Lusternik–Schnirelmann count of A is the sum of the counts of its parts, each computed in the subspace C i.

theorem TauCeti.lsCategoryCount_univ_eq_sum_connectedComponents {X : Type u_1} [TopologicalSpace X] [LocallyConnectedSpace X] [Fintype (ConnectedComponents X)] : lsCategoryCount X Set.univ = ∑ C : ConnectedComponents X, lsCategoryCount (↥C.opens) Set.univ

The component sum formula. The Lusternik–Schnirelmann count of a locally connected space with finitely many connected components is the sum of the counts of its components.

theorem ContinuousMap.HomotopyEquiv.lsCategoryCount_univ_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : TauCeti.lsCategoryCount X Set.univ = TauCeti.lsCategoryCount Y Set.univ

A homotopy equivalence preserves the Lusternik–Schnirelmann count of the whole space.

@[simp]

theorem Homeomorph.lsCategoryCount_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (A : Set X) : TauCeti.lsCategoryCount Y (⇑e '' A) = TauCeti.lsCategoryCount X A

A homeomorphism preserves the Lusternik–Schnirelmann count of every subset.

theorem TauCeti.lsCategoryCount_univ_eq_finsum_connectedComponents {X : Type u_1} [TopologicalSpace X] [Finite (ConnectedComponents X)] : lsCategoryCount X Set.univ = ∑ᶠ (C : ConnectedComponents X), lsCategoryCount (↑(ConnectedComponents.mk ⁻¹' {C})) Set.univ

Component sum formula. The Lusternik–Schnirelmann count of a space with finitely many connected components is the sum of the counts of its components, each regarded as a space in its own right.