mathlib3 documentation

topology.algebra.semigroup

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.

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.

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

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.

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.