Structures · Category theory
CategoryTheory.Localization.HasSmallLocalizedHom
This property holds if the type of morphisms between X and Y
in the localized category with respect to W : MorphismProperty C
is small.
- Shape
- 3 explicit arguments · adds small
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- CategoryTheory.Localization.SmallHom.equiv
- CategoryTheory.Localization.SmallHom
- CategoryTheory.Localization.SmallHom.comp
- CategoryTheory.Localization.SmallHom.equiv_comp
- CategoryTheory.Localization.SmallHom.equiv_mk
- CategoryTheory.Localization.SmallHom.mkInv
- CategoryTheory.LocalizerMorphism.smallHomMap
- CategoryTheory.LocalizerMorphism.equiv_smallHomMap
- CategoryTheory.Localization.SmallHom.equiv_mkInv
- CategoryTheory.Localization.SmallHom.shift
- CategoryTheory.LocalizerMorphism.smallHomMap'
- CategoryTheory.Localization.SmallHom.equiv_equiv_symm
- CategoryTheory.Localization.hasSmallLocalizedHom_of_isos
- CategoryTheory.Localization.SmallHom.mk_comp_mk
- CategoryTheory.Localization.SmallHom.mk_id_comp
- CategoryTheory.Localization.small_of_hasSmallLocalizedHom
- CategoryTheory.LocalizerMorphism.smallHomMap_mk
- CategoryTheory.Localization.SmallHom.equiv_shift
- CategoryTheory.LocalizerMorphism.equiv_smallHomMap'
- CategoryTheory.LocalizerMorphism.smallHomMap_comp
- CategoryTheory.Localization.SmallHom.chgUniv
- CategoryTheory.Localization.SmallHom.comp_assoc
- CategoryTheory.Localization.SmallHom.equiv_chgUniv
- CategoryTheory.Localization.SmallHom.equiv.congr_simp
- CategoryTheory.Localization.SmallHom.comp_mk_id
- CategoryTheory.Localization.SmallHom.mkInv_comp_mk
- CategoryTheory.LocalizerMorphism.smallHomMap'_mk
- CategoryTheory.Localization.SmallHom.shift.congr_simp
- CategoryTheory.LocalizerMorphism.smallHomMap'_comp
- CategoryTheory.Localization.HasSmallLocalizedHom.small
- CategoryTheory.Localization.SmallHom.mkInv.congr_simp
- CategoryTheory.Localization.SmallHom.mk_comp_mkInv
Ancestors0
No ancestors.