refactor(combinatorics/quiver): split into several files (#11006)

This PR splits `combinatorics/quiver.lean` into several files. The main reason for this is to ensure that the category theory library only imports the necessary definitions (and not for example the stuff on arborescences). Also adds some more documentation, and fixes a bug in the definition of weakly connected components.
leanprover-community · Jan 8, 2022 · b181a12 · b181a12
1 parent 9b3fec5
commit b181a12
Show file tree

Hide file tree

Showing 9 changed files with 473 additions and 373 deletions.
diff --git a/src/category_theory/category/basic.lean b/src/category_theory/category/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
 -/
-import combinatorics.quiver
+import combinatorics.quiver.basic
 import tactic.basic
 
 /-!

diff --git a/src/category_theory/path_category.lean b/src/category_theory/path_category.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.eq_to_hom
+import combinatorics.quiver.path
 
 /-!
 # The category paths on a quiver.

diff --git a/src/combinatorics/quiver.lean b/src/combinatorics/quiver.lean