Topological properties of units

This file contains lemmas about the topology of units in topological monoids, including results about submonoid units and units of product spaces.

theorem Submonoid.isOpen_units {M : Type u_1} [TopologicalSpace M] [Monoid M] {U : Submonoid M} (hU : IsOpen ↑U) : IsOpen ↑U.units

If a submonoid is open in a topological monoid, then its units form an open subset of the units of the monoid.

theorem AddSubmonoid.isOpen_addUnits {M : Type u_1} [TopologicalSpace M] [AddMonoid M] {U : AddSubmonoid M} (hU : IsOpen ↑U) : IsOpen ↑U.addUnits

If a submonoid is open in a topological additive monoid, then its additive units form an open subset of the additive units of the monoid.

def ContinuousMulEquiv.piUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] [(i : ι) → TopologicalSpace (M i)] : ((i : ι) → M i)ˣ ≃ₜ* ((i : ι) → (M i)ˣ)

The isomorphism of topological groups between the units of a product and the product of the units.

Equations

• ContinuousMulEquiv.piUnits = { toMulEquiv := MulEquiv.piUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piAddUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] [(i : ι) → TopologicalSpace (M i)] : AddUnits ((i : ι) → M i) ≃ₜ+ ((i : ι) → AddUnits (M i))

The isomorphism of topological additive groups between the additive units of a product and the product of the additive units.

Equations

• ContinuousAddEquiv.piAddUnits = { toAddEquiv := AddEquiv.piAddUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Units.mapContinuousMulEquiv {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) : Mˣ ≃ₜ* Nˣ

Any ContinuousMulEquiv induces a ContinuousMulEquiv on units.

Equations

• Units.mapContinuousMulEquiv f = { toMulEquiv := Units.mapEquiv ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Units.mapContinuousMulEquiv_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) (a✝ : Mˣ) : (mapContinuousMulEquiv f) a✝ = (map ↑↑f) a✝

@[simp]

theorem Units.symm_mapContinuousMulEquiv {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) : (mapContinuousMulEquiv f).symm = mapContinuousMulEquiv f.symm

@[simp]

theorem Units.toMulEquiv_mapContinuousMulEquiv {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) : ↑(mapContinuousMulEquiv f) = mapEquiv ↑f

def toUnits_homeomorph {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ

If G is a group with topological ⁻¹, then it is homeomorphic to its units.

Equations

• toUnits_homeomorph = { toEquiv := toUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def toAddUnits_homeomorph {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] : G ≃ₜ AddUnits G

If G is an additive group with topological negation, then it is homeomorphic to its additive units.

Equations

• toAddUnits_homeomorph = { toEquiv := toAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Units.isEmbedding_val {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] : Topology.IsEmbedding val

theorem AddUnits.isEmbedding_val {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] : Topology.IsEmbedding val

theorem Continuous.of_coeHom_comp {G : Type u_1} {H : Type u_2} [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv G] {f : G →* Hˣ} (hf : Continuous ⇑((Units.coeHom H).comp f)) : Continuous ⇑f

theorem Units.range_embedProduct {α : Type u_3} [Monoid α] : Set.range ⇑(embedProduct α) = {p : α × αᵐᵒᵖ | p.1 * MulOpposite.unop p.2 = 1 ∧ MulOpposite.unop p.2 * p.1 = 1}

theorem AddUnits.range_embedProduct {α : Type u_3} [AddMonoid α] : Set.range ⇑(embedProduct α) = {p : α × αᵃᵒᵖ | p.1 + AddOpposite.unop p.2 = 0 ∧ AddOpposite.unop p.2 + p.1 = 0}

instance Units.instIsTopologicalGroupOfContinuousMul {α : Type u_3} [Monoid α] [TopologicalSpace α] [ContinuousMul α] : IsTopologicalGroup αˣ

instance AddUnits.instIsTopologicalAddGroupOfContinuousAdd {α : Type u_3} [AddMonoid α] [TopologicalSpace α] [ContinuousAdd α] : IsTopologicalAddGroup (AddUnits α)

theorem Units.isClosedEmbedding_embedProduct {α : Type u_3} [Monoid α] [TopologicalSpace α] [T1Space α] [ContinuousMul α] : Topology.IsClosedEmbedding ⇑(embedProduct α)

theorem AddUnits.isClosedEmbedding_embedProduct {α : Type u_3} [AddMonoid α] [TopologicalSpace α] [T1Space α] [ContinuousAdd α] : Topology.IsClosedEmbedding ⇑(embedProduct α)

theorem Topology.IsClosedEmbedding.units_map {α : Type u_3} {β : Type u_4} [Monoid α] [TopologicalSpace α] [Monoid β] [TopologicalSpace β] [ContinuousMul α] [T1Space α] {f : α →* β} (hf : IsClosedEmbedding ⇑f) : IsClosedEmbedding ⇑(Units.map f)

instance Units.instCompactSpaceOfT1SpaceOfContinuousMul {α : Type u_3} [Monoid α] [TopologicalSpace α] [T1Space α] [ContinuousMul α] [CompactSpace α] : CompactSpace αˣ

instance AddUnits.instCompactSpaceOfT1SpaceOfContinuousAdd {α : Type u_3} [AddMonoid α] [TopologicalSpace α] [T1Space α] [ContinuousAdd α] [CompactSpace α] : CompactSpace (AddUnits α)

instance Units.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul {α : Type u_3} [Monoid α] [TopologicalSpace α] [T1Space α] [ContinuousMul α] [WeaklyLocallyCompactSpace α] : WeaklyLocallyCompactSpace αˣ

instance AddUnits.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd {α : Type u_3} [AddMonoid α] [TopologicalSpace α] [T1Space α] [ContinuousAdd α] [WeaklyLocallyCompactSpace α] : WeaklyLocallyCompactSpace (AddUnits α)

instance Units.instLocallyCompactSpaceOfT1SpaceOfContinuousMul {α : Type u_3} [Monoid α] [TopologicalSpace α] [T1Space α] [ContinuousMul α] [LocallyCompactSpace α] : LocallyCompactSpace αˣ

instance AddUnits.instLocallyCompactSpaceOfT1SpaceOfContinuousAdd {α : Type u_3} [AddMonoid α] [TopologicalSpace α] [T1Space α] [ContinuousAdd α] [LocallyCompactSpace α] : LocallyCompactSpace (AddUnits α)

theorem Submonoid.units_isCompact {α : Type u_3} [Monoid α] [TopologicalSpace α] [T1Space α] [ContinuousMul α] {S : Submonoid α} (hS : IsCompact ↑S) : IsCompact ↑S.units

def Homeomorph.prodUnits {α : Type u_3} {β : Type u_4} [Monoid α] [TopologicalSpace α] [Monoid β] [TopologicalSpace β] : (α × β)ˣ ≃ₜ αˣ × βˣ

The topological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.

Equations

• Homeomorph.prodUnits = { toEquiv := MulEquiv.prodUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.prodAddUnits {α : Type u_3} {β : Type u_4} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] : AddUnits (α × β) ≃ₜ AddUnits α × AddUnits β

The topological group isomorphism between the additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Equations

• Homeomorph.prodAddUnits = { toEquiv := AddEquiv.prodAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }