Commit 2023-09-08 11:01 a384f1b2

View on Github →

feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/CofilteredSystem.lean

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

added theorem CategoryTheory.essentiallySmall_of_small_of_locallySmall

added theorem CategoryTheory.locallySmall_max

Renamed Mathlib/CategoryTheory/Filtered.lean to Mathlib/CategoryTheory/Filtered/Basic.lean

Created Mathlib/CategoryTheory/Filtered/Small.lean

added inductive CategoryTheory.IsCofiltered.CofilteredClosure

added def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate

added theorem CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure

added inductive CategoryTheory.IsFiltered.FilteredClosure

added def CategoryTheory.IsFiltered.SmallFilteredIntermediate

added theorem CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure

Modified Mathlib/CategoryTheory/Limits/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/Types.lean

Modified Mathlib/Logic/Small/Basic.lean

added theorem small_of_injective_of_exists

Modified docs/references.bib