mathlib3 documentation

group_theory.group_action.fixing_subgroup

Fixing submonoid, fixing subgroup of an action #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

TODO :

def fixing_add_submonoid (M : Type u_1) {α : Type u_2} [add_monoid M] [add_action 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] [mul_action 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] [mul_action M α] {s : set α} {m : M} :
m fixing_submonoid M s (y : α), y s m y = y

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] [mul_action M α] :
antitone (λ (s : set α), fixing_submonoid M s)
theorem fixed_points_antitone (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] :
theorem fixing_submonoid_union (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] {s t : set α} :

Fixing submonoid of union is intersection

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

Fixing submonoid of Union is intersection

Fixed points of sup of submonoids is intersection

theorem fixed_points_submonoid_supr (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] {ι : Sort u_3} {P : ι submonoid M} :

Fixed points of supr of submonoids is intersection

def fixing_subgroup (M : Type u_1) {α : Type u_2} [group M] [mul_action 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] [add_action 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] [mul_action M α] {s : set α} {m : M} :
m fixing_subgroup M s (y : α), y s m y = y

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] [mul_action M α] :
theorem fixed_points_subgroup_antitone (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] :
theorem fixing_subgroup_union (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] {s t : set α} :

Fixing subgroup of union is intersection

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

Fixing subgroup of Union is intersection

Fixed points of sup of subgroups is intersection

theorem fixed_points_subgroup_supr (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] {ι : Sort u_3} {P : ι subgroup M} :

Fixed points of supr of subgroups is intersection