Commit 2022-12-17 06:45 706d88f2

feat(combinatorics/quiver/*): More edge reversal constructions (#17665) Move

• quiver.symmetrify,
• quiver.has_reverse,
• quiver.has_involutive_reverse,
• quiver.reverse,
• quiver.path.reverse,
• quiver.symmetrify.of,
• quiver.lift,
• associated lemmas, from combinatorics/quiver/connected_component.lean to combinatorics/quiver/symmetrify.lean. Add
• the class prefunctor.map_reverse witnessing that a prefunctor maps reverses to reverses, and change the lemmas taking this property as an explicit argument.
• prefunctor.symmetrify mapping a prefunctor to the prefunctor between symmetrifications,
• associated lemmas, to combinatorics/quiver/symmetrify.lean. Move quiver.hom.to_pos and quiver.hom.to_neg from category_theory/groupoid/free_groupoid.lean to combinatorics/quiver/symmetrify.lean. Add map_reverse instance for functors between groupoids.