Theorems · Theorem · category theory

CategoryTheory.Paths.induction_fixed_source

∀ {V : Type u₁} [inst : Quiver V] {a : CategoryTheory.Paths V} (P : {b : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  P (CategoryTheory.CategoryStruct.id a) →
    (∀ {u v : V} (p : a ⟶ (CategoryTheory.Paths.of V).obj u) (q : u ⟶ v),
        P p → P (CategoryTheory.CategoryStruct.comp p ((CategoryTheory.Paths.of V).map q))) →
      ∀ {b : CategoryTheory.Paths V} (f : a ⟶ b), P f

To prove a property on morphisms of a path category with given source a, it suffices to prove it for the identity and prove that the property is preserved under composition on the right with length 1 paths.

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

Quiver