Commit 2023-09-21 16:56 80106b75

View on Github →

feat(CategoryTheory): the pullback of a shift by a monoid morphism (#7270)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monoidal/Discrete.lean

Created Mathlib/CategoryTheory/Shift/Pullback.lean

added def CategoryTheory.PullbackShift

added theorem CategoryTheory.pullbackShiftFunctorAdd'_hom_app

added theorem CategoryTheory.pullbackShiftFunctorAdd'_inv_app

added theorem CategoryTheory.pullbackShiftFunctorZero_hom_app

added theorem CategoryTheory.pullbackShiftFunctorZero_inv_app