Theorems · Theorem · category theory

CategoryTheory.Paths.induction_fixed_target

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

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

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

1 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Quiver