A tentative definition of Schreier graphs of groups acting on sets and Cayley graphs as a special case.
More precisely:

• action_graph is the quiver obtained by an action of a group and a choice of letters.
• schreier_graph is the action graph of a group acting on its cosets for a subgroup
• cayley_graph is the schreier graph for the trivial subgroup

More important than just the graphs are the labellings of the arrows, defined as quiver morphism to the single object quiver of letters.

It is then shown that:

• Extending the orbit-stabilizer theorem, orbit_stabilizer_covering_iso essentially shows that the restriction of an action_graph to the orbit of a vertexs is isomorphic to the Schreier graph given by the stabilizer of the vertex.
  Thus, transitive action_graphs are just Schreier graphs
• For Schreier graphs, if the subgroup is normal, there is an action of the group on the graph (preserving the labelling); see the various as_autom lemmas.
• Still in the case of normal subgroups, any automorphism is given by a unique group element, up to the normal subgroup itself (exists_as_autom and as_autom_eq_iff).

It's in a messy state, in great part because:

• I didn't know how to bundle those labelled graphs and their isomorphisms and automorphisms.
• I wasn't sure how much one could and should generalize.

• depends on: [Merged by Bors] - feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths #17828
• depends on: feat(combinatorics/quiver): isomorphisms of quivers #18511