vadd_singleton_mem_nhds_of_sigmaCompact
theorem vadd_singleton_mem_nhds_of_sigmaCompact :
∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
[inst_3 : TopologicalAddGroup G] [inst_4 : AddAction G X] [inst_5 : SigmaCompactSpace G] [inst_6 : BaireSpace X]
[inst_7 : T2Space X] [inst_8 : ContinuousVAdd G X] [inst_9 : AddAction.IsPretransitive G X] {U : Set G},
U ∈ nhds 0 → ∀ (x : X), U +ᵥ {x} ∈ nhds x
This theorem states that for a sigma-compact topological additive group (G) acting continuously and transitively on a Baire space (X), the orbit map is open around zero. Specifically, for any neighborhood (U) of the zero element in G, the set obtained by adding U element-wise to the singleton set containing a point (x) in X, is a neighborhood of x. This property indicates the local continuity of the action, which implies that the orbit map is open at every point, as shown in `isOpenMap_vadd_of_sigmaCompact`.
More concisely: For a sigma-compact topological additive group acting continuously and transitively on a Baire space, the orbit map is open at every point, i.e., for any neighborhood U of the zero element in the group, the set of points x in the space with U added element-wise forms a neighborhood of x.
|
isOpenMap_vadd_of_sigmaCompact
theorem isOpenMap_vadd_of_sigmaCompact :
∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
[inst_3 : TopologicalAddGroup G] [inst_4 : AddAction G X] [inst_5 : SigmaCompactSpace G] [inst_6 : BaireSpace X]
[inst_7 : T2Space X] [inst_8 : ContinuousVAdd G X] [inst_9 : AddAction.IsPretransitive G X] (x : X),
IsOpenMap fun g => g +ᵥ x
The theorem `isOpenMap_vadd_of_sigmaCompact` states that for a sigma-compact additive group `G` continuously and transitively acting on a Baire space `X`, the orbit map - a function obtained by adding each element of `G` to a fixed element `x` of `X` - is open. This result is a version of the open mapping theorem, which holds notably for the action of a sigma-compact locally compact group on a locally compact space.
More concisely: For a sigma-compact, additive group continuously and transitively acting on a Baire space, the orbit map is an open function.
|
smul_singleton_mem_nhds_of_sigmaCompact
theorem smul_singleton_mem_nhds_of_sigmaCompact :
∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
[inst_3 : TopologicalGroup G] [inst_4 : MulAction G X] [inst_5 : SigmaCompactSpace G] [inst_6 : BaireSpace X]
[inst_7 : T2Space X] [inst_8 : ContinuousSMul G X] [inst_9 : MulAction.IsPretransitive G X] {U : Set G},
U ∈ nhds 1 → ∀ (x : X), U • {x} ∈ nhds x
This theorem states that for a sigma-compact group `G` acting continuously and transitively on a Baire space `X`, if a set `U` is a neighborhood of the identity in `G`, then the set obtained by scaling every point in the singleton set `{x}` by `U` is a neighborhood of `x` in `X`. The implications of this theorem are further discussed in `isOpenMap_smul_of_sigmaCompact`, which states that the orbit map is open around any point in `X` under these conditions.
In more formal mathematical language, this theorem asserts that for all `U` in the neighborhood of the identity in `G`, and for all `x` in `X`, the orbit of `x` under `U` is a neighborhood of `x` in `X` if `G` is a sigma-compact topological group acting continuously, transitively, and continuously scalar multiply on a Baire `T2` space `X`.
More concisely: For a sigma-compact, continuous, transitive, and scalar multiplicatively continuous group action of a topological group `G` on a Baire space `X`, the orbit of any point `x` in `X` under a neighborhood `U` of the identity element in `G` is a neighborhood of `x` in `X`.
|
isOpenMap_smul_of_sigmaCompact
theorem isOpenMap_smul_of_sigmaCompact :
∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
[inst_3 : TopologicalGroup G] [inst_4 : MulAction G X] [inst_5 : SigmaCompactSpace G] [inst_6 : BaireSpace X]
[inst_7 : T2Space X] [inst_8 : ContinuousSMul G X] [inst_9 : MulAction.IsPretransitive G X] (x : X),
IsOpenMap fun g => g • x
This theorem states that if a sigma-compact group is acting continuously and transitively on a Baire space, then the orbit map is open. In other words, for any point in the Baire space, the mapping that sends each element of the group to its corresponding orbit under the group action is an open map. The orbit map being open is a concept from topology that means the image of any open set is also an open set. This is a special case of the open mapping theorem and is especially relevant for the action of a sigma-compact locally compact group on a locally compact space.
More concisely: A sigma-compact group acting continuously and transitively on a Baire space induces an open orbit map.
|
MonoidHom.isOpenMap_of_sigmaCompact
theorem MonoidHom.isOpenMap_of_sigmaCompact :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : SigmaCompactSpace G] {H : Type u_3} [inst_4 : Group H] [inst_5 : TopologicalSpace H]
[inst_6 : BaireSpace H] [inst_7 : T2Space H] [inst_8 : ContinuousMul H] (f : G →* H),
Function.Surjective ⇑f → Continuous ⇑f → IsOpenMap ⇑f
The theorem `MonoidHom.isOpenMap_of_sigmaCompact` states that for any surjective morphism (represented by `f : G →* H`) between two topological groups `G` and `H`, if `G` is sigma-compact and `H` is a Baire space (an example of which is a locally compact group), then `f` is an open map. This is under the conditions that `f` is surjective, continuous, and the multiplication operation in `H` is continuous. An open map is a function where the image of any open set in `G` is also open in `H`.
More concisely: If `f : G →* H` is a continuous, surjective homomorphism between sigma-compact topological groups `G` and a locally compact group `H`, then `f` is an open map.
|