Documentation

Mathlib.GroupTheory.GroupAction.FixingSubgroup

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 #

TODO :

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

The additive submonoid fixing a set under an AddAction.

Equations
  • One or more equations did not get rendered due to their size.
def fixingAddSubmonoid.proof_1 (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] (s : Set α) {x : M} {y : M} (hx : x { ϕ | ∀ (x : s), ϕ +ᵥ x = x }) (hy : y { ϕ | ∀ (x : s), ϕ +ᵥ x = x }) (z : s) :
x + y +ᵥ z = z
Equations
def fixingAddSubmonoid.proof_2 (M : Type u_2) {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] (s : Set α) :
∀ (x : s), 0 +ᵥ x = x
Equations
def fixingSubmonoid (M : Type u_1) {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] (s : Set α) :

The submonoid fixing a set under a MulAction.

Equations
  • One or more equations did not get rendered due to their size.
theorem mem_fixingSubmonoid_iff (M : Type u_2) {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] {s : Set α} {m : M} :
m fixingSubmonoid M s ∀ (y : α), y sm y = y
theorem fixingSubmonoid_fixedPoints_gc (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] :
GaloisConnection (OrderDual.toDual fixingSubmonoid M) ((fun P => MulAction.fixedPoints { x // x P } α) OrderDual.ofDual)

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

theorem fixingSubmonoid_antitone (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] :
theorem fixedPoints_antitone (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] :
Antitone fun P => MulAction.fixedPoints { x // x P } α
theorem fixingSubmonoid_union (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] {s : Set α} {t : Set α} :

Fixing submonoid of union is intersection

theorem fixingSubmonoid_unionᵢ (M : Type u_3) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] {ι : Sort u_1} {s : ιSet α} :
fixingSubmonoid M (Set.unionᵢ fun i => s i) = i, fixingSubmonoid M (s i)

Fixing submonoid of unionᵢ is intersection

theorem fixedPoints_submonoid_sup (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] {P : Submonoid M} {Q : Submonoid M} :
MulAction.fixedPoints { x // x P Q } α = MulAction.fixedPoints { x // x P } α MulAction.fixedPoints { x // x Q } α

Fixed points of sup of submonoids is intersection

theorem fixedPoints_submonoid_supᵢ (M : Type u_2) (α : Type u_3) [inst : Monoid M] [inst : MulAction M α] {ι : Sort u_1} {P : ιSubmonoid M} :
MulAction.fixedPoints { x // x supᵢ P } α = Set.interᵢ fun i => MulAction.fixedPoints { x // x P i } α

Fixed points of supᵢ of submonoids is intersection

def fixingAddSubgroup.proof_2 (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :
∀ {x : M}, x { toAddSubsemigroup := (fixingAddSubmonoid M s).toAddSubsemigroup, zero_mem' := (_ : 0 (fixingAddSubmonoid M s).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier∀ (z : s), -x +ᵥ z = z
Equations
def fixingAddSubgroup (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :

The additive subgroup fixing a set under an AddAction.

Equations
  • One or more equations did not get rendered due to their size.
def fixingAddSubgroup.proof_1 (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :
0 (fixingAddSubmonoid M s).toAddSubsemigroup.carrier
Equations
def fixingSubgroup (M : Type u_1) {α : Type u_2} [inst : Group M] [inst : MulAction M α] (s : Set α) :

The subgroup fixing a set under a MulAction.

Equations
  • One or more equations did not get rendered due to their size.
theorem mem_fixingSubgroup_iff (M : Type u_2) {α : Type u_1} [inst : Group M] [inst : MulAction M α] {s : Set α} {m : M} :
m fixingSubgroup M s ∀ (y : α), y sm y = y
theorem fixingSubgroup_fixedPoints_gc (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] :
GaloisConnection (OrderDual.toDual fixingSubgroup M) ((fun P => MulAction.fixedPoints { x // x P } α) OrderDual.ofDual)

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

theorem fixingSubgroup_antitone (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] :
theorem fixedPoints_subgroup_antitone (M : Type u_1) (α : Type u_2) [inst : Group M] [inst : MulAction M α] :
Antitone fun P => MulAction.fixedPoints { x // x P } α
theorem fixingSubgroup_union (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] {s : Set α} {t : Set α} :

Fixing subgroup of union is intersection

theorem fixingSubgroup_unionᵢ (M : Type u_3) (α : Type u_2) [inst : Group M] [inst : MulAction M α] {ι : Sort u_1} {s : ιSet α} :
fixingSubgroup M (Set.unionᵢ fun i => s i) = i, fixingSubgroup M (s i)

Fixing subgroup of unionᵢ is intersection

theorem fixedPoints_subgroup_sup (M : Type u_1) (α : Type u_2) [inst : Group M] [inst : MulAction M α] {P : Subgroup M} {Q : Subgroup M} :
MulAction.fixedPoints { x // x P Q } α = MulAction.fixedPoints { x // x P } α MulAction.fixedPoints { x // x Q } α

Fixed points of sup of subgroups is intersection

theorem fixedPoints_subgroup_supᵢ (M : Type u_2) (α : Type u_3) [inst : Group M] [inst : MulAction M α] {ι : Sort u_1} {P : ιSubgroup M} :
MulAction.fixedPoints { x // x supᵢ P } α = Set.interᵢ fun i => MulAction.fixedPoints { x // x P i } α

Fixed points of supᵢ of subgroups is intersection