Documentation

Mathlib.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 AddAction.IsMinimal (M : Type u_1) (α : Type u_2) [AddMonoid M] [TopologicalSpace α] [AddAction M α] :

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
    theorem AddAction.IsMinimal.dense_orbit {M : Type u_1} {α : Type u_2} :
    ∀ {inst : AddMonoid M} {inst_1 : TopologicalSpace α} {inst_2 : AddAction M α} [self : AddAction.IsMinimal M α] (x : α), Dense (AddAction.orbit M x)
    class MulAction.IsMinimal (M : Type u_1) (α : Type u_2) [Monoid M] [TopologicalSpace α] [MulAction M α] :

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

    Instances
      theorem MulAction.IsMinimal.dense_orbit {M : Type u_1} {α : Type u_2} :
      ∀ {inst : Monoid M} {inst_1 : TopologicalSpace α} {inst_2 : MulAction M α} [self : MulAction.IsMinimal M α] (x : α), Dense (MulAction.orbit M x)
      theorem AddAction.dense_orbit (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) :
      theorem MulAction.dense_orbit (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) :
      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
      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
      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =
      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
      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
      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
      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
      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
      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
      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 : U.Nonempty) :
      ∃ (I : Finset G), K gI, g +ᵥ U
      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 : U.Nonempty) :
      ∃ (I : Finset G), K gI, g U
      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) (hsmul : ∀ (c : M), c +ᵥ s s) :
      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) :
      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
      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
      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
      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