Commit 2023-08-18 09:29 3febb8c2

View on Github →

feat: the shift on a quotient category

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Quotient.lean

added theorem CategoryTheory.Quotient.comp_natTransLift

added def CategoryTheory.Quotient.natIsoLift

added def CategoryTheory.Quotient.natTransLift

added theorem CategoryTheory.Quotient.natTransLift_app

added theorem CategoryTheory.Quotient.natTransLift_id

added theorem CategoryTheory.Quotient.natTrans_ext

Created Mathlib/CategoryTheory/Shift/Quotient.lean

added theorem CategoryTheory.HasShift.quotient'_aux

added def CategoryTheory.Quotient.shiftFunctor'

added def CategoryTheory.Quotient.shiftFunctor'Factors