RightDerived

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

Statistics

Metric	Count
Definitions HasRightDerivedFunctor, IsRightDerivedFunctor, rightDerivedDesc, rightDerivedNatIso, rightDerivedNatTrans, rightDerivedUnique, totalRightDerived, totalRightDerivedUnit	8
Theorems hasLeftKanExtension, hasLeftKanExtension', mk', isLeftKanExtension, hasRightDerivedFunctor_iff, hasRightDerivedFunctor_iff_of_iso, instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit, isRightDerivedFunctor_iff_isIso_rightDerivedDesc, isRightDerivedFunctor_iff_isLeftKanExtension, isRightDerivedFunctor_iff_of_iso, rightDerivedNatIso_hom, rightDerivedNatIso_inv, rightDerivedNatTrans_app, rightDerivedNatTrans_app_assoc, rightDerivedNatTrans_comp, rightDerivedNatTrans_comp_assoc, rightDerivedNatTrans_fac, rightDerivedNatTrans_fac_assoc, rightDerivedNatTrans_id, rightDerived_ext, rightDerived_fac, rightDerived_fac_app, rightDerived_fac_app_assoc, rightDerived_fac_assoc	24
Total	32

CategoryTheory.Functor

Definitions

Name	Category	Theorems
HasRightDerivedFunctor 📖	CompData	4 math math: hasRightDerivedFunctor_iff, HasRightDerivedFunctor.mk', hasRightDerivedFunctor_iff_of_iso, hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor
IsRightDerivedFunctor 📖	CompData	9 math math: isRightDerivedFunctor_iff_isLeftKanExtension, instIsRightDerivedFunctorLiftInvFac, isRightDerivedFunctor_iff_of_inverts, instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit, isRightDerivedFunctor_iff_of_iso, CategoryTheory.LocalizerMorphism.Derives.isRightDerivedFunctor_of_isIso, isRightDerivedFunctor_iff_isIso_rightDerivedDesc, isRightDerivedFunctor_of_inverts, CategoryTheory.LocalizerMorphism.Derives.isRightDerivedFunctor_iff_isIso
rightDerivedDesc 📖	CompOp	5 math math: rightDerived_fac_app, rightDerived_fac_assoc, rightDerived_fac_app_assoc, isRightDerivedFunctor_iff_isIso_rightDerivedDesc, rightDerived_fac
rightDerivedNatIso 📖	CompOp	2 math math: rightDerivedNatIso_inv, rightDerivedNatIso_hom
rightDerivedNatTrans 📖	CompOp	9 math math: rightDerivedNatTrans_id, rightDerivedNatIso_inv, rightDerivedNatTrans_comp, rightDerivedNatIso_hom, rightDerivedNatTrans_app_assoc, rightDerivedNatTrans_fac, rightDerivedNatTrans_comp_assoc, rightDerivedNatTrans_app, rightDerivedNatTrans_fac_assoc
rightDerivedUnique 📖	CompOp	—
totalRightDerived 📖	CompOp	1 math math: instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit
totalRightDerivedUnit 📖	CompOp	1 math math: instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasRightDerivedFunctor_iff 📖	mathematical	—	HasRightDerivedFunctor HasLeftKanExtension	—	HasRightDerivedFunctor.hasLeftKanExtension' hasLeftExtension_iff_postcomp₁ q_isLocalization CategoryTheory.Equivalence.isEquivalence_functor
hasRightDerivedFunctor_iff_of_iso 📖	mathematical	—	HasRightDerivedFunctor	—	hasRightDerivedFunctor_iff q_isLocalization hasLeftExtension_iff_of_iso₂
instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit 📖	mathematical	—	IsRightDerivedFunctor totalRightDerived totalRightDerivedUnit	—	HasRightDerivedFunctor.hasLeftKanExtension instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
isRightDerivedFunctor_iff_isIso_rightDerivedDesc 📖	mathematical	—	IsRightDerivedFunctor CategoryTheory.IsIso CategoryTheory.Functor category rightDerivedDesc	—	isRightDerivedFunctor_iff_isLeftKanExtension IsRightDerivedFunctor.isLeftKanExtension isLeftKanExtension_iff_isIso rightDerived_fac
isRightDerivedFunctor_iff_isLeftKanExtension 📖	mathematical	—	IsRightDerivedFunctor IsLeftKanExtension	—	IsRightDerivedFunctor.isLeftKanExtension
isRightDerivedFunctor_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsRightDerivedFunctor	—	isLeftKanExtension_iff_of_iso
rightDerivedNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category rightDerivedNatIso rightDerivedNatTrans	—	—
rightDerivedNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category rightDerivedNatIso rightDerivedNatTrans	—	—
rightDerivedNatTrans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.NatTrans.app rightDerivedNatTrans	—	rightDerived_fac_app
rightDerivedNatTrans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app comp rightDerivedNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedNatTrans_app
rightDerivedNatTrans_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerivedNatTrans	—	rightDerived_ext rightDerivedNatTrans_fac_assoc rightDerivedNatTrans_fac CategoryTheory.Category.assoc
rightDerivedNatTrans_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerivedNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedNatTrans_comp
rightDerivedNatTrans_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft rightDerivedNatTrans	—	rightDerived_fac
rightDerivedNatTrans_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft rightDerivedNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedNatTrans_fac
rightDerivedNatTrans_id 📖	mathematical	—	rightDerivedNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category	—	rightDerived_ext rightDerivedNatTrans_fac CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
rightDerived_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	—	—	IsRightDerivedFunctor.isLeftKanExtension hom_ext_of_isLeftKanExtension
rightDerived_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft rightDerivedDesc	—	IsRightDerivedFunctor.isLeftKanExtension descOfIsLeftKanExtension_fac
rightDerived_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.NatTrans.app rightDerivedDesc	—	IsRightDerivedFunctor.isLeftKanExtension descOfIsLeftKanExtension_fac_app
rightDerived_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app comp rightDerivedDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerived_fac_app
rightDerived_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft rightDerivedDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerived_fac

CategoryTheory.Functor.HasRightDerivedFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasLeftKanExtension	—	CategoryTheory.Functor.hasRightDerivedFunctor_iff
hasLeftKanExtension' 📖	mathematical	—	CategoryTheory.Functor.HasLeftKanExtension CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.HasRightDerivedFunctor	—	CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension CategoryTheory.Functor.hasRightDerivedFunctor_iff

CategoryTheory.Functor.IsRightDerivedFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension	—	—

---

← Back to Index