# Minimal action of a group #

In this file we define an action of a monoid `M` on a topological space `α` to be minimal if the `M`-orbit of every point `x : α` is dense. We also provide an additive version of this definition and prove some basic facts about minimal actions.

## TODO #

- Define a minimal set of an action.

## Tags #

group action, minimal

source
class AddAction.IsMinimal (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 minimal if the `M`-orbit of every point `x : α` is dense.

- dense_orbit (x : α) : Dense (orbit M x)

Instances

source
class MulAction.IsMinimal (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 minimal if the `M`-orbit of every point `x : α` is dense.

- dense_orbit (x : α) : Dense (orbit M x)

Instances

source
theorem MulAction.dense_orbit (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [IsMinimal M α] (x : α) :
Dense (orbit M x)
source
theorem AddAction.dense_orbit (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [IsMinimal M α] (x : α) :
Dense (orbit M x)
source
theorem denseRange_smul (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) :
DenseRange fun (c : M) => c • x
source
theorem denseRange_vadd (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) :
DenseRange fun (c : M) => c +ᵥ x
source
@[instance 100]
instance MulAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [IsPretransitive M α] :
IsMinimal M α
source
@[instance 100]
instance AddAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [IsPretransitive M α] :
IsMinimal M α
source
theorem IsOpen.exists_smul_mem (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
∃ (c : M), c • x ∈ U
source
theorem IsOpen.exists_vadd_mem (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
∃ (c : M), c +ᵥ x ∈ U
source
theorem IsOpen.iUnion_preimage_smul (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
⋃ (c : M), (fun (x : α) => c • x) ⁻¹' U = Set.univ
source
theorem IsOpen.iUnion_preimage_vadd (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
⋃ (c : M), (fun (x : α) => c +ᵥ x) ⁻¹' U = Set.univ
source
theorem IsOpen.iUnion_smul (G : Type u_2) {α : Type u_3} [Group G] [TopologicalSpace α] [MulAction G α] [MulAction.IsMinimal G α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
⋃ (g : G), g • U = Set.univ
source
theorem IsOpen.iUnion_vadd (G : Type u_2) {α : Type u_3} [AddGroup G] [TopologicalSpace α] [AddAction G α] [AddAction.IsMinimal G α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
⋃ (g : G), g +ᵥ U = Set.univ
source
theorem IsCompact.exists_finite_cover_smul (G : Type u_2) {α : Type u_3} [Group G] [TopologicalSpace α] [MulAction G α] [MulAction.IsMinimal G α] [ContinuousConstSMul G α] {K U : Set α} (hK : IsCompact K) (hUo : IsOpen U) (hne : U.Nonempty) :
∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g • U
source
theorem IsCompact.exists_finite_cover_vadd (G : Type u_2) {α : Type u_3} [AddGroup G] [TopologicalSpace α] [AddAction G α] [AddAction.IsMinimal G α] [ContinuousConstVAdd G α] {K U : Set α} (hK : IsCompact K) (hUo : IsOpen U) (hne : U.Nonempty) :
∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U
source
theorem dense_of_nonempty_smul_invariant (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] {s : Set α} (hne : s.Nonempty) (hsmul : ∀ (c : M), c • s ⊆ s) :
Dense s
source
theorem dense_of_nonempty_vadd_invariant (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] {s : Set α} (hne : s.Nonempty) (hvadd : ∀ (c : M), c +ᵥ s ⊆ s) :
Dense s
source
theorem eq_empty_or_univ_of_smul_invariant_closed (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] {s : Set α} (hs : IsClosed s) (hsmul : ∀ (c : M), c • s ⊆ s) :
s = ∅ ∨ s = Set.univ
source
theorem eq_empty_or_univ_of_vadd_invariant_closed (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] {s : Set α} (hs : IsClosed s) (hvadd : ∀ (c : M), c +ᵥ s ⊆ s) :
s = ∅ ∨ s = Set.univ
source
theorem isMinimal_iff_isClosed_smul_invariant (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] :
MulAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = Set.univ
source
theorem isMinimal_iff_isClosed_vadd_invariant (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [ContinuousConstVAdd M α] :
AddAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c +ᵥ s ⊆ s) → s = ∅ ∨ s = Set.univ