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 #

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 ?

source

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

add_submonoid M

The additive submonoid fixing a set under an add_action.

Equations

fixing_add_submonoid M s = {carrier := {ϕ : M | ∀ (x : ↥s), ϕ +ᵥ ↑x = ↑x}, add_mem' := _, zero_mem' := _}

source

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

submonoid M

The submonoid fixing a set under a mul_action.

Equations

fixing_submonoid M s = {carrier := {ϕ : M | ∀ (x : ↥s), ϕ • ↑x = ↑x}, mul_mem' := _, one_mem' := _}

source

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

source

theorem fixing_submonoid_fixed_points_gc (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] :

galois_connection (⇑order_dual.to_dual ∘ fixing_submonoid M) ((λ (P : submonoid M), mul_action.fixed_points ↥P α) ∘ ⇑order_dual.of_dual)

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

source

theorem fixing_submonoid_antitone (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] :

antitone (λ (s : set α), fixing_submonoid M s)

source

theorem fixed_points_antitone (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] :

antitone (λ (P : submonoid M), mul_action.fixed_points ↥P α)

source

theorem fixing_submonoid_union (M : Type u_1) (α : Type u_2) [monoid M] [mul_action M α] {s t : set α} :

fixing_submonoid M (s ∪ t) = fixing_submonoid M s ⊓ fixing_submonoid M t

Fixing submonoid of union is intersection

source

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

source

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

mul_action.fixed_points ↥(P ⊔ Q) α = mul_action.fixed_points ↥P α ∩ mul_action.fixed_points ↥Q α

Fixed points of sup of submonoids is intersection

source

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

mul_action.fixed_points ↥(supr P) α = ⋂ (i : ι), mul_action.fixed_points ↥(P i) α

Fixed points of supr of submonoids is intersection

source

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

subgroup M

The subgroup fixing a set under a mul_action.

Equations

fixing_subgroup M s = {carrier := (fixing_submonoid M s).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

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

add_subgroup M

The additive subgroup fixing a set under an add_action.

Equations

fixing_add_subgroup M s = {carrier := (fixing_add_submonoid M s).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

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

source

theorem fixing_subgroup_fixed_points_gc (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] :

galois_connection (⇑order_dual.to_dual ∘ fixing_subgroup M) ((λ (P : subgroup M), mul_action.fixed_points ↥P α) ∘ ⇑order_dual.of_dual)

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

source

theorem fixing_subgroup_antitone (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] :

antitone (fixing_subgroup M)

source

theorem fixed_points_subgroup_antitone (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] :

antitone (λ (P : subgroup M), mul_action.fixed_points ↥P α)

source

theorem fixing_subgroup_union (M : Type u_1) (α : Type u_2) [group M] [mul_action M α] {s t : set α} :

fixing_subgroup M (s ∪ t) = fixing_subgroup M s ⊓ fixing_subgroup M t

Fixing subgroup of union is intersection

source

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

source

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

mul_action.fixed_points ↥(P ⊔ Q) α = mul_action.fixed_points ↥P α ∩ mul_action.fixed_points ↥Q α

Fixed points of sup of subgroups is intersection

source

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

mul_action.fixed_points ↥(supr P) α = ⋂ (i : ι), mul_action.fixed_points ↥(P i) α

Fixed points of supr of subgroups is intersection