Theorems · Theorem · category theory

HomotopicalAlgebra.BifibrantObject.inverts_iff_factors

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) D),
  (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C)).IsInvertedBy F ↔
    ∀ ⦃K L : HomotopicalAlgebra.BifibrantObject C⦄ (f g : K ⟶ L),
      HomotopicalAlgebra.BifibrantObject.homRel C f g → F.map f = F.map g

Defined in

Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.ModelCategoryCategoryTheory.Category