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_3} {M : ι → Type u_4} [(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_3} {M : ι → Type u_4} [(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 := ⋯ }

theorem ContinuousMulEquiv.piUnits_isOpenEmbedding {I : Type u_3} {f : I → Type u_4} [(i : I) → Monoid (f i)] [(i : I) → TopologicalSpace (f i)] : Topology.IsOpenEmbedding ⇑piUnits

Given a family of topological monoids M, (Π i, M i)ˣ → Π i, M i is an open embedding.

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_3} [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_3} [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_3} [Group G] [TopologicalSpace G] [ContinuousInv G] : Topology.IsEmbedding val

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

theorem Continuous.of_coeHom_comp {G : Type u_3} {H : Type u_4} [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_5} [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_5} [AddMonoid α] : Set.range ⇑(embedProduct α) = {p : α × αᵃᵒᵖ | p.1 + AddOpposite.unop p.2 = 0 ∧ AddOpposite.unop p.2 + p.1 = 0}

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

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

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

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

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

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

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

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

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

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

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

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

def Homeomorph.prodUnits {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [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 := ⋯ }

def ContinuousMulEquiv.prodUnits (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] : (M × N)ˣ ≃ₜ* Mˣ × Nˣ

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

Equations

• ContinuousMulEquiv.prodUnits M N = { toMulEquiv := MulEquiv.prodUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.sumAddUnits (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [AddMonoid M] [AddMonoid N] : AddUnits (M × N) ≃ₜ+ AddUnits M × AddUnits N

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

Equations

• ContinuousAddEquiv.sumAddUnits M N = { toAddEquiv := AddEquiv.prodAddUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.val_inv_prodUnits_symm_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (u : Mˣ × Nˣ) : ↑((prodUnits M N).symm u)⁻¹ = (↑u.1⁻¹, ↑u.2⁻¹)

@[simp]

theorem ContinuousMulEquiv.val_prodUnits_symm_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (u : Mˣ × Nˣ) : ↑((prodUnits M N).symm u) = (↑u.1, ↑u.2)

@[simp]

theorem ContinuousMulEquiv.prodUnits_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (a : (M × N)ˣ) : (prodUnits M N) a = ((Units.map (MonoidHom.fst M N)) a, (Units.map (MonoidHom.snd M N)) a)

@[simp]

theorem ContinuousAddEquiv.val_sumAddUnits_symm_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [AddMonoid M] [AddMonoid N] (u : AddUnits M × AddUnits N) : ↑((sumAddUnits M N).symm u) = (↑u.1, ↑u.2)

@[simp]

theorem ContinuousAddEquiv.val_neg_sumAddUnits_symm_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [AddMonoid M] [AddMonoid N] (u : AddUnits M × AddUnits N) : ↑(-(sumAddUnits M N).symm u) = (↑(-u.1), ↑(-u.2))

@[simp]

theorem ContinuousAddEquiv.sumAddUnits_apply (M : Type u_1) (N : Type u_2) [TopologicalSpace M] [TopologicalSpace N] [AddMonoid M] [AddMonoid N] (a : AddUnits (M × N)) : (sumAddUnits M N) a = ((AddUnits.map (AddMonoidHom.fst M N)) a, (AddUnits.map (AddMonoidHom.snd M N)) a)

theorem ContinuousMulEquiv.prodUnits_isOpenEmbedding {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] : Topology.IsOpenEmbedding ⇑(prodUnits M N)

Given two topological monoids M and N, (M × N)ˣ → M × N is an open embedding.

@[simp]

theorem ContinuousMulEquiv.toMulEquiv_prodUnits {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] : ↑(prodUnits M N) = MulEquiv.prodUnits

@[simp]

theorem ContinuousMulEquiv.toHomeomorph_prodUnits {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] : (prodUnits M N).toHomeomorph = Homeomorph.prodUnits