Idempotents in topological semigroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M : Type u_1} [nonempty M] [semigroup M] [topological_space M] [compact_space M] [t2_space M] (continuous_mul_left : ∀ (r : M), continuous (λ (_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.

source

theorem exists_idempotent_of_compact_t2_of_continuous_add_left {M : Type u_1} [nonempty M] [add_semigroup M] [topological_space M] [compact_space M] [t2_space M] (continuous_mul_left : ∀ (r : M), continuous (λ (_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

source

theorem exists_idempotent_in_compact_add_subsemigroup {M : Type u_1} [add_semigroup M] [topological_space M] [t2_space M] (continuous_mul_left : ∀ (r : M), continuous (λ (_x : M), _x + r)) (s : set M) (snemp : s.nonempty) (s_compact : is_compact s) (s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x + y ∈ s) :

∃ (m : M) (H : 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.

source

theorem exists_idempotent_in_compact_subsemigroup {M : Type u_1} [semigroup M] [topological_space M] [t2_space M] (continuous_mul_left : ∀ (r : M), continuous (λ (_x : M), _x * r)) (s : set M) (snemp : s.nonempty) (s_compact : is_compact s) (s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s) :

∃ (m : M) (H : 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.