# mathlibdocumentation

group_theory.group_action.fixing_subgroup

# Fixing submonoid, fixing subgroup of an action #

In the presence of 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 #

• fixing_submonoid M s : in the presence of mul_action M α (with monoid M) it is the submonoid M consisting of elements which fix s : set α pointwise.

• fixing_submonoid_fixed_points_gc M α is the galois_connection that relates fixing_submonoid with fixed_points.

• fixing_subgroup M s : in the presence of mul_action M α (with group M) it is the subgroup M consisting of elements which fix s : set α pointwise.

• fixing_subgroup_fixed_points_gc M α is the galois_connection that relates fixing_subgroup with fixed_points.

TODO :

• Maybe other lemmas are useful

• Treat semigroups ?

def fixing_add_submonoid (M : Type u_1) {α : Type u_2} [add_monoid M] [ α] (s : set α) :

The additive submonoid fixing a set under an add_action.

Equations
def fixing_submonoid (M : Type u_1) {α : Type u_2} [monoid M] [ α] (s : set α) :

The submonoid fixing a set under a mul_action.

Equations
theorem mem_fixing_submonoid_iff (M : Type u_1) {α : Type u_2} [monoid M] [ α] {s : set α} {m : M} :
m ∀ (y : α), y sm y = y
theorem fixing_submonoid_fixed_points_gc (M : Type u_1) (α : Type u_2) [monoid M] [ α] :

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

theorem fixing_submonoid_antitone (M : Type u_1) (α : Type u_2) [monoid M] [ α] :
antitone (λ (s : set α), s)
theorem fixed_points_antitone (M : Type u_1) (α : Type u_2) [monoid M] [ α] :
antitone (λ (P : ,
theorem fixing_submonoid_union (M : Type u_1) (α : Type u_2) [monoid M] [ α] {s t : set α} :
(s t) =

Fixing submonoid of union is intersection

theorem fixing_submonoid_Union (M : Type u_1) (α : Type u_2) [monoid M] [ α] {ι : Sort u_3} {s : ι → set α} :
(⋃ (i : ι), s i) = ⨅ (i : ι), (s i)

Fixing submonoid of Union is intersection

theorem fixed_points_submonoid_sup (M : Type u_1) (α : Type u_2) [monoid M] [ α] {P Q : submonoid M} :
α =

Fixed points of sup of submonoids is intersection

theorem fixed_points_submonoid_supr (M : Type u_1) (α : Type u_2) [monoid M] [ α] {ι : Sort u_3} {P : ι → } :
= ⋂ (i : ι), α

Fixed points of supr of submonoids is intersection

def fixing_subgroup (M : Type u_1) {α : Type u_2} [group M] [ α] (s : set α) :

The subgroup fixing a set under a mul_action.

Equations
def fixing_add_subgroup (M : Type u_1) {α : Type u_2} [add_group M] [ α] (s : set α) :

The additive subgroup fixing a set under an add_action.

Equations
theorem mem_fixing_subgroup_iff (M : Type u_1) {α : Type u_2} [group M] [ α] {s : set α} {m : M} :
m ∀ (y : α), y sm y = y
theorem fixing_subgroup_fixed_points_gc (M : Type u_1) (α : Type u_2) [group M] [ α] :

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

theorem fixing_subgroup_antitone (M : Type u_1) (α : Type u_2) [group M] [ α] :
theorem fixed_points_subgroup_antitone (M : Type u_1) (α : Type u_2) [group M] [ α] :
antitone (λ (P : subgroup M),
theorem fixing_subgroup_union (M : Type u_1) (α : Type u_2) [group M] [ α] {s t : set α} :
(s t) =

Fixing subgroup of union is intersection

theorem fixing_subgroup_Union (M : Type u_1) (α : Type u_2) [group M] [ α] {ι : Sort u_3} {s : ι → set α} :
(⋃ (i : ι), s i) = ⨅ (i : ι), (s i)

Fixing subgroup of Union is intersection

theorem fixed_points_subgroup_sup (M : Type u_1) (α : Type u_2) [group M] [ α] {P Q : subgroup M} :
α =

Fixed points of sup of subgroups is intersection

theorem fixed_points_subgroup_supr (M : Type u_1) (α : Type u_2) [group M] [ α] {ι : Sort u_3} {P : ι → } :
= ⋂ (i : ι), α

Fixed points of supr of subgroups is intersection