Theorems · Definition · category theory

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {E : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          {X Y : C} →
            CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y →
              (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → (F.obj X ⟶ F.obj Y)

The image by a functor which inverts W of an equivalence class of left fractions.

Defined in

Mathlib.CategoryTheory.Localization.CalculusOfFractions

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category