Separation, neighbourhoods, σ-compactness and preconnected sets in a group of units

The units Mˣ of a topological monoid M carry the topology induced by u ↦ (u, u⁻¹). This file records consequences of that definition.

• The units of a T₁ monoid form a T₁ space, without a continuity assumption on multiplication.
• The neighbourhood filter of a unit u is the meet of the pullbacks of the neighbourhood filters of u and of u⁻¹ along the coercion and the inverse coercion. Concretely, a set is a neighbourhood of u in Mˣ exactly when it contains every unit v with v in a prescribed neighbourhood of u and v⁻¹ in a prescribed neighbourhood of u⁻¹.
• In a T₁ monoid with continuous multiplication, u ↦ (u, u⁻¹) is a closed embedding, so the units of a σ-compact monoid are σ-compact.
• In a group with zero with continuous inversion away from zero, the coercion G₀ˣ → G₀ is a topological embedding, so a preconnected set of nonzero elements pulls back to a preconnected set of units.

Main results

• Units.instT1Space: the T₁ separation property for units.
• Units.nhds_eq_comap_inf: the neighbourhood filter of a unit.
• Units.mem_nhds_iff: the resulting membership criterion for neighbourhoods of a unit.
• Units.instSigmaCompactSpace: the units of a σ-compact monoid are σ-compact.
• IsPreconnected.preimage_units_val: preconnected sets of nonzero elements pull back to preconnected sets of units.

instance Units.instT1Space {M : Type u_1} [Monoid M] [TopologicalSpace M] [T1Space M] : T1Space Mˣ

The units of a T₁ monoid form a T₁ space.

instance AddUnits.instT1Space {M : Type u_1} [AddMonoid M] [TopologicalSpace M] [T1Space M] : T1Space (AddUnits M)

The additive units of a T₁ additive monoid form a T₁ space.

theorem Units.nhds_eq_comap_inf {M : Type u_1} [Monoid M] [TopologicalSpace M] (u : Mˣ) : nhds u = Filter.comap val (nhds ↑u) ⊓ Filter.comap (fun (v : Mˣ) => ↑v⁻¹) (nhds ↑u⁻¹)

The neighbourhood filter of a unit is the meet of the pullbacks of the neighbourhood filters of the unit and of its inverse along the two coercions to M.

theorem Units.mem_nhds_iff {M : Type u_1} [Monoid M] [TopologicalSpace M] {u : Mˣ} {s : Set Mˣ} : s ∈ nhds u ↔ ∃ t ∈ nhds ↑u, ∃ t' ∈ nhds ↑u⁻¹, ∀ (v : Mˣ), ↑v ∈ t → ↑v⁻¹ ∈ t' → v ∈ s

Neighbourhoods of a unit. A set is a neighbourhood of u in Mˣ exactly when it contains every unit v with v in a prescribed neighbourhood of u and v⁻¹ in a prescribed neighbourhood of u⁻¹.

instance Units.instSigmaCompactSpace {M : Type u_1} [Monoid M] [TopologicalSpace M] [T1Space M] [ContinuousMul M] [SigmaCompactSpace M] : SigmaCompactSpace Mˣ

The units of a σ-compact monoid are σ-compact. In a T₁ monoid with continuous multiplication, u ↦ (u, u⁻¹) is a closed embedding of Mˣ into the σ-compact space M × M.

instance AddUnits.instSigmaCompactSpace {M : Type u_1} [AddMonoid M] [TopologicalSpace M] [T1Space M] [ContinuousAdd M] [SigmaCompactSpace M] : SigmaCompactSpace (AddUnits M)

The additive units of a σ-compact additive monoid are σ-compact.

theorem IsPreconnected.preimage_units_val {G₀ : Type u_1} [GroupWithZero G₀] [TopologicalSpace G₀] [ContinuousInv₀ G₀] {s : Set G₀} (hs : IsPreconnected s) (h0 : 0 ∉ s) : IsPreconnected (Units.val ⁻¹' s)

Preconnected sets of nonzero elements pull back to preconnected sets of units. In a group with zero whose inversion is continuous away from zero, the coercion from the units is a topological embedding, so the units lying over a preconnected set of nonzero elements form a preconnected set.