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 #
-
fixingSubmonoid M s
: in the presence ofMulAction M α
(withmonoid M
) it is theSubmonoid M
consisting of elements which fixs : Set α
pointwise. -
fixingSubmonoid_fixedPoints_gc M α
is theGaloisConnection
that relatesfixingSubmonoid
withfixedPoints
. -
fixingSubgroup M s
: in the presence ofMulAction M α
(withGroup M
) it is theSubgroup M
consisting of elements which fixs : Set α
pointwise. -
fixingSubgroup_fixedPoints_gc M α
is theGaloisConnection
that relatesfixingSubgroup
withfixedPoints
.
TODO :
-
Maybe other lemmas are useful
-
Treat semigroups ?
The Galois connection between fixing submonoids and fixed points of a monoid action
Fixing submonoid of union is intersection
Fixing submonoid of unionᵢ is intersection
Fixed points of sup of submonoids is intersection
Fixed points of supᵢ of submonoids is intersection
Equations
- (_ : 0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier) = (_ : 0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier)
The Galois connection between fixing subgroups and fixed points of a group action
Fixing subgroup of union is intersection
Fixing subgroup of unionᵢ is intersection
Fixed points of sup of subgroups is intersection
Fixed points of supᵢ of subgroups is intersection