Commit 2025-03-13 09:34 6bc8904b

View on Github →

feat(CategoryTheory/WithTerminal): functors out of WithTerminal (#22658) Define an equivalence between the functor category WithTerminal C ⥤ D and the comma category Comma (𝟭 (C ⥤ D)) (const C). Dually, we define an equivalence between the functor category WithInitial C ⥤ D and Comma (const C) (𝟭 (C ⥤ D)).

Estimated changes

Modified Mathlib/CategoryTheory/WithTerminal.lean

added def CategoryTheory.WithInitial.equivComma

added def CategoryTheory.WithInitial.mkCommaMorphism

added def CategoryTheory.WithInitial.mkCommaObject

added def CategoryTheory.WithInitial.ofCommaMorphism

added def CategoryTheory.WithInitial.ofCommaObject

added def CategoryTheory.WithTerminal.equivComma

added def CategoryTheory.WithTerminal.mkCommaMorphism

added def CategoryTheory.WithTerminal.mkCommaObject

added def CategoryTheory.WithTerminal.ofCommaMorphism

added def CategoryTheory.WithTerminal.ofCommaObject