Commit 2025-11-19 16:51 631f0c1f

View on Github →

feat: dualize Pseudofunctor.CoGrothendieck results to Pseudofunctor.Grothendieck (#30071) Continuing from #29681, dualize all definitions and lemmas in the namespace Pseudofunctor.CoGrothendieck to results in the namespace Pseudofunctor.Grothendieck.

depends on: #29681

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff

added def CategoryTheory.Pseudofunctor.Grothendieck.forget

added def CategoryTheory.Pseudofunctor.Grothendieck.map

added def CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso

added def CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_comp_eq

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_comp_forget

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_id_eq

added theorem CategoryTheory.Pseudofunctor.Grothendieck.map_id_map