Commit 2025-03-11 16:03 5509cf26

View on Github →

feat(CategoryTheory/Subobject): add some lemmas wrt. the IsPullback API (#22379) We introduce some lemmas in CategoryTheory/Subobject/Basic.lean about the interaction of subobjects with the CategoryTheory.IsPullback API. Will be used in PR #22245.

Estimated changes

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

added theorem CategoryTheory.Subobject.mk_surjective

added theorem CategoryTheory.Subobject.pullback_obj

added theorem CategoryTheory.Subobject.pullback_obj_mk

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

added def CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback