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

dense_orbit : ∀ (x : α), Dense (AddAction.orbit M x)

An action of an additive monoid M on a topological space is called minimal if the M-orbit of every point x : α is dense.

Instances

source

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

Prop

dense_orbit : ∀ (x : α), Dense (MulAction.orbit M x)

An action of a monoid M on a topological space is called minimal if the M-orbit of every point x : α is dense.

Instances

source

theorem AddAction.dense_orbit (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) :

Dense (AddAction.orbit M x)

source

theorem MulAction.dense_orbit (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) :

Dense (MulAction.orbit M x)

source

theorem denseRange_vadd (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) :

DenseRange fun c => c +ᵥ x

source

theorem denseRange_smul (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) :

DenseRange fun c => c • x

source

instance AddAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsPretransitive M α] :

AddAction.IsMinimal M α

Equations

AddAction.isMinimal_of_pretransitive = AddAction.isMinimal_of_pretransitive.proof_1

source

theorem AddAction.isMinimal_of_pretransitive.proof_1 (M : Type u_1) {α : Type u_2} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsPretransitive M α] :

AddAction.IsMinimal M α

source

instance MulAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsPretransitive M α] :

MulAction.IsMinimal M α

Equations

MulAction.isMinimal_of_pretransitive = MulAction.isMinimal_of_pretransitive.proof_1

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 : Set.Nonempty U) :

∃ c, c +ᵥ x ∈ U

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 : Set.Nonempty U) :

∃ c, c • x ∈ U

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 : Set.Nonempty U) :

⋃ (c : M), (fun x x_1 => x +ᵥ x_1) c ⁻¹' U = Set.univ

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 : Set.Nonempty U) :

⋃ (c : M), (fun x x_1 => x • x_1) c ⁻¹' U = Set.univ

source

abbrev IsOpen.iUnion_vadd.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} (x : α) (motive : (∃ c, c +ᵥ x ∈ U) → Prop) :

(x : ∃ c, c +ᵥ x ∈ U) → ((g : G) → (hg : g +ᵥ x ∈ U) → motive (_ : ∃ c, c +ᵥ x ∈ U)) → motive x

Equations

IsOpen.iUnion_vadd.match_1 G x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

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 : Set.Nonempty U) :

⋃ (g : G), g +ᵥ 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 : Set.Nonempty U) :

⋃ (g : G), g • U = Set.univ

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 : Set α} {U : Set α} (hK : IsCompact K) (hUo : IsOpen U) (hne : Set.Nonempty U) :

∃ I, K ⊆ ⋃ (g : G) (_ : g ∈ I), g +ᵥ U

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 : Set α} {U : Set α} (hK : IsCompact K) (hUo : IsOpen U) (hne : Set.Nonempty U) :

∃ I, K ⊆ ⋃ (g : G) (_ : g ∈ I), g • U

source

abbrev dense_of_nonempty_vadd_invariant.match_1 {α : Type u_1} {s : Set α} (motive : Set.Nonempty s → Prop) :

(hne : Set.Nonempty s) → ((x : α) → (hx : x ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive hne

Equations

dense_of_nonempty_vadd_invariant.match_1 motive hne h_1 = Exists.casesOn hne fun w h => h_1 w h

Instances For

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 : Set.Nonempty s) (hsmul : ∀ (c : M), c +ᵥ s ⊆ s) :

Dense s

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 : Set.Nonempty s) (hsmul : ∀ (c : M), c • s ⊆ s) :

Dense s

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) (hsmul : ∀ (c : M), c +ᵥ s ⊆ s) :

s = ∅ ∨ s = Set.univ

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 isMinimal_iff_closed_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

source

theorem isMinimal_iff_closed_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