Commit 2026-01-31 23:36 c3cf7cbc

View on Github →

feat(CategoryTheory/Elements): initially small if functor is (co)representable (#34117) We show that Functor.Elements F has an initial element if F is (co)representable and that categories with initial element are initially small.

Estimated changes

Modified Mathlib/CategoryTheory/Elements.lean

added def CategoryTheory.Functor.Elements.initialOfCorepresentableBy

added def CategoryTheory.Functor.Elements.initialOfRepresentableBy

modified def CategoryTheory.Functor.Elements.isInitial

added def CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy

added def CategoryTheory.Functor.Elements.isInitialOfRepresentableBy

Modified Mathlib/CategoryTheory/Limits/Elements.lean

Modified Mathlib/CategoryTheory/Limits/FinallySmall.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.Functor.CorepresentableBy.coyoneda_homEquiv

added theorem CategoryTheory.Functor.RepresentableBy.coyoneda_homEquiv

added theorem CategoryTheory.Functor.RepresentableBy.homEquiv_unop_comp