∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubmonoid M)
    ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)