Commit 2025-10-12 14:20 1a7fef66

View on Github →

feat(CategoryTheory): pseudofunctors to Cat (#25971) This PR adds convenience lemmas for pseudofunctors to Cat, mostly using the to_app attribute. The simp set for the to_app attribute is extended in order to take into account that in Cat, associators and unitors induce identities.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

added theorem CategoryTheory.Pseudofunctor.mapComp'_hom_naturality

added theorem CategoryTheory.Pseudofunctor.mapComp'_inv_naturality

added theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_1

added theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_2

added theorem CategoryTheory.Pseudofunctor.mapId'_hom_naturality

added theorem CategoryTheory.Pseudofunctor.mapId'_inv_naturality

Modified Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

added theorem CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv

deleted theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight

deleted theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv

deleted theorem CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom

deleted theorem CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv

added theorem CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight

added theorem CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv

deleted theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv

added theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv

Modified Mathlib/Tactic/CategoryTheory/ToApp.lean

Modified MathlibTest/CategoryTheory/ToApp.lean