Documentation

Mathlib.CategoryTheory.PathCategory.MorphismProperty

Properties of morphisms in a path category. #

We provide a formulation of induction principles for morphisms in a path category in terms of MorphismProperty. This file is separate from CategoryTheory.PathCategory.Basic in order to reduce transitive imports.

source
theorem CategoryTheory.Paths.morphismProperty_eq_top (V : Type u₁) [Quiver V] (P : MorphismProperty (Paths V)) (id : ∀ {v : V}, P (CategoryStruct.id ((of V).obj v))) (comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (CategoryStruct.comp p ((of V).map q))) :
P = ⊤

A reformulation of CategoryTheory.Paths.induction in terms of MorphismProperty.

source
theorem CategoryTheory.Paths.morphismProperty_eq_top' (V : Type u₁) [Quiver V] (P : MorphismProperty (Paths V)) (id : ∀ {v : V}, P (CategoryStruct.id ((of V).obj v))) (comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P (CategoryStruct.comp ((of V).map p) q)) :
P = ⊤

A reformulation of CategoryTheory.Paths.induction' in terms of MorphismProperty.

source
theorem CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative (V : Type u₁) [Quiver V] (P : MorphismProperty (Paths V)) [P.IsMultiplicative] (hP : ∀ {u v : V} (p : u ⟶ v), P ((of V).map p)) :
P = ⊤
source
def CategoryTheory.Paths.liftNatTrans {C : Type u_1} [Category.{u_2, u_1} C] {V : Type u₁} [Quiver V] {F G : Functor (Paths V) C} (α_app : (v : V) → F.obj v ⟶ G.obj v) (α_nat : ∀ {X Y : V} (f : X ⟶ Y), CategoryStruct.comp (F.map f.toPath) (α_app Y) = CategoryStruct.comp (α_app X) (G.map f.toPath)) :
F ⟶ G

A natural transformation between F G : Paths V ⥤ C is defined by its components and its unary naturality squares.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Paths.liftNatTrans_app {C : Type u_1} [Category.{u_2, u_1} C] {V : Type u₁} [Quiver V] {F G : Functor (Paths V) C} (α_app : (v : V) → F.obj v ⟶ G.obj v) (α_nat : ∀ {X Y : V} (f : X ⟶ Y), CategoryStruct.comp (F.map f.toPath) (α_app Y) = CategoryStruct.comp (α_app X) (G.map f.toPath)) (v : V) :
    (liftNatTrans α_app α_nat).app v = α_app v
    source
    def CategoryTheory.Paths.liftNatIso {V : Type u₁} [Quiver V] {C : Type u_2} [Category.{u_3, u_2} C] {F G : Functor (Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v) (α_nat : ∀ {X Y : V} (f : X ⟶ Y), CategoryStruct.comp (F.map f.toPath) (α_app Y).hom = CategoryStruct.comp (α_app X).hom (G.map f.toPath)) :
    F ≅ G

    A natural isomorphism between F G : Paths V ⥤ C is defined by its components and its unary naturality squares.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Paths.liftNatIso_inv_app {V : Type u₁} [Quiver V] {C : Type u_2} [Category.{u_3, u_2} C] {F G : Functor (Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v) (α_nat : ∀ {X Y : V} (f : X ⟶ Y), CategoryStruct.comp (F.map f.toPath) (α_app Y).hom = CategoryStruct.comp (α_app X).hom (G.map f.toPath)) (X : Paths V) :
      (liftNatIso α_app α_nat).inv.app X = (α_app X).inv
      source
      @[simp]
      theorem CategoryTheory.Paths.liftNatIso_hom_app {V : Type u₁} [Quiver V] {C : Type u_2} [Category.{u_3, u_2} C] {F G : Functor (Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v) (α_nat : ∀ {X Y : V} (f : X ⟶ Y), CategoryStruct.comp (F.map f.toPath) (α_app Y).hom = CategoryStruct.comp (α_app X).hom (G.map f.toPath)) (X : Paths V) :
      (liftNatIso α_app α_nat).hom.app X = (α_app X).hom