Commit 2021-03-29 13:12 318cb4bc

View on Github →

feat(category_theory): essentially_small categories (#6801) Preparation for well_powered, then for complete_semilattice_Inf|Sup on subobject X, then for work on chain complexes.

Estimated changes

Modified src/category_theory/equivalence.lean

Created src/category_theory/essentially_small.lean

added def category_theory.equiv_small_model

added theorem category_theory.essentially_small.mk'

added theorem category_theory.essentially_small_congr

added theorem category_theory.essentially_small_iff

added theorem category_theory.essentially_small_iff_of_thin

added theorem category_theory.locally_small_congr

added def category_theory.shrink_homs.equivalence

added def category_theory.shrink_homs.from_shrink_homs

added theorem category_theory.shrink_homs.from_to

added def category_theory.shrink_homs.functor

added def category_theory.shrink_homs.inverse

added theorem category_theory.shrink_homs.to_from

added def category_theory.shrink_homs.to_shrink_homs

added def category_theory.shrink_homs

added def category_theory.small_model

Modified src/category_theory/skeletal.lean

added def category_theory.equivalence.skeleton_equiv

added theorem category_theory.skeleton_skeletal

Modified src/data/equiv/basic.lean

added def equiv.punit_of_nonempty_of_subsingleton

Modified src/data/fintype/basic.lean

Created src/logic/small.lean

added def equiv_shrink

added def shrink

added theorem small.mk'

added theorem small_congr

added theorem small_of_injective