| Name | Category | Theorems |
|---|
IsLocalizedEquivalence 📖 | CompData | 11 mathmath: HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, IsLocalizedEquivalence.of_equivalence, HomRel.FactorsThroughLocalization.isLocalizedEquivalence, isLocalizedEquivalence_of_unit_of_unit, instIsLocalizedEquivalenceOppositeOpOp, isLocalizedEquivalence_of_functorial_right_resolutions, IsLocalizedEquivalence.of_isLocalization_of_isLocalization, IsLocalizedEquivalence.mk', HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
|
arrow 📖 | CompOp | 4 mathmath: hasRightResolutions_arrow_of_functorial_resolutions, arrow_functor, HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism
|
catCommSq 📖 | CompOp | 9 mathmath: rightDerivedFunctorComparison_fac_app_assoc, rightDerivedFunctorComparison_fac, rightDerivedFunctorComparison_fac_app, guitartExact_of_isRightDerivabilityStructure, IsRightDerivabilityStructure.guitartExact', guitartExact_of_isLeftDerivabilityStructure, instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor, rightDerivedFunctorComparison_fac_assoc, IsLeftDerivabilityStructure.guitartExact'
|
comp 📖 | CompOp | 2 mathmath: comp_functor, homMap_homMap
|
functor 📖 | CompOp | 72 mathmath: IsRightDerivabilityStructure.Constructor.fromRightResolution_map, id_functor, natTransCommShift_hom, homMap_map, rightDerivedFunctorComparison_fac_app_assoc, homMap_id, commShift_iso_hom_app, commShift_iso_inv_app, arrow_functor, Derives.isIso, smallHomMap_comp, LeftResolution.Hom.comm, smallShiftedHomMap_mk, hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure, functorialRightResolutions.Φ_functor_map_ι_app, HomotopicalAlgebra.FibrantObject.localizerMorphism_functor, smallHomMap_mk, HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, rightDerivedFunctorComparison_fac, comp_functor, LeftResolution.unop_w, homMap_apply, commShift_iso_hom_app_assoc, rightDerivedFunctorComparison_fac_app, commShift_iso_inv_app_assoc, equiv_smallHomMap', hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure, homMap_apply_assoc, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, smallHomMap'_mk, equiv_smallShiftedHomMap, guitartExact_of_isLeftDerivabilityStructure', homMap_comp, RightResolution.Hom.comm, ofEq_functor, homMap_comp_assoc, guitartExact_of_isRightDerivabilityStructure, isRightDerivabilityStructure_iff, LeftResolution.hw, op_functor, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences, IsRightDerivabilityStructure.Constructor.isConnected, essSurj_of_hasRightResolutions, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences, HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor, homMap_homMap, isIso_iff_of_hasRightResolutions, equiv_smallHomMap, IsRightDerivabilityStructure.guitartExact', map, RightResolution.hw, RightResolution.unop_w, LeftResolution.op_w, guitartExact_of_isLeftDerivabilityStructure, guitartExact_of_isRightDerivabilityStructure', inverts, Derives.isRightDerivedFunctor_iff_isIso, LeftResolution.Hom.comm_assoc, IsLocalizedEquivalence.isLocalization, HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor, RightResolution.op_w, rightDerivedFunctorComparison_fac_assoc, IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor, RightResolution.Hom.comm_assoc, isLeftDerivabilityStructure_iff, isIso_iff_of_hasLeftResolutions, smallShiftedHomMap_mk₀, IsLeftDerivabilityStructure.guitartExact', essSurj_of_hasLeftResolutions
|
id 📖 | CompOp | 7 mathmath: id_functor, instHasRightResolutionsIdOfContainsIdentities, instIsLeftDerivabilityStructureIdOfContainsIdentities, CategoryTheory.Localization.homEquiv_apply, id_homMap, instIsRightDerivabilityStructureIdOfContainsIdentities, instHasLeftResolutionsIdOfContainsIdentities
|
liftingLocalizedFunctor 📖 | CompOp | — |
localizedFunctor 📖 | CompOp | 12 mathmath: rightDerivedFunctorComparison_fac_app_assoc, localizedFunctor_isEquivalence, rightDerivedFunctorComparison_fac, rightDerivedFunctorComparison_fac_app, IsLocalizedEquivalence.isEquivalence, guitartExact_of_isRightDerivabilityStructure, IsRightDerivabilityStructure.guitartExact', guitartExact_of_isLeftDerivabilityStructure, instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor, rightDerivedFunctorComparison_fac_assoc, IsLeftDerivabilityStructure.guitartExact', instIsIsoFunctorRightDerivedFunctorComparison
|
ofEq 📖 | CompOp | 2 mathmath: HomRel.FactorsThroughLocalization.isLocalizedEquivalence, ofEq_functor
|
op 📖 | CompOp | 25 mathmath: LeftResolution.opFunctor_map_f, hasLeftResolutions_iff_op, RightResolution.op_X₁, LeftResolution.unop_X₁, RightResolution.unop_X₁, LeftResolution.opEquivalence_unitIso, instHasLeftResolutionsOppositeOpOpOfHasRightResolutions, nonempty_rightResolution_iff_op, LeftResolution.opEquivalence_inverse, LeftResolution.opFunctor_obj, LeftResolution.unop_w, instIsLocalizedEquivalenceOppositeOpOp, RightResolution.unopFunctor_obj, op_functor, nonempty_leftResolution_iff_op, RightResolution.unop_w, LeftResolution.op_w, RightResolution.unopFunctor_map_f, LeftResolution.op_X₁, LeftResolution.opEquivalence_counitIso, RightResolution.op_w, hasRightResolutions_iff_op, LeftResolution.opEquivalence_functor, instHasRightResolutionsOppositeOpOpOfHasLeftResolutions, isLeftDerivabilityStructure_iff_op
|