Commit 2025-05-18 11:22 4731dfb9

View on Github →

refactor(CategoryTheory/Core): make Core and its Hom one-field structures (#24987) This PR refactors the groupoid core of a category to prevents abuses on its Hom field.

Estimated changes

Modified Mathlib/CategoryTheory/Core.lean

deleted theorem CategoryTheory.Core.comp_hom

modified theorem CategoryTheory.Core.hom_ext

deleted theorem CategoryTheory.Core.id_hom

added structure CategoryTheory.Core

deleted def CategoryTheory.Core

added structure CategoryTheory.CoreHom

added theorem CategoryTheory.coreCategory_comp_iso