Documentation

Mathlib.GroupTheory.GroupAction.FixingSubgroup

Fixing submonoid, fixing subgroup of an action #

In the presence of an action of a monoid or a group, this file defines the fixing submonoid or the fixing subgroup, and relates it to the set of fixed points via a Galois connection.

Main definitions #

TODO :

def fixingAddSubmonoid (M : Type u_1) {α : Type u_2} [AddMonoid M] [AddAction M α] (s : Set α) :

The additive submonoid fixing a set under an AddAction.

Equations
  • fixingAddSubmonoid M s = { carrier := {ϕ : M | ∀ (x : s), ϕ +ᵥ x = x}, add_mem' := , zero_mem' := }
Instances For
    theorem fixingAddSubmonoid.proof_1 (M : Type u_1) {α : Type u_2} [AddMonoid M] [AddAction M α] (s : Set α) {x : M} {y : M} (hx : x {ϕ : M | ∀ (x : s), ϕ +ᵥ x = x}) (hy : y {ϕ : M | ∀ (x : s), ϕ +ᵥ x = x}) (z : s) :
    x + y +ᵥ z = z
    theorem fixingAddSubmonoid.proof_2 (M : Type u_2) {α : Type u_1} [AddMonoid M] [AddAction M α] (s : Set α) :
    ∀ (x : s), 0 +ᵥ x = x
    def fixingSubmonoid (M : Type u_1) {α : Type u_2} [Monoid M] [MulAction M α] (s : Set α) :

    The submonoid fixing a set under a MulAction.

    Equations
    • fixingSubmonoid M s = { carrier := {ϕ : M | ∀ (x : s), ϕ x = x}, mul_mem' := , one_mem' := }
    Instances For
      theorem mem_fixingSubmonoid_iff (M : Type u_1) {α : Type u_2} [Monoid M] [MulAction M α] {s : Set α} {m : M} :
      m fixingSubmonoid M s ys, m y = y
      theorem fixingSubmonoid_fixedPoints_gc (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] :
      GaloisConnection (OrderDual.toDual fixingSubmonoid M) ((fun (P : Submonoid M) => MulAction.fixedPoints (P) α) OrderDual.ofDual)

      The Galois connection between fixing submonoids and fixed points of a monoid action

      theorem fixingSubmonoid_antitone (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] :
      Antitone fun (s : Set α) => fixingSubmonoid M s
      theorem fixedPoints_antitone (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] :
      Antitone fun (P : Submonoid M) => MulAction.fixedPoints (P) α
      theorem fixingSubmonoid_union (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {s : Set α} {t : Set α} :

      Fixing submonoid of union is intersection

      theorem fixingSubmonoid_iUnion (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {ι : Sort u_3} {s : ιSet α} :
      fixingSubmonoid M (⋃ (i : ι), s i) = ⨅ (i : ι), fixingSubmonoid M (s i)

      Fixing submonoid of iUnion is intersection

      theorem fixedPoints_submonoid_sup (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {P : Submonoid M} {Q : Submonoid M} :

      Fixed points of sup of submonoids is intersection

      theorem fixedPoints_submonoid_iSup (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {ι : Sort u_3} {P : ιSubmonoid M} :
      MulAction.fixedPoints ((iSup P)) α = ⋂ (i : ι), MulAction.fixedPoints ((P i)) α

      Fixed points of iSup of submonoids is intersection

      def fixingAddSubgroup (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) :

      The additive subgroup fixing a set under an AddAction.

      Equations
      Instances For
        theorem fixingAddSubgroup.proof_1 (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) :
        ∀ {x : M}, x (fixingAddSubmonoid M s).carrier∀ (z : s), -x +ᵥ z = z
        def fixingSubgroup (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) :

        The subgroup fixing a set under a MulAction.

        Equations
        Instances For
          theorem mem_fixingSubgroup_iff (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} :
          m fixingSubgroup M s ys, m y = y
          theorem mem_fixingSubgroup_iff_subset_fixedBy (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} :
          theorem mem_fixingSubgroup_compl_iff_movedBy_subset (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} :
          theorem fixingSubgroup_fixedPoints_gc (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] :
          GaloisConnection (OrderDual.toDual fixingSubgroup M) ((fun (P : Subgroup M) => MulAction.fixedPoints (P) α) OrderDual.ofDual)

          The Galois connection between fixing subgroups and fixed points of a group action

          theorem fixingSubgroup_antitone (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] :
          theorem fixedPoints_subgroup_antitone (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] :
          Antitone fun (P : Subgroup M) => MulAction.fixedPoints (P) α
          theorem fixingSubgroup_union (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {s : Set α} {t : Set α} :

          Fixing subgroup of union is intersection

          theorem fixingSubgroup_iUnion (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {ι : Sort u_3} {s : ιSet α} :
          fixingSubgroup M (⋃ (i : ι), s i) = ⨅ (i : ι), fixingSubgroup M (s i)

          Fixing subgroup of iUnion is intersection

          theorem fixedPoints_subgroup_sup (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {P : Subgroup M} {Q : Subgroup M} :

          Fixed points of sup of subgroups is intersection

          theorem fixedPoints_subgroup_iSup (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {ι : Sort u_3} {P : ιSubgroup M} :
          MulAction.fixedPoints ((iSup P)) α = ⋂ (i : ι), MulAction.fixedPoints ((P i)) α

          Fixed points of iSup of subgroups is intersection

          theorem orbit_fixingSubgroup_compl_subset (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {s : Set α} {a : α} (a_in_s : a s) :

          The orbit of the fixing subgroup of sᶜ (ie. the moving subgroup of s) is a subset of s