Orbital and Fixed Point Functors

This lecture formalizes and generalizes the construction of orbits and fixed points of a group action to any category, describing it in terms of adjunctions. Functors for orbits and fixed points for group sets are constructed, showing they are left and right adjoints to the functor providing a set with a trivial group action. The lecture also covers how to define morphisms, the naturalness of certain applications, and the verification of naturalness in the context of group actions.