Dense

📁 Source: Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean

Statistics

Metric	Count
Definitions IsDense, denseAt	2
Theorems comp_left_iff_of_isEquivalence, comp_right_iff_of_isEquivalence, iff_of_iso, isDenseAt, of_fullyFaithful_restrictedULiftYoneda, of_iso, instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense, instFullOppositeTypeRestrictedULiftYonedaOfIsDense, instIsDenseCompOfIsEquivalence, instIsDenseCompOfIsEquivalence_1, isDense_iff_fullyFaithful_restrictedULiftYoneda, isDense_iff_nonempty_isPointwiseLeftKanExtension, isStrongGenerator_of_isDense	13
Total	15

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsDense 📖	CompData	12 math math: IsDense.comp_left_iff_of_isEquivalence, isDense_iff_nonempty_isPointwiseLeftKanExtension, instIsDenseCompOfIsEquivalence_1, IsDense.iff_of_iso, isDense_iff_fullyFaithful_restrictedULiftYoneda, IsDense.of_iso, CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι, CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι, instIsDenseCompOfIsEquivalence, CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι, IsDense.of_fullyFaithful_restrictedULiftYoneda, IsDense.comp_right_iff_of_isEquivalence
denseAt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense 📖	mathematical	—	Faithful CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types category CategoryTheory.Presheaf.restrictedULiftYoneda	—	LeftExtension.IsPointwiseLeftKanExtensionAt.hom_ext' CategoryTheory.Category.id_comp ULift.up_injective CategoryTheory.NatTrans.congr_app
instFullOppositeTypeRestrictedULiftYonedaOfIsDense 📖	mathematical	—	Full CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types category CategoryTheory.Presheaf.restrictedULiftYoneda	—	CategoryTheory.Category.comp_id CategoryTheory.CommaMorphism.w CategoryTheory.NatTrans.naturality CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.Limits.IsColimit.fac CategoryTheory.Category.id_comp ULift.down_injective
instIsDenseCompOfIsEquivalence 📖	mathematical	—	IsDense comp	—	final_of_isRightAdjoint isRightAdjoint_of_isEquivalence CategoryTheory.CostructuredArrow.isEquivalence_pre
instIsDenseCompOfIsEquivalence_1 📖	mathematical	—	IsDense comp	—	—
isDense_iff_fullyFaithful_restrictedULiftYoneda 📖	mathematical	—	IsDense FullyFaithful CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types category CategoryTheory.Presheaf.restrictedULiftYoneda	—	instFullOppositeTypeRestrictedULiftYonedaOfIsDense instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense IsDense.of_fullyFaithful_restrictedULiftYoneda
isDense_iff_nonempty_isPointwiseLeftKanExtension 📖	mathematical	—	IsDense LeftExtension.IsPointwiseLeftKanExtension id CategoryTheory.Iso.inv CategoryTheory.Functor category comp rightUnitor	—	—
isStrongGenerator_of_isDense 📖	mathematical	—	CategoryTheory.ObjectProperty.IsStrongGenerator CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct obj	—	CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_colimitsOfShape CategoryTheory.CostructuredArrow.instSmallOfLocallySmall UnivLE.small univLE_of_max UnivLE.self CategoryTheory.locallySmall_of_univLE CategoryTheory.Shrink.instLocallySmallShrink CategoryTheory.locallySmall_of_essentiallySmall CategoryTheory.CostructuredArrow.essentiallySmall CategoryTheory.essentiallySmall_of_small_of_locallySmall

CategoryTheory.Functor.IsDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left_iff_of_isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsDense CategoryTheory.Functor.comp	—	of_iso CategoryTheory.Functor.instIsDenseCompOfIsEquivalence CategoryTheory.Functor.isEquivalence_inv
comp_right_iff_of_isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsDense CategoryTheory.Functor.comp	—	of_iso CategoryTheory.Functor.instIsDenseCompOfIsEquivalence_1 CategoryTheory.Functor.isEquivalence_inv
iff_of_iso 📖	mathematical	—	CategoryTheory.Functor.IsDense	—	of_iso
isDenseAt 📖	mathematical	—	CategoryTheory.Functor.isDenseAt	—	—
of_fullyFaithful_restrictedULiftYoneda 📖	mathematical	—	CategoryTheory.Functor.IsDense	—	CategoryTheory.types_ext CategoryTheory.Limits.Cocone.w CategoryTheory.NatTrans.ext' CategoryTheory.Functor.map_preimage CategoryTheory.Functor.FullyFaithful.map_injective CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Functor.FullyFaithful.map_preimage
of_iso 📖	mathematical	—	CategoryTheory.Functor.IsDense	—	CategoryTheory.Functor.congr_isDenseAt

---

← Back to Index