Minimal action of a group #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
@[class]
structure
add_action.is_minimal
(M : Type u_1)
(α : Type u_2)
[add_monoid M]
[topological_space α]
[add_action M α] :
Prop
- dense_orbit : ∀ (x : α), dense (add_action.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 of this typeclass
@[class]
structure
mul_action.is_minimal
(M : Type u_1)
(α : Type u_2)
[monoid M]
[topological_space α]
[mul_action M α] :
Prop
- dense_orbit : ∀ (x : α), dense (mul_action.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 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 : α) :
dense (add_action.orbit 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 : α) :
dense (mul_action.orbit 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]
def
add_action.is_minimal_of_pretransitive
(M : Type u_1)
{α : Type u_3}
[add_monoid M]
[topological_space α]
[add_action M α]
[add_action.is_pretransitive M α] :
@[protected, instance]
def
mul_action.is_minimal_of_pretransitive
(M : Type u_1)
{α : Type u_3}
[monoid M]
[topological_space α]
[mul_action M α]
[mul_action.is_pretransitive M α] :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
dense 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) :
dense 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 α] :
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 α] :