Structures · Category theory
CategoryTheory.Functor.IsDense
A functor F : C ⥤ D is dense if any Y : D is a canonical colimit
relatively to F.
- Shape
- One type argument · adds isDenseAt
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.ObjectProperty.FullSubcategory
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- CategoryTheory.Functor.denseAt
- CategoryTheory.Functor.IsDense.leftKanExtensionIso
- CategoryTheory.Functor.IsDense.of_iso
- CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι
- CategoryTheory.Functor.IsDense.isDenseAt
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense
- CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app
- CategoryTheory.Functor.instHasPointwiseLeftKanExtensionOfIsDense
- CategoryTheory.Functor.instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense
- CategoryTheory.Functor.instFullOppositeTypeRestrictedULiftYonedaOfIsDense
- CategoryTheory.Functor.instIsDenseCompOfIsEquivalence
- CategoryTheory.Functor.instIsLeftKanExtensionIdInvRightUnitorOfIsDense
- CategoryTheory.Functor.denseAt.congr_simp
- CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_assoc
- CategoryTheory.Functor.isStrongGenerator_of_isDense
- CategoryTheory.Functor.instIsDenseCompOfIsEquivalence_1
- CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app_assoc
Ancestors0
No ancestors.