Commit 2023-04-03 00:49 96323779

View on Github →

feat: port CategoryTheory.Shift.Basic (#3039)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monoidal/Discrete.lean

Created Mathlib/CategoryTheory/Shift/Basic.lean

added theorem CategoryTheory.HasShift.shift_obj_obj

added theorem CategoryTheory.ShiftMkCore.add_zero_inv_app

added theorem CategoryTheory.ShiftMkCore.assoc_inv_app

added theorem CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq

added theorem CategoryTheory.ShiftMkCore.shiftFunctorZero_eq

added theorem CategoryTheory.ShiftMkCore.shiftFunctor_eq

added theorem CategoryTheory.ShiftMkCore.zero_add_inv_app

added structure CategoryTheory.ShiftMkCore

added def CategoryTheory.hasShiftMk

added def CategoryTheory.hasShiftOfFullyFaithful

added def CategoryTheory.hasShiftOfFullyFaithful_add

added def CategoryTheory.hasShiftOfFullyFaithful_zero

added theorem CategoryTheory.map_hasShiftOfFullyFaithful_add_hom_app

added theorem CategoryTheory.map_hasShiftOfFullyFaithful_add_inv_app

added theorem CategoryTheory.map_hasShiftOfFullyFaithful_zero_hom_app

added theorem CategoryTheory.map_hasShiftOfFullyFaithful_zero_inv_app

added theorem CategoryTheory.shiftComm_hom_comp

added theorem CategoryTheory.shiftComm_symm

added def CategoryTheory.shiftEquiv'

added def CategoryTheory.shiftFunctor

added def CategoryTheory.shiftFunctorAdd'

added theorem CategoryTheory.shiftFunctorAdd'_add_zero

added theorem CategoryTheory.shiftFunctorAdd'_add_zero_hom_app

added theorem CategoryTheory.shiftFunctorAdd'_add_zero_inv_app

added theorem CategoryTheory.shiftFunctorAdd'_assoc

added theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app

added theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app

added theorem CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd

added theorem CategoryTheory.shiftFunctorAdd'_zero_add

added theorem CategoryTheory.shiftFunctorAdd'_zero_add_hom_app

added theorem CategoryTheory.shiftFunctorAdd'_zero_add_inv_app

added def CategoryTheory.shiftFunctorAdd

added theorem CategoryTheory.shiftFunctorAdd_add_zero_hom_app

added theorem CategoryTheory.shiftFunctorAdd_add_zero_inv_app

added theorem CategoryTheory.shiftFunctorAdd_assoc

added theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app

added theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app

added theorem CategoryTheory.shiftFunctorAdd_zero_add_hom_app

added theorem CategoryTheory.shiftFunctorAdd_zero_add_inv_app

added def CategoryTheory.shiftFunctorComm

added theorem CategoryTheory.shiftFunctorComm_eq

added theorem CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app

added theorem CategoryTheory.shiftFunctorComm_symm

added def CategoryTheory.shiftFunctorCompIsoId

added def CategoryTheory.shiftFunctorZero

added theorem CategoryTheory.shiftFunctorZero_hom_app_shift

added theorem CategoryTheory.shiftFunctorZero_inv_app_shift

added theorem CategoryTheory.shiftFunctor_inv

added def CategoryTheory.shiftMonoidalFunctor

added theorem CategoryTheory.shift_comm'

added theorem CategoryTheory.shift_equiv_triangle

added theorem CategoryTheory.shift_neg_shift'

added theorem CategoryTheory.shift_shift'

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_self_hom_app

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_self_inv_app

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_hom_app

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_inv_app

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_self_hom_app

added theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_self_inv_app

added theorem CategoryTheory.shift_shift_neg'

added theorem CategoryTheory.shift_zero'

added theorem CategoryTheory.shift_zero_eq_zero