Structures · Category theory
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure
A localizer morphism Φ : LocalizerMorphism W₁ W₂ is a left derivability
structure if it has left resolutions and the 2-square where the top and bottom functors
are localization functors for W₁ and W₂ is Guitart exact.
- Shape
- One type argument · adds hasLeftResolutions, guitartExact'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- HomotopicalAlgebra.CofibrantObject
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_equivalences
- CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure
- CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.hasLeftResolutions
- CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureOppositeOpOpOfIsLeftDerivabilityStructure
- CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure'
- CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact'
Ancestors0
No ancestors.