Commit 2024-11-27 11:40 cb86c750

View on Github →

feat(CategoryTheory): pushforward pullback adjunction for P.Over Q X (#19271)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added theorem CategoryTheory.MorphismProperty.Comma.comp_left

added theorem CategoryTheory.MorphismProperty.Comma.comp_right

added theorem CategoryTheory.MorphismProperty.Comma.eqToHom_left

added theorem CategoryTheory.MorphismProperty.Comma.eqToHom_right

added def CategoryTheory.MorphismProperty.Comma.lift

added def CategoryTheory.MorphismProperty.Comma.mapLeft

added def CategoryTheory.MorphismProperty.Comma.mapRight

added theorem CategoryTheory.MorphismProperty.Over.Hom.ext

added theorem CategoryTheory.MorphismProperty.Over.w

added theorem CategoryTheory.MorphismProperty.Under.Hom.ext

added theorem CategoryTheory.MorphismProperty.Under.w

Created Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

added def CategoryTheory.MorphismProperty.Over.map

added def CategoryTheory.MorphismProperty.Over.mapComp

added theorem CategoryTheory.MorphismProperty.Over.map_comp

added theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst

added theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst