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 #

• fixingSubmonoid M s : in the presence of MulAction M α (with Monoid M) it is the Submonoid M consisting of elements which fix s : Set α pointwise.

• fixingSubmonoid_fixedPoints_gc M α is the GaloisConnection that relates fixingSubmonoid with fixedPoints.

• fixingSubgroup M s : in the presence of MulAction M α (with Group M) it is the Subgroup M consisting of elements which fix s : Set α pointwise.

• fixingSubgroup_fixedPoints_gc M α is the GaloisConnection that relates fixingSubgroup with fixedPoints.

TODO :

• Maybe other lemmas are useful

• Treat semigroups ?

• add to_additive for the various lemmas

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

The additive submonoid fixing a set under an AddAction.

Equations
• = { carrier := {ϕ : M | ∀ (x : s), ϕ +ᵥ x = x}, add_mem' := , zero_mem' := }
Instances For
theorem fixingAddSubmonoid.proof_1 (M : Type u_1) {α : Type u_2} [] [] (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} [] [] (s : Set α) :
∀ (x : s), 0 +ᵥ x = x
def fixingSubmonoid (M : Type u_1) {α : Type u_2} [] [] (s : Set α) :

The submonoid fixing a set under a MulAction.

Equations
• = { carrier := {ϕ : M | ∀ (x : s), ϕ x = x}, mul_mem' := , one_mem' := }
Instances For
theorem mem_fixingSubmonoid_iff (M : Type u_1) {α : Type u_2} [] [] {s : Set α} {m : M} :
m ys, m y = y
theorem fixingSubmonoid_fixedPoints_gc (M : Type u_1) (α : Type u_2) [] [] :
GaloisConnection (OrderDual.toDual ) ((fun (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) [] [] :
Antitone fun (s : Set α) =>
theorem fixedPoints_antitone (M : Type u_1) (α : Type u_2) [] [] :
Antitone fun (P : ) =>
theorem fixingSubmonoid_union (M : Type u_1) (α : Type u_2) [] [] {s : Set α} {t : Set α} :

Fixing submonoid of union is intersection

theorem fixingSubmonoid_iUnion (M : Type u_1) (α : Type u_2) [] [] {ι : 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) [] [] {P : } {Q : } :

Fixed points of sup of submonoids is intersection

theorem fixedPoints_submonoid_iSup (M : Type u_1) (α : Type u_2) [] [] {ι : Sort u_3} {P : ι} :
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} [] [] (s : Set α) :

The additive subgroup fixing a set under an AddAction.

Equations
• = let __src := ; { toAddSubmonoid := __src, neg_mem' := }
Instances For
theorem fixingAddSubgroup.proof_1 (M : Type u_1) {α : Type u_2} [] [] (s : Set α) :
∀ {x : M}, x ().carrier∀ (z : s), -x +ᵥ z = z
def fixingSubgroup (M : Type u_1) {α : Type u_2} [] [] (s : Set α) :

The subgroup fixing a set under a MulAction.

Equations
• = let __src := ; { toSubmonoid := __src, inv_mem' := }
Instances For
theorem mem_fixingSubgroup_iff (M : Type u_1) {α : Type u_2} [] [] {s : Set α} {m : M} :
m ys, m y = y
theorem mem_fixingSubgroup_iff_subset_fixedBy (M : Type u_1) {α : Type u_2} [] [] {s : Set α} {m : M} :
m s
theorem mem_fixingSubgroup_compl_iff_movedBy_subset (M : Type u_1) {α : Type u_2} [] [] {s : Set α} {m : M} :
m () s
theorem fixingSubgroup_fixedPoints_gc (M : Type u_1) (α : Type u_2) [] [] :
GaloisConnection (OrderDual.toDual ) ((fun (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) [] [] :
theorem fixedPoints_subgroup_antitone (M : Type u_1) (α : Type u_2) [] [] :
Antitone fun (P : ) =>
theorem fixingSubgroup_union (M : Type u_1) (α : Type u_2) [] [] {s : Set α} {t : Set α} :

Fixing subgroup of union is intersection

theorem fixingSubgroup_iUnion (M : Type u_1) (α : Type u_2) [] [] {ι : 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) [] [] {P : } {Q : } :

Fixed points of sup of subgroups is intersection

theorem fixedPoints_subgroup_iSup (M : Type u_1) (α : Type u_2) [] [] {ι : Sort u_3} {P : ι} :
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) [] [] {s : Set α} {a : α} (a_in_s : a s) :
MulAction.orbit (()) a s

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