Neighborhoods in topological groups

Translation formulas and neighborhood bases at one, continuity criteria for homomorphisms, extensionality and construction results for topological groups, and the multiplicative neighborhood homomorphism.

theorem exists_nhds_split_inv {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : s ∈ nhds 1) : ∃ V ∈ nhds 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

theorem exists_nhds_half_neg {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : s ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v - w ∈ s

theorem nhds_translation_mul_inv {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 * x⁻¹) (nhds 1) = nhds x

theorem nhds_translation_add_neg {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 + -x) (nhds 0) = nhds x

theorem nhds_translation_inv_mul {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x⁻¹ * x_1) (nhds 1) = nhds x

theorem nhds_translation_neg_add {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun (x_1 : G) => -x + x_1) (nhds 0) = nhds x

@[simp]

theorem map_mul_left_nhds {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x * x_1) (nhds y) = nhds (x * y)

@[simp]

theorem map_add_left_nhds {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x + x_1) (nhds y) = nhds (x + y)

theorem map_mul_left_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : Filter.map (fun (x_1 : G) => x * x_1) (nhds 1) = nhds x

theorem map_add_left_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x + x_1) (nhds 0) = nhds x

@[simp]

theorem map_mul_right_nhds {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x_1 * x) (nhds y) = nhds (y * x)

@[simp]

theorem map_add_right_nhds {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x_1 + x) (nhds y) = nhds (y + x)

theorem map_mul_right_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : Filter.map (fun (x_1 : G) => x_1 * x) (nhds 1) = nhds x

theorem map_add_right_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x_1 + x) (nhds 0) = nhds x

theorem Filter.HasBasis.nhds_of_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 1).HasBasis p s) (x : G) : (nhds x).HasBasis p fun (i : ι) => {y : G | y / x ∈ s i}

theorem Filter.HasBasis.nhds_of_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 0).HasBasis p s) (x : G) : (nhds x).HasBasis p fun (i : ι) => {y : G | y - x ∈ s i}

theorem Filter.HasBasis.nhds_of_one' {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 1).HasBasis p s) (x : G) : (nhds x).HasBasis p fun (i : ι) => x • s i

theorem Filter.HasBasis.nhds_of_zero' {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 0).HasBasis p s) (x : G) : (nhds x).HasBasis p fun (i : ι) => x +ᵥ s i

theorem Filter.HasBasis.nhds_one_inv {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Sort u_2} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : (nhds 1).HasBasis p fun (i : ι) => (U i)⁻¹

theorem Filter.HasBasis.nhds_zero_neg {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : (nhds 0).HasBasis p fun (i : ι) => -U i

theorem mem_closure_iff_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 1, ∃ y ∈ s, y / x ∈ U

theorem mem_closure_iff_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 0, ∃ y ∈ s, y - x ∈ U

theorem continuous_of_tendsto_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {M : Type u_2} {hom : Type u_3} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom) (hf : Filter.Tendsto (⇑f) (nhds 1) (nhds 1)) : Continuous ⇑f

A monoid homomorphism (a bundled morphism of a type that implements MonoidHomClass) from a topological group to a topological monoid is continuous provided that it is continuous at one.

This version assumes that f x → 1 as x → 1, saving a rewrite of f 1 = 1 compared to continuous_of_continuousAt_one in some cases. See also uniformContinuous_of_continuousAt_one.

theorem continuous_of_tendsto_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {M : Type u_2} {hom : Type u_3} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : Filter.Tendsto (⇑f) (nhds 0) (nhds 0)) : Continuous ⇑f

An additive monoid homomorphism (a bundled morphism of a type that implements AddMonoidHomClass) from an additive topological group to an additive topological monoid is continuous provided that it is continuous at zero.

This version assumes that f x → 0 as x → 0, saving a rewrite of f 0 = 0 compared to continuous_of_continuousAt_zero in some cases. See also uniformContinuous_of_continuousAt_zero.

theorem continuous_of_continuousAt_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {M : Type u_2} {hom : Type u_3} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (⇑f) 1) : Continuous ⇑f

A monoid homomorphism (a bundled morphism of a type that implements MonoidHomClass) from a topological group to a topological monoid is continuous provided that it is continuous at one. See also uniformContinuous_of_continuousAt_one.

theorem continuous_of_continuousAt_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {M : Type u_2} {hom : Type u_3} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (⇑f) 0) : Continuous ⇑f

An additive monoid homomorphism (a bundled morphism of a type that implements AddMonoidHomClass) from an additive topological group to an additive topological monoid is continuous provided that it is continuous at zero. See also uniformContinuous_of_continuousAt_zero.

theorem continuous_of_continuousAt_one₂ {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Type u_2} {M : Type u_3} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H →* M) (hf : ContinuousAt (fun (x : G × H) => (f x.1) x.2) (1, 1)) (hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 1) : Continuous fun (x : G × H) => (f x.1) x.2

theorem continuous_of_continuousAt_zero₂ {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H →+ M) (hf : ContinuousAt (fun (x : G × H) => (f x.1) x.2) (0, 0)) (hl : ∀ (x : G), ContinuousAt (⇑(f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 0) : Continuous fun (x : G × H) => (f x.1) x.2

theorem IsTopologicalGroup.isInducing_iff_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] {f : F} : Topology.IsInducing ⇑f ↔ nhds 1 = Filter.comap (⇑f) (nhds 1)

theorem IsTopologicalAddGroup.isInducing_iff_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : Topology.IsInducing ⇑f ↔ nhds 0 = Filter.comap (⇑f) (nhds 0)

theorem IsTopologicalGroup.isOpenMap_iff_nhds_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Type u_2} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] {f : F} : IsOpenMap ⇑f ↔ nhds 1 ≤ Filter.map (⇑f) (nhds 1)

theorem IsTopologicalAddGroup.isOpenMap_iff_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} [AddMonoid H] [TopologicalSpace H] [ContinuousConstVAdd H H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : IsOpenMap ⇑f ↔ nhds 0 ≤ Filter.map (⇑f) (nhds 0)

theorem MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type u_2} [Group A] [TopologicalSpace A] [ContinuousMul A] {B : Type u_3} [Group B] [TopologicalSpace B] {F : Type u_4} [FunLike F A B] [MonoidHomClass F A B] {φ : F} (hφ : Topology.IsQuotientMap ⇑φ) : IsOpenQuotientMap ⇑φ

Let A and B be topological groups, and let φ : A → B be a continuous surjective group homomorphism. Assume furthermore that φ is a quotient map (i.e., V ⊆ B is open iff φ⁻¹ V is open). Then φ is an open quotient map, and in particular an open map.

theorem AddMonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type u_2} [AddGroup A] [TopologicalSpace A] [ContinuousAdd A] {B : Type u_3} [AddGroup B] [TopologicalSpace B] {F : Type u_4} [FunLike F A B] [AddMonoidHomClass F A B] {φ : F} (hφ : Topology.IsQuotientMap ⇑φ) : IsOpenQuotientMap ⇑φ

Let A and B be topological additive groups, and let φ : A → B be a continuous surjective additive group homomorphism. Assume furthermore that φ is a quotient map (i.e., V ⊆ B is open iff φ⁻¹ V is open). Then φ is an open quotient map, and in particular an open map.

theorem MonoidHom.isOpenQuotientMap_iff_isQuotientMap {A : Type u_2} [Group A] [TopologicalSpace A] [ContinuousMul A] {B : Type u_3} [Group B] [TopologicalSpace B] {F : Type u_4} [FunLike F A B] [MonoidHomClass F A B] {φ : F} : IsOpenQuotientMap ⇑φ ↔ Topology.IsQuotientMap ⇑φ

theorem AddMonoidHom.isOpenQuotientMap_iff_isQuotientMap {A : Type u_2} [AddGroup A] [TopologicalSpace A] [ContinuousAdd A] {B : Type u_3} [AddGroup B] [TopologicalSpace B] {F : Type u_4} [FunLike F A B] [AddMonoidHomClass F A B] {φ : F} : IsOpenQuotientMap ⇑φ ↔ Topology.IsQuotientMap ⇑φ

theorem IsTopologicalGroup.ext {G : Type u_2} [Group G] {t t' : TopologicalSpace G} (tg : IsTopologicalGroup G) (tg' : IsTopologicalGroup G) (h : nhds 1 = nhds 1) : t = t'

theorem IsTopologicalAddGroup.ext {G : Type u_2} [AddGroup G] {t t' : TopologicalSpace G} (tg : IsTopologicalAddGroup G) (tg' : IsTopologicalAddGroup G) (h : nhds 0 = nhds 0) : t = t'

theorem IsTopologicalGroup.ext_iff {G : Type u_2} [Group G] {t t' : TopologicalSpace G} (tg : IsTopologicalGroup G) (tg' : IsTopologicalGroup G) : t = t' ↔ nhds 1 = nhds 1

theorem IsTopologicalAddGroup.ext_iff {G : Type u_2} [AddGroup G] {t t' : TopologicalSpace G} (tg : IsTopologicalAddGroup G) (tg' : IsTopologicalAddGroup G) : t = t' ↔ nhds 0 = nhds 0

theorem ContinuousInv.of_nhds_one {G : Type u_2} [Group G] [TopologicalSpace G] (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) : ContinuousInv G

theorem ContinuousNeg.of_nhds_zero {G : Type u_2} [AddGroup G] [TopologicalSpace G] (hneg : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (haddConj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) : ContinuousNeg G

theorem IsTopologicalGroup.of_nhds_one' {G : Type u_2} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x * x₀) (nhds 1)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.of_nhds_zero' {G : Type u_2} [AddGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x + x₀) (nhds 0)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.of_nhds_one {G : Type u_2} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.of_nhds_zero {G : Type u_2} [AddGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (haddConj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.of_comm_of_nhds_one {G : Type u_2} [CommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.of_comm_of_nhds_zero {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.exists_antitone_basis_nhds_one (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [FirstCountableTopology G] : ∃ (u : ℕ → Set G), (nhds 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n

Any first countable topological group has an antitone neighborhood basis u : ℕ → Set G for which (u (n + 1)) ^ 2 ⊆ u n. The existence of such a neighborhood basis is a key tool for QuotientGroup.completeSpace_right.

theorem IsTopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [FirstCountableTopology G] : ∃ (u : ℕ → Set G), (nhds 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n

Any first countable topological additive group has an antitone neighborhood basis u : ℕ → set G for which u (n + 1) + u (n + 1) ⊆ u n. The existence of such a neighborhood basis is a key tool for QuotientAddGroup.completeSpace_right.

theorem nhds_mul {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : nhds (x * y) = nhds x * nhds y

theorem nhds_add {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : nhds (x + y) = nhds x + nhds y

def nhdsMulHom {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : G →ₙ* Filter G

On a topological group, 𝓝 : G → Filter G can be promoted to a MulHom.

Equations

• nhdsMulHom = { toFun := nhds, map_mul' := ⋯ }

def nhdsAddHom {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : G →ₙ+ Filter G

On an additive topological group, 𝓝 : G → Filter G can be promoted to an AddHom.

Equations

• nhdsAddHom = { toFun := nhds, map_add' := ⋯ }

@[simp]

theorem nhdsMulHom_apply {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : nhdsMulHom x = nhds x

@[simp]

theorem nhdsAddHom_apply {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : nhdsAddHom x = nhds x