Idempotents in topological semigroups

This file provides a sufficient condition for a semigroup M to contain an idempotent (i.e. an element m such that m * m = m ), namely that M is a nonempty compact Hausdorff space where right-multiplication by constants is continuous.

We also state a corresponding lemma guaranteeing that a subset of M contains an idempotent.

theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M : Type u_1} [Nonempty M] [Semigroup M] [TopologicalSpace M] [CompactSpace M] [T2Space M] (continuous_mul_left : ∀ (r : M), Continuous fun (x : M) => x * r) : ∃ (m : M), m * m = m

Any nonempty compact Hausdorff semigroup where right-multiplication is continuous contains an idempotent, i.e. an m such that m * m = m.

theorem exists_idempotent_of_compact_t2_of_continuous_add_left {M : Type u_1} [Nonempty M] [AddSemigroup M] [TopologicalSpace M] [CompactSpace M] [T2Space M] (continuous_mul_left : ∀ (r : M), Continuous fun (x : M) => x + r) : ∃ (m : M), m + m = m

Any nonempty compact Hausdorff additive semigroup where right-addition is continuous contains an idempotent, i.e. an m such that m + m = m

theorem exists_idempotent_in_compact_subsemigroup {M : Type u_1} [Semigroup M] [TopologicalSpace M] [T2Space M] (continuous_mul_left : ∀ (r : M), Continuous fun (x : M) => x * r) (s : Set M) (snemp : s.Nonempty) (s_compact : IsCompact s) (s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s) : ∃ m ∈ s, m * m = m

A version of exists_idempotent_of_compact_t2_of_continuous_mul_left where the idempotent lies in some specified nonempty compact subsemigroup.

theorem exists_idempotent_in_compact_add_subsemigroup {M : Type u_1} [AddSemigroup M] [TopologicalSpace M] [T2Space M] (continuous_mul_left : ∀ (r : M), Continuous fun (x : M) => x + r) (s : Set M) (snemp : s.Nonempty) (s_compact : IsCompact s) (s_add : ∀ x ∈ s, ∀ y ∈ s, x + y ∈ s) : ∃ m ∈ s, m + m = m

A version of exists_idempotent_of_compact_t2_of_continuous_add_left where the idempotent lies in some specified nonempty compact additive subsemigroup.