Theorems · Definition · category theory

HomotopicalAlgebra.leftHomotopyClassToHom

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {H : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} H] →
          (L : CategoryTheory.Functor C H) →
            [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              {X Y : C} → HomotopicalAlgebra.LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)

The map LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y) when L is a localization functor with respect to weakEquivalences C.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.ModelCategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalization