mathlib documentation

dynamics.minimal

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 #

Tags #

group action, minimal

@[class]
structure add_action.is_minimal (M : Type u_1) (α : Type u_2) [add_monoid M] [topological_space α] [add_action 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.

Instances of this typeclass
@[class]
structure mul_action.is_minimal (M : Type u_1) (α : Type u_2) [monoid M] [topological_space α] [mul_action 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.

Instances of this typeclass
theorem add_action.dense_orbit (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] (x : α) :
theorem mul_action.dense_orbit (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] (x : α) :
theorem dense_range_vadd (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] (x : α) :
dense_range (λ (c : M), c +ᵥ x)
theorem dense_range_smul (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] (x : α) :
dense_range (λ (c : M), c x)
@[protected, instance]
@[protected, instance]
theorem is_open.exists_vadd_mem (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] (x : α) {U : set α} (hUo : is_open U) (hne : U.nonempty) :
∃ (c : M), c +ᵥ x U
theorem is_open.exists_smul_mem (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] (x : α) {U : set α} (hUo : is_open U) (hne : U.nonempty) :
∃ (c : M), c x U
theorem is_open.Union_preimage_smul (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(⋃ (c : M), has_smul.smul c ⁻¹' U) = set.univ
theorem is_open.Union_preimage_vadd (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(⋃ (c : M), has_vadd.vadd c ⁻¹' U) = set.univ
theorem is_open.Union_vadd (G : Type u_2) {α : Type u_3} [add_group G] [topological_space α] [add_action G α] [add_action.is_minimal G α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(⋃ (g : G), g +ᵥ U) = set.univ
theorem is_open.Union_smul (G : Type u_2) {α : Type u_3} [group G] [topological_space α] [mul_action G α] [mul_action.is_minimal G α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(⋃ (g : G), g U) = set.univ
theorem is_compact.exists_finite_cover_vadd (G : Type u_2) {α : Type u_3} [add_group G] [topological_space α] [add_action G α] [add_action.is_minimal G α] [has_continuous_const_vadd G α] {K U : set α} (hK : is_compact K) (hUo : is_open U) (hne : U.nonempty) :
∃ (I : finset G), K ⋃ (g : G) (H : g I), g +ᵥ U
theorem is_compact.exists_finite_cover_smul (G : Type u_2) {α : Type u_3} [group G] [topological_space α] [mul_action G α] [mul_action.is_minimal G α] [has_continuous_const_smul G α] {K U : set α} (hK : is_compact K) (hUo : is_open U) (hne : U.nonempty) :
∃ (I : finset G), K ⋃ (g : G) (H : g I), g U
theorem dense_of_nonempty_smul_invariant (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] {s : set α} (hne : s.nonempty) (hsmul : ∀ (c : M), c s s) :
theorem dense_of_nonempty_vadd_invariant (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] {s : set α} (hne : s.nonempty) (hsmul : ∀ (c : M), c +ᵥ s s) :
theorem eq_empty_or_univ_of_vadd_invariant_closed (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [add_action.is_minimal M α] {s : set α} (hs : is_closed s) (hsmul : ∀ (c : M), c +ᵥ s s) :
theorem eq_empty_or_univ_of_smul_invariant_closed (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [mul_action.is_minimal M α] {s : set α} (hs : is_closed s) (hsmul : ∀ (c : M), c s s) :
theorem is_minimal_iff_closed_smul_invariant (M : Type u_1) {α : Type u_3} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_smul M α] :
mul_action.is_minimal M α ∀ (s : set α), is_closed s(∀ (c : M), c s s)s = s = set.univ
theorem is_minimal_iff_closed_vadd_invariant (M : Type u_1) {α : Type u_3} [add_monoid M] [topological_space α] [add_action M α] [has_continuous_const_vadd M α] :
add_action.is_minimal M α ∀ (s : set α), is_closed s(∀ (c : M), c +ᵥ s s)s = s = set.univ