Commit 2025-11-04 23:41 99382bdb

View on Github →

feat(CategoryTheory): naturality lemmas for Core construction (#29284) Lemmas for PR #29283 to prove that Core is the right adjoint to the forgetful functor from Cat to Grpd. These lemmas are more general than that setting, and need not be stated in the bundled format.

depends on: #29250

Estimated changes

Modified Mathlib/CategoryTheory/Core.lean

added def CategoryTheory.Core.functorToCoreCompLeftIso

added def CategoryTheory.Core.functorToCoreCompRightIso

added def CategoryTheory.Core.functorToCoreInclusionIso

added theorem CategoryTheory.Core.functorToCore_comp_left

added theorem CategoryTheory.Core.functorToCore_comp_right

added theorem CategoryTheory.Core.functorToCore_inclusion

added def CategoryTheory.Core.inclusionCompFunctorToCoreIso

added theorem CategoryTheory.Core.inclusion_comp_functorToCore

added def CategoryTheory.Functor.coreCompInclusionIso

added theorem CategoryTheory.Functor.core_comp_inclusion