Commit 2026-03-27 11:45 d32fafc1

View on Github →

chore(CategoryTheory/MorphismProperty): dualise IsStableUnderBaseChangeAlong and related declarations (#36900) We also fix some naming inconsistencies.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

deleted theorem CategoryTheory.MorphismProperty.baseChange_map'

deleted theorem CategoryTheory.MorphismProperty.baseChange_map

deleted theorem CategoryTheory.MorphismProperty.of_isPullback

deleted theorem CategoryTheory.MorphismProperty.of_isPushout

added theorem CategoryTheory.MorphismProperty.overPullbackMap

added theorem CategoryTheory.MorphismProperty.pullbackLift_fst_snd

added theorem CategoryTheory.MorphismProperty.pullbackMap

deleted theorem CategoryTheory.MorphismProperty.pullback_map

added theorem CategoryTheory.MorphismProperty.pushoutDesc_inl_inr

added theorem CategoryTheory.MorphismProperty.pushoutMap

modified theorem CategoryTheory.MorphismProperty.pushout_inl

modified theorem CategoryTheory.MorphismProperty.pushout_inr

added theorem CategoryTheory.MorphismProperty.underPushoutMap

Modified Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean