Commit 2025-02-15 12:38 ab7cf6ec

View on Github →

feat(CategoryTheory): Grothendieck.map preserves finality (#19073)

Estimated changes

Modified Mathlib/CategoryTheory/EqToHom.lean

added theorem CategoryTheory.eqToHom_heq_id_cod

added theorem CategoryTheory.eqToHom_heq_id_dom

Modified Mathlib/CategoryTheory/Grothendieck.lean

added def CategoryTheory.Grothendieck.ιCompMap

Modified Mathlib/CategoryTheory/Limits/Final.lean

added def CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence

added theorem CategoryTheory.Grothendieck.final_map