Commit 2025-05-18 14:11 458a6079

View on Github →

feat(CategoryTheory/Equivalences): category structure on equivalences (#23197) We put a category structure on (C ≌ D). The morphisms are simply natural transformations between the underlying functor. We also provide various API for this structure.

Estimated changes

Modified Mathlib/CategoryTheory/Equivalence.lean

added def CategoryTheory.Equivalence.asNatTrans

added theorem CategoryTheory.Equivalence.asNatTrans_mkHom

added theorem CategoryTheory.Equivalence.comp_asNatTrans

added def CategoryTheory.Equivalence.congrRightFunctor

added def CategoryTheory.Equivalence.functorFunctor

added theorem CategoryTheory.Equivalence.hom_ext

added theorem CategoryTheory.Equivalence.id_asNatTrans

added def CategoryTheory.Equivalence.mkHom

added theorem CategoryTheory.Equivalence.mkHom_asNatTrans

added theorem CategoryTheory.Equivalence.mkHom_comp

added theorem CategoryTheory.Equivalence.mkHom_id_functor

added theorem CategoryTheory.Equivalence.mkHom_id_inverse

added def CategoryTheory.Equivalence.mkIso