Theorems · Theorem · category theory

CategoryTheory.Localization.Construction.liftToPathCategory_map

∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G)
  {X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)} (f : X ⟶ Y),
  (CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f =
    CategoryTheory.composePath
      ({ obj := fun X => G.obj X.obj,
            map := fun {X Y} a =>
              Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }.mapPath
        f)

Defined in

Mathlib.CategoryTheory.Localization.Construction

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Category