Commit 2025-05-11 19:52 a8b54a8a

View on Github →

feat(CategoryTheory): left derived functors (#24142) The definitions in the file CategoryTheory.Functor.Derived.RightDerived are dualized in order to define left derived functors.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/Derived/LeftDerived.lean

added theorem CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension

added theorem CategoryTheory.Functor.HasLeftDerivedFunctor.mk'

added theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff

added theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff_of_iso

added theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift

added theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isRightKanExtension

added theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_iso

added theorem CategoryTheory.Functor.leftDerivedNatTrans_app

added theorem CategoryTheory.Functor.leftDerivedNatTrans_comp

added theorem CategoryTheory.Functor.leftDerivedNatTrans_fac

added theorem CategoryTheory.Functor.leftDerivedNatTrans_id

added theorem CategoryTheory.Functor.leftDerived_ext

added theorem CategoryTheory.Functor.leftDerived_fac

added theorem CategoryTheory.Functor.leftDerived_fac_app

Modified Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean

deleted theorem CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension