Commit 2024-07-17 18:39 5388b1c6

View on Github →

deduplicate pullback and baseChange (#14519) Deduplication of Over.pullback and Over.baseChange. Over.baseChange has been renamed to Over.pullback and simp lemmas added to Over.pullback and Over.mapPullbackAdj.

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

Modified Mathlib/CategoryTheory/Adjunction/Over.lean

deleted def CategoryTheory.Over.baseChange

deleted def CategoryTheory.Over.mapAdjunction

added def CategoryTheory.Over.mapPullbackAdj

added def CategoryTheory.Over.pullback

added def CategoryTheory.Over.pullbackComp

added def CategoryTheory.Over.pullbackId

added def CategoryTheory.Under.mapPushoutAdj

added def CategoryTheory.Under.pullbackComp

added def CategoryTheory.Under.pushout

added def CategoryTheory.Under.pushoutId

Modified Mathlib/CategoryTheory/Limits/Over.lean

deleted def CategoryTheory.Over.mapPullbackAdj

deleted def CategoryTheory.Over.pullback

deleted def CategoryTheory.Over.pullbackComp

deleted def CategoryTheory.Over.pullbackId

deleted def CategoryTheory.Under.pushout

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Preadditive/Projective.lean

Modified Mathlib/CategoryTheory/Subobject/Comma.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean