Commit 2023-09-05 08:30 5dac7e8d

View on Github →

feat: the shift on a quotient category (#6653) This PR constructs 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