Structures · Category theory
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence
Condition that a LocalizerMorphism induces an equivalence on the localized categories
- Shape
- One type argument · adds isEquivalence
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- CochainComplex.Plus
- HomotopicalAlgebra.CofibrantObject
- HomotopicalAlgebra.BifibrantObject
- HomotopicalAlgebra.FibrantObject
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence
- CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.comp
- CategoryTheory.LocalizerMorphism.instIsLocalizedFullyFaithfulOfIsLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.instIsLocalizedEquivalenceOppositeOpOp
- CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_isLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence
- CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_isLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization
- CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk'
- CategoryTheory.LocalizerMorphism.isEquivalence
Ancestors0
No ancestors.