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 fixingSubmonoid (M : Type u_1) {α : Type u_2} [Monoid M] [MulAction M α] (s : Set α) : Submonoid M

The submonoid fixing a set under a MulAction.

Equations

• fixingSubmonoid M s = { carrier := {ϕ : M | ∀ (x : ↑s), ϕ • ↑x = ↑x}, mul_mem' := ⋯, one_mem' := ⋯ }

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

The additive submonoid fixing a set under an AddAction.

Equations

• fixingAddSubmonoid M s = { carrier := {ϕ : M | ∀ (x : ↑s), ϕ +ᵥ ↑x = ↑x}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem mem_fixingSubmonoid_iff (M : Type u_1) {α : Type u_2} [Monoid M] [MulAction M α] {s : Set α} {m : M} : m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y

theorem mem_fixingAddSubmonoid_iff (M : Type u_1) {α : Type u_2} [AddMonoid M] [AddAction M α] {s : Set α} {m : M} : m ∈ fixingAddSubmonoid M s ↔ ∀ y ∈ s, 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 fixingAddSubmonoid_fixedPoints_gc (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubmonoid M) ((fun (P : AddSubmonoid M) => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)

theorem fixingSubmonoid_antitone (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] : Antitone fun (s : Set α) => fixingSubmonoid M s

theorem fixingAddSubmonoid_antitone (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] : Antitone fun (s : Set α) => fixingAddSubmonoid 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 fixedPoints_antitone_addSubmonoid (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] : Antitone fun (P : AddSubmonoid M) => AddAction.fixedPoints (↥P) α

theorem fixingSubmonoid_union (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {s t : Set α} : fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t

Fixing submonoid of union is intersection

theorem fixingAddSubmonoid_union (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] {s t : Set α} : fixingAddSubmonoid M (s ∪ t) = fixingAddSubmonoid M s ⊓ fixingAddSubmonoid M t

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 fixingAddSubmonoid_iUnion (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] {ι : Sort u_3} {s : ι → Set α} : fixingAddSubmonoid M (⋃ (i : ι), s i) = ⨅ (i : ι), fixingAddSubmonoid M (s i)

theorem fixedPoints_submonoid_sup (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] {P Q : Submonoid M} : MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α

Fixed points of sup of submonoids is intersection

theorem fixedPoints_addSubmonoid_sup (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] {P Q : AddSubmonoid M} : AddAction.fixedPoints (↥(P ⊔ Q)) α = AddAction.fixedPoints (↥P) α ∩ AddAction.fixedPoints (↥Q) α

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

theorem fixedPoints_addSubmonoid_iSup (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] {ι : Sort u_3} {P : ι → AddSubmonoid M} : AddAction.fixedPoints (↥(iSup P)) α = ⋂ (i : ι), AddAction.fixedPoints (↥(P i)) α

def fixingSubgroup (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) : Subgroup M

The subgroup fixing a set under a MulAction.

Equations

• fixingSubgroup M s = { toSubmonoid := fixingSubmonoid M s, inv_mem' := ⋯ }

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

The additive subgroup fixing a set under an AddAction.

Equations

• fixingAddSubgroup M s = { toAddSubmonoid := fixingAddSubmonoid M s, neg_mem' := ⋯ }

theorem mem_fixingSubgroup_iff (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y

theorem mem_fixingAddSubgroup_iff (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {m : M} : m ∈ fixingAddSubgroup M s ↔ ∀ y ∈ s, m +ᵥ y = y

theorem mem_fixingSubgroup_iff_subset_fixedBy (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ s ⊆ MulAction.fixedBy α m

theorem mem_fixingAddSubgroup_iff_subset_fixedBy (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {m : M} : m ∈ fixingAddSubgroup M s ↔ s ⊆ AddAction.fixedBy α m

theorem mem_fixingSubgroup_compl_iff_movedBy_subset (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {m : M} : m ∈ fixingSubgroup M sᶜ ↔ (MulAction.fixedBy α m)ᶜ ⊆ s

theorem mem_fixingAddSubgroup_compl_iff_movedBy_subset (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {m : M} : m ∈ fixingAddSubgroup M sᶜ ↔ (AddAction.fixedBy α m)ᶜ ⊆ s

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 fixingAddSubgroup_fixedPoints_gc (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubgroup M) ((fun (P : AddSubgroup M) => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)

theorem fixingSubgroup_antitone (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] : Antitone (fixingSubgroup M)

theorem fixingAddSubgroup_antitone (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : Antitone (fixingAddSubgroup 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 fixedPoints_addSubgroup_antitone (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : Antitone fun (P : AddSubgroup M) => AddAction.fixedPoints (↥P) α

theorem fixingSubgroup_union (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {s t : Set α} : fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t

Fixing subgroup of union is intersection

theorem fixingAddSubgroup_union (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {s t : Set α} : fixingAddSubgroup M (s ∪ t) = fixingAddSubgroup M s ⊓ fixingAddSubgroup M t

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 fixingAddSubgroup_iUnion (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {ι : Sort u_3} {s : ι → Set α} : fixingAddSubgroup M (⋃ (i : ι), s i) = ⨅ (i : ι), fixingAddSubgroup M (s i)

theorem fixedPoints_subgroup_sup (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {P Q : Subgroup M} : MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α

Fixed points of sup of subgroups is intersection

theorem fixedPoints_addSubgroup_sup (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {P Q : AddSubgroup M} : AddAction.fixedPoints (↥(P ⊔ Q)) α = AddAction.fixedPoints (↥P) α ∩ AddAction.fixedPoints (↥Q) α

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 fixedPoints_addSubgroup_iSup (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {ι : Sort u_3} {P : ι → AddSubgroup M} : AddAction.fixedPoints (↥(iSup P)) α = ⋂ (i : ι), AddAction.fixedPoints (↥(P i)) α

theorem orbit_fixingSubgroup_compl_subset (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {s : Set α} {a : α} (a_in_s : a ∈ s) : MulAction.orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s

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

theorem orbit_fixingAddSubgroup_compl_subset (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {s : Set α} {a : α} (a_in_s : a ∈ s) : AddAction.orbit (↥(fixingAddSubgroup M sᶜ)) a ⊆ s