Commit 2025-06-22 08:32 69f66e45

View on Github →

feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories (#25744) Promote the constructions C ↦ C ⋆ D and D ↦ C ⋆ D to pseudofunctors from Cat to Cat. The construction is carried in a new file CategoryTheory/Join/Pseudofunctor.lean to reduce imports.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Join/Basic.lean

added theorem CategoryTheory.Join.mapWhiskerLeft_id

added theorem CategoryTheory.Join.mapWhiskerRight_id

Created Mathlib/CategoryTheory/Join/Pseudofunctor.lean

added def CategoryTheory.Join.mapCompLeft

added def CategoryTheory.Join.mapCompRight

added theorem CategoryTheory.Join.mapWhiskerLeft_associator_hom

added theorem CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom

added theorem CategoryTheory.Join.mapWhiskerLeft_rightUnitor_hom

added theorem CategoryTheory.Join.mapWhiskerLeft_whiskerLeft

added theorem CategoryTheory.Join.mapWhiskerLeft_whiskerRight

added theorem CategoryTheory.Join.mapWhiskerRight_associator_hom

added theorem CategoryTheory.Join.mapWhiskerRight_leftUnitor_hom

added theorem CategoryTheory.Join.mapWhiskerRight_rightUnitor_hom

added theorem CategoryTheory.Join.mapWhiskerRight_whiskerLeft

added theorem CategoryTheory.Join.mapWhiskerRight_whiskerRight

added def CategoryTheory.Join.pseudofunctorLeft

added def CategoryTheory.Join.pseudofunctorRight