Topologically transitive monoid actions

In this file we define an action of a monoid M on a topological space α to be topologically transitive if for any pair of nonempty open sets U and V in α there exists an m : M such that (m • U) ∩ V is nonempty. We also provide an additive version of this definition and prove basic facts about topologically transitive actions.

Tags

group action, topologically transitive

class AddAction.IsTopologicallyTransitive (M : Type u_1) (α : Type u_2) [AddMonoid M] [TopologicalSpace α] [AddAction M α] : Prop

An action of an additive monoid M on a topological space α is called topologically transitive if for any pair of nonempty open sets U and V in α there exists an m : M such that (m +ᵥ U) ∩ V is nonempty.

• exists_vadd_inter {U V : Set α} : IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), ((m +ᵥ U) ∩ V).Nonempty

class MulAction.IsTopologicallyTransitive (M : Type u_1) (α : Type u_2) [Monoid M] [TopologicalSpace α] [MulAction M α] : Prop

An action of a monoid M on a topological space α is called topologically transitive if for any pair of nonempty open sets U and V in α there exists an m : M such that (m • U) ∩ V is nonempty.

• exists_smul_inter {U V : Set α} : IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (m • U ∩ V).Nonempty

theorem MulAction.isTopologicallyTransitive_iff (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (m • U ∩ V).Nonempty

theorem AddAction.isTopologicallyTransitive_iff (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), ((m +ᵥ U) ∩ V).Nonempty

theorem MulAction.isTopologicallyTransitive_iff_dense_iUnion (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ (m : M), m • U)

An action of a monoid M on α is topologically transitive if and only if for any nonempty open subset U of α the union over the elements of M of images of U is dense in α.

theorem AddAction.isTopologicallyTransitive_iff_dense_iUnion (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ (m : M), m +ᵥ U)

An action of an additive monoid M on α is topologically transitive if and only if for any nonempty open subset U of α the union over the elements of M of images of U is dense in α.

theorem MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ (m : M), (fun (x : α) => m • x) ⁻¹' U)

An action of a monoid M on α is topologically transitive if and only if for any nonempty open subset U of α the union of the preimages of U over the elements of M is dense in α.

theorem AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimage (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ (m : M), (fun (x : α) => m +ᵥ x) ⁻¹' U)

An action of an additive monoid M on α is topologically transitive if and only if for any nonempty open subset U of α the union of the preimages of U over the elements of M is dense in α.

theorem IsOpen.dense_iUnion_smul (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [h : MulAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) : Dense (⋃ (m : M), m • U)

theorem IsOpen.dense_iUnion_vadd (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [h : AddAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) : Dense (⋃ (m : M), m +ᵥ U)

theorem IsOpen.dense_iUnion_preimage_smul (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [h : MulAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) : Dense (⋃ (m : M), (fun (x : α) => m • x) ⁻¹' U)

theorem IsOpen.dense_iUnion_preimage_vadd (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [h : AddAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) : Dense (⋃ (m : M), (fun (x : α) => m +ᵥ x) ⁻¹' U)

theorem IsOpen.dense_of_preimage_smul_invariant (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [MulAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) (hUinv : ∀ (m : M), (fun (x : α) => m • x) ⁻¹' U ⊆ U) : Dense U

Let M be a monoid with a topologically transitive action on α. If U is a nonempty open subset of α and (m • ·) ⁻¹' U ⊆ U for all m : M then U is dense in α.

theorem IsOpen.dense_of_preimage_vadd_invariant (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [AddAction.IsTopologicallyTransitive M α] {U : Set α} (hUo : IsOpen U) (hUne : U.Nonempty) (hUinv : ∀ (m : M), (fun (x : α) => m +ᵥ x) ⁻¹' U ⊆ U) : Dense U

Let M be an additive monoid with a topologically transitive action on α. If U is a nonempty open subset of α and (m +ᵥ ·) ⁻¹' U ⊆ U for all m : M then U is dense in α.

theorem MulAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [h : ContinuousConstSMul M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) => m • x) ⁻¹' U ⊆ U) → Dense U

An action of a monoid M on α that is continuous in the second argument is topologically transitive if and only if any nonempty open subset U of α with (m • ·) ⁻¹' U ⊆ U for all m : M is dense in α.

theorem AddAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [h : ContinuousConstVAdd M α] : IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) => m +ᵥ x) ⁻¹' U ⊆ U) → Dense U

An action of an additive monoid M on α that is continuous in the second argument is topologically transitive if and only if any nonempty open subset U of α with (m +ᵥ ·) ⁻¹' U ⊆ U for all m : M is dense in α.

instance MulAction.isTopologicallyTransitive_of_isMinimal (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [IsMinimal M α] : IsTopologicallyTransitive M α

instance AddAction.isTopologicallyTransitive_of_isMinimal (M : Type u_1) {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [IsMinimal M α] : IsTopologicallyTransitive M α