LeftDerived

📁 Source: Mathlib/CategoryTheory/Functor/Derived/LeftDerived.lean

Statistics

Metric	Count
Definitions HasLeftDerivedFunctor, IsLeftDerivedFunctor, leftDerivedLift, leftDerivedNatIso, leftDerivedNatTrans, leftDerivedUnique, totalLeftDerived, totalLeftDerivedCounit	8
Theorems hasRightKanExtension, hasRightKanExtension', mk', isRightKanExtension, hasLeftDerivedFunctor_iff, hasLeftDerivedFunctor_iff_of_iso, instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit, isLeftDerivedFunctor_iff_isIso_leftDerivedLift, isLeftDerivedFunctor_iff_isRightKanExtension, isLeftDerivedFunctor_iff_of_iso, leftDerivedNatIso_hom, leftDerivedNatIso_inv, leftDerivedNatTrans_app, leftDerivedNatTrans_app_assoc, leftDerivedNatTrans_comp, leftDerivedNatTrans_comp_assoc, leftDerivedNatTrans_fac, leftDerivedNatTrans_fac_assoc, leftDerivedNatTrans_id, leftDerived_ext, leftDerived_fac, leftDerived_fac_app, leftDerived_fac_app_assoc, leftDerived_fac_assoc	24
Total	32

CategoryTheory.Functor

Definitions

Name	Category	Theorems
HasLeftDerivedFunctor 📖	CompData	4 math math: hasLeftDerivedFunctor_iff, hasLeftDerivedFunctor_of_hasPointwiseLeftDerivedFunctor, hasLeftDerivedFunctor_iff_of_iso, HasLeftDerivedFunctor.mk'
IsLeftDerivedFunctor 📖	CompData	7 math math: isLeftDerivedFunctor_iff_isRightKanExtension, isLeftDerivedFunctor_iff_of_inverts, isLeftDerivedFunctor_of_inverts, instIsLeftDerivedFunctorLiftHomFac, isLeftDerivedFunctor_iff_of_iso, instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit, isLeftDerivedFunctor_iff_isIso_leftDerivedLift
leftDerivedLift 📖	CompOp	5 math math: leftDerived_fac_app, leftDerived_fac_assoc, leftDerived_fac, leftDerived_fac_app_assoc, isLeftDerivedFunctor_iff_isIso_leftDerivedLift
leftDerivedNatIso 📖	CompOp	2 math math: leftDerivedNatIso_inv, leftDerivedNatIso_hom
leftDerivedNatTrans 📖	CompOp	9 math math: leftDerivedNatTrans_fac_assoc, leftDerivedNatIso_inv, leftDerivedNatTrans_comp_assoc, leftDerivedNatTrans_comp, leftDerivedNatTrans_app_assoc, leftDerivedNatIso_hom, leftDerivedNatTrans_app, leftDerivedNatTrans_id, leftDerivedNatTrans_fac
leftDerivedUnique 📖	CompOp	—
totalLeftDerived 📖	CompOp	1 math math: instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit
totalLeftDerivedCounit 📖	CompOp	1 math math: instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLeftDerivedFunctor_iff 📖	mathematical	—	HasLeftDerivedFunctor HasRightKanExtension	—	HasLeftDerivedFunctor.hasRightKanExtension' hasRightExtension_iff_postcomp₁ q_isLocalization CategoryTheory.Equivalence.isEquivalence_functor
hasLeftDerivedFunctor_iff_of_iso 📖	mathematical	—	HasLeftDerivedFunctor	—	hasLeftDerivedFunctor_iff q_isLocalization hasRightExtension_iff_of_iso₂
instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit 📖	mathematical	—	IsLeftDerivedFunctor totalLeftDerived totalLeftDerivedCounit	—	HasLeftDerivedFunctor.hasRightKanExtension instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit
isLeftDerivedFunctor_iff_isIso_leftDerivedLift 📖	mathematical	—	IsLeftDerivedFunctor CategoryTheory.IsIso CategoryTheory.Functor category leftDerivedLift	—	isLeftDerivedFunctor_iff_isRightKanExtension IsLeftDerivedFunctor.isRightKanExtension isRightKanExtension_iff_isIso leftDerived_fac
isLeftDerivedFunctor_iff_isRightKanExtension 📖	mathematical	—	IsLeftDerivedFunctor IsRightKanExtension	—	IsLeftDerivedFunctor.isRightKanExtension
isLeftDerivedFunctor_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsLeftDerivedFunctor	—	isRightKanExtension_iff_of_iso
leftDerivedNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category leftDerivedNatIso leftDerivedNatTrans	—	—
leftDerivedNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category leftDerivedNatIso leftDerivedNatTrans	—	—
leftDerivedNatTrans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app leftDerivedNatTrans comp	—	leftDerived_fac_app
leftDerivedNatTrans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app leftDerivedNatTrans comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedNatTrans_app
leftDerivedNatTrans_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerivedNatTrans	—	leftDerived_ext CategoryTheory.Category.assoc leftDerivedNatTrans_fac leftDerivedNatTrans_fac_assoc
leftDerivedNatTrans_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerivedNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedNatTrans_comp
leftDerivedNatTrans_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft leftDerivedNatTrans	—	leftDerived_fac
leftDerivedNatTrans_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft leftDerivedNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedNatTrans_fac
leftDerivedNatTrans_id 📖	mathematical	—	leftDerivedNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category	—	leftDerived_ext leftDerivedNatTrans_fac CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
leftDerived_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	—	—	IsLeftDerivedFunctor.isRightKanExtension hom_ext_of_isRightKanExtension
leftDerived_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft leftDerivedLift	—	IsLeftDerivedFunctor.isRightKanExtension liftOfIsRightKanExtension_fac
leftDerived_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app leftDerivedLift comp	—	IsLeftDerivedFunctor.isRightKanExtension liftOfIsRightKanExtension_fac_app
leftDerived_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app leftDerivedLift comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerived_fac_app
leftDerived_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft leftDerivedLift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerived_fac

CategoryTheory.Functor.HasLeftDerivedFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasRightKanExtension	—	CategoryTheory.Functor.hasLeftDerivedFunctor_iff
hasRightKanExtension' 📖	mathematical	—	CategoryTheory.Functor.HasRightKanExtension CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.HasLeftDerivedFunctor	—	CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension CategoryTheory.Functor.hasLeftDerivedFunctor_iff

CategoryTheory.Functor.IsLeftDerivedFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsRightKanExtension	—	—

---

← Back to Index