StrongGenerator

📁 Source: Mathlib/CategoryTheory/Presentable/StrongGenerator.lean

Statistics

Metric	Count
Definitions	0
Theorems of_isDense, of_isDense_ι, iff_exists_isStrongGenerator, of_le, colimitsCardinalClosure_eq_isCardinalPresentable, isDense_colimitsCardinalClosure_ι, colimitsCardinalClosure_le_isCardinalPresentable, isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, isFiltered_costructuredArrow_colimitsCardinalClosure_ι	9
Total	9

CategoryTheory.IsCardinalFilteredGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isDense 📖	mathematical	CategoryTheory.IsCardinalPresentable CategoryTheory.Functor.obj CategoryTheory.IsCardinalFiltered CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator CategoryTheory.ObjectProperty.map Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	CategoryTheory.isCardinalPresentable_of_iso CategoryTheory.CostructuredArrow.essentiallySmall CategoryTheory.IsCardinalFiltered.of_equivalence
of_isDense_ι 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.isCardinalPresentable CategoryTheory.IsCardinalFiltered CategoryTheory.CostructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.instCategoryCostructuredArrow	CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator	—	CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.congr_simp CategoryTheory.ObjectProperty.ι_map_top of_isDense CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1

CategoryTheory.IsCardinalLocallyPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_isStrongGenerator 📖	mathematical	—	CategoryTheory.IsCardinalLocallyPresentable CategoryTheory.ObjectProperty.IsStrongGenerator CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.isCardinalPresentable	—	CategoryTheory.HasCardinalFilteredGenerator.exists_small_generator CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isStrongGenerator CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall CategoryTheory.ObjectProperty.instEssentiallySmallOfSmall CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι
of_le 📖	mathematical	Cardinal Cardinal.instLE	CategoryTheory.IsCardinalLocallyPresentable	—	iff_exists_isStrongGenerator toHasColimitsOfSize CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable LE.le.trans CategoryTheory.isCardinalPresentable_monotone

CategoryTheory.IsStrongGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsCardinalClosure_eq_isCardinalPresentable 📖	mathematical	CategoryTheory.ObjectProperty.IsStrongGenerator CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.isCardinalPresentable	CategoryTheory.ObjectProperty.colimitsCardinalClosure	—	le_antisymm CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι CategoryTheory.ObjectProperty.retractClosure_eq_self CategoryTheory.ObjectProperty.isStableUnderRetracts_colimitsCardinalClosure CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit CategoryTheory.isCardinalPresentable_iff CategoryTheory.CostructuredArrow.essentiallySmall CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall CategoryTheory.ObjectProperty.instEssentiallySmallOfSmall CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsCardinalClosure_le_isCardinalPresentable 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.isCardinalPresentable	colimitsCardinalClosure	—	colimitsCardinalClosure_le CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable CategoryTheory.isClosedUnderColimitsOfShape_isCardinalPresentable CategoryTheory.Limits.Types.hasLimitsOfShape Opposite.small UnivLE.small UnivLE.self
isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι 📖	mathematical	—	CategoryTheory.IsCardinalFiltered CategoryTheory.CostructuredArrow FullSubcategory colimitsCardinalClosure FullSubcategory.category ι CategoryTheory.instCategoryCostructuredArrow	—	isClosedUnderColimitsOfShape_colimitsCardinalClosure CategoryTheory.CostructuredArrow.hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.preservesColimit_comp_of_createsColimit CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
isFiltered_costructuredArrow_colimitsCardinalClosure_ι 📖	mathematical	—	CategoryTheory.IsFiltered CategoryTheory.CostructuredArrow FullSubcategory colimitsCardinalClosure FullSubcategory.category ι CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.isFiltered_of_isCardinalFiltered isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι

CategoryTheory.ObjectProperty.IsStrongGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDense_colimitsCardinalClosure_ι 📖	mathematical	CategoryTheory.ObjectProperty.IsStrongGenerator CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.isCardinalPresentable	CategoryTheory.Functor.IsDense CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.colimitsCardinalClosure CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.CostructuredArrow.essentiallySmall CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall CategoryTheory.ObjectProperty.instEssentiallySmallOfSmall CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.ObjectProperty.IsSeparating.mono_iff isSeparating CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.w CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure HasCardinalLT.of_le CategoryTheory.Arrow.finite Cardinal.IsRegular.aleph0_le Fact.out CategoryTheory.Limits.hasCoequalizers_of_hasWideCoequalizers CategoryTheory.ObjectProperty.prop_colimit CategoryTheory.ObjectProperty.le_colimitsCardinalClosure CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.Limits.coequalizer.desc.congr_simp CategoryTheory.Limits.coequalizer.condition_assoc isIso_of_mono

---

← Back to Index