Definitions/Def_Mathlib_Topology_Algebra_Group_Units.lean

A single auxiliary lemma of topological algebra. Let M be a monoid carrying a topology, and let U be a submonoid of M. Mathlib's Submonoid.units attaches to U the subgroup U^\times of the unit group M^\times consisting of those units u for which both u and u^{-1}, viewed in M, lie in U; as a subset of M^\times it is thus the intersection of the preimages of U under the two maps u \mapsto u and u \mapsto u^{-1} from M^\times to M. The lemma Submonoid.units_isOpen asserts that if U is open as a subset of M, then U^\times is open as a subset of M^\times, the latter being given its usual topology as a unit group, for which both coercion maps M^\times \to M are continuous. No separate continuity hypothesis on the multiplication of M is imposed: the statement is purely about openness of an intersection of two preimages of the open set U. The typical use is with M a topological ring or a profinite monoid and U an open submonoid, to produce open subgroups of M^\times from open submonoids of M, for instance in the construction of neighbourhood bases of the identity in unit groups of topological rings.