feat(CategoryTheory): add MorphismProperty.paths

Mathlib/CategoryTheory/PathCategory/Basic.lean

@@ -5,9 +5,8 @@ Authors: Kim Morrison, Robin Carlier
 -/
 module
 
-public import Mathlib.CategoryTheory.EqToHom
+public import Mathlib.CategoryTheory.MorphismProperty.Composition
 public import Mathlib.CategoryTheory.Quotient
-public import Mathlib.Combinatorics.Quiver.Path
 
 /-!
 # The category paths on a quiver.
@@ -22,7 +21,6 @@ We check that the quotient of the path category of a category by the canonical r
 
 @[expose] public section
 
-
 universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
@@ -287,4 +285,83 @@ def quotientPathsEquiv : Quotient (pathsHomRel C) ≌ C where
 
 end
 
+namespace MorphismProperty
+
+variable {C : Type*} [Category* C]
+
+open Quiver
+
+/-- For any morphism property `W` on `C`, `W.paths` is the morphism property on `Paths C`
+containing all paths of morphisms in `W`. -/
+def paths (W : MorphismProperty C) : MorphismProperty (Paths C) :=
+  fun _ _ p ↦ p.rec True fun _ f P ↦ P ∧ W f
+
+@[simp]
+lemma nil_mem_paths {W : MorphismProperty C} {X : C} : W.paths (.nil (a := X)) := trivial
+
+lemma cons_mem_paths {W : MorphismProperty C} {X Y Z : C} {p : Path X Y} {f : Y ⟶ Z}
+    (hp : W.paths p) (hf : W f) : W.paths (p.cons f) :=
+  ⟨hp, hf⟩
+
+@[simp]
+lemma cons_mem_paths_iff {W : MorphismProperty C} {X Y Z : C} {p : Path X Y} {f : Y ⟶ Z} :
+    W.paths (p.cons f) ↔ W.paths p ∧ W f :=
+  Iff.rfl
+
+lemma toPath_mem_paths {W : MorphismProperty C} {X Y : C} {f : X ⟶ Y} (hf : W f) :
+    W.paths f.toPath :=
+  ⟨trivial, hf⟩
+
+@[simp]
+lemma toPath_mem_paths_iff {W : MorphismProperty C} {X Y : C} {f : X ⟶ Y} :
+    W.paths f.toPath ↔ W f :=
+  ⟨fun h ↦ h.2, fun h ↦ ⟨trivial, h⟩⟩
+
+@[simp]
+lemma comp_mem_paths_iff {W : MorphismProperty C} {X Y Z : C} {p : Path X Y} {q : Path Y Z} :
+    W.paths (p.comp q) ↔ W.paths p ∧ W.paths q := by
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
+  · induction q with
+    | nil => simpa using h
+    | cons q' f h' =>
+      rw [Path.comp_cons] at h
+      exact h' h.1
+  · induction q with
+    | nil => simp
+    | cons q' f h' =>
+      rw [Path.comp_cons] at h
+      exact ⟨h' h.1, h.2⟩
+  · induction q with
+    | nil => exact hp
+    | cons q q' h => exact ⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩
+
+instance (W : MorphismProperty C) : W.paths.IsMultiplicative where
+  id_mem _ := nil_mem_paths
+  comp_mem _ _ hf hg := W.comp_mem_paths_iff.2 ⟨hf, hg⟩
+
+@[gcongr]
+lemma monotone_paths : Monotone (paths (C := C)) :=
+  fun _ _ h _ _ p ↦ p.rec (fun _ ↦ trivial) (fun _ _ hp' hp ↦ ⟨hp' hp.1, h _ hp.2⟩)
+
+lemma composePath_mem' (W : MorphismProperty C) [W.IsStableUnderComposition] {X Y : C}
+    {p : Path X Y} (hp : W.paths p) (h : 0 < p.length ∨ W (𝟙 X)) : W (composePath p) := by
+  obtain hp' | hX := h
+  · revert hp hp'
+    refine p.rec (by simp) fun p f hp hp' hp'' ↦ ?_
+    cases p
+    · simpa [paths] using hp'
+    · refine W.comp_mem _ _ (hp hp'.1 (by simp)) hp'.2
+  · revert hp
+    exact p.rec (fun _ ↦ hX) fun p f hp hp' ↦ W.comp_mem _ _ (hp hp'.1) hp'.2
+
+lemma composePath_mem (W : MorphismProperty C) [W.IsMultiplicative] {X Y : C}
+    {p : Path X Y} (hp : W.paths p) : W (composePath p) :=
+  W.composePath_mem' hp <| .inr (W.id_mem X)
+
+lemma paths_le_inverseImage (W : MorphismProperty C) [W.IsMultiplicative] :
+    W.paths ≤ W.inverseImage (pathComposition C) :=
+  fun _ _ _ ↦ W.composePath_mem
+
+end MorphismProperty
+
 end CategoryTheory