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 Mathlib/CategoryTheory/PathCategory/Basic.lean in order to reduce transitive imports.

We also define a morpism property W.paths : MorphismProperty (Paths C) for any W : MorphismProperty C, consisting of all paths in C that consist only of morphisms in W.

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.{v_1, 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.{v_1, 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.{v_2, 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_hom_app {V : Type u₁} [Quiver V] {C : Type u_2} [Category.{v_2, 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
      source
      @[simp]
      theorem CategoryTheory.Paths.liftNatIso_inv_app {V : Type u₁} [Quiver V] {C : Type u_2} [Category.{v_2, 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
      def CategoryTheory.MorphismProperty.paths {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :
      MorphismProperty (Paths C)

      For any morphism property W on C, W.paths is the morphism property on Paths C containing all paths of morphisms in W.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.nil_mem_paths {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X : C} :
        W.paths Quiver.Path.nil
        source
        theorem CategoryTheory.MorphismProperty.cons_mem_paths {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {f : Y ⟶ Z} (hp : W.paths p) (hf : W f) :
        W.paths (p.cons f)
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.cons_mem_paths_iff {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {f : Y ⟶ Z} :
        W.paths (p.cons f) ↔ W.paths p ∧ W f
        source
        theorem CategoryTheory.MorphismProperty.toPath_mem_paths {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y : C} {f : X ⟶ Y} (hf : W f) :
        W.paths f.toPath
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.toPath_mem_paths_iff {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y : C} {f : X ⟶ Y} :
        W.paths f.toPath ↔ W f
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.comp_mem_paths_iff {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {q : Quiver.Path Y Z} :
        W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.comp_mem_paths_iff' {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y Z : Paths C} {p : X ⟶ Y} {q : Y ⟶ Z} :
        W.paths (CategoryStruct.comp p q) ↔ W.paths p ∧ W.paths q
        source
        instance CategoryTheory.MorphismProperty.instIsMultiplicativePathsPaths {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :
        W.paths.IsMultiplicative
        source
        theorem CategoryTheory.MorphismProperty.monotone_paths {C : Type u_1} [Category.{v_1, u_1} C] :
        Monotone paths

        If W and W' are morphism properties on C such that W ≤ W', then W.paths ≤ W'.paths.

        source
        theorem CategoryTheory.MorphismProperty.composePath_mem_of_id_mem {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) (h : W (CategoryStruct.id X)) :
        W (composePath p)
        source
        theorem CategoryTheory.MorphismProperty.composePath_mem_of_length_pos {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) (h : 0 < p.length) :
        W (composePath p)
        source
        theorem CategoryTheory.MorphismProperty.composePath_mem {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [W.IsMultiplicative] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) :
        W (composePath p)
        source
        theorem CategoryTheory.MorphismProperty.paths_le_inverseImage {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [W.IsMultiplicative] :
        W.paths ≤ W.inverseImage (pathComposition C)
        source
        instance CategoryTheory.MorphismProperty.instIsMultiplicativeStrictMapPathsPathsPathComposition {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :
        (W.paths.strictMap (pathComposition C)).IsMultiplicative
        source
        theorem CategoryTheory.MorphismProperty.multiplicativeClosure_eq_strictMap_paths {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :
        W.multiplicativeClosure = W.paths.strictMap (pathComposition C)