Preserves

📁 Source: Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean

Statistics

Metric	Count
Definitions postcompose, postcompose, coconeAtWhiskerRightIso, PreservesLeftKanExtension, PreservesLeftKanExtensions, PreservesPointwiseLeftKanExtension, PreservesPointwiseLeftKanExtensionAt, PreservesPointwiseLeftKanExtensions, PreservesPointwiseRightKanExtension, PreservesPointwiseRightKanExtensionAt, PreservesPointwiseRightKanExtensions, PreservesRightKanExtension, PreservesRightKanExtensions, postcompose, postcompose, coneAtWhiskerRightIso, lanCompIsoOfPreserves, leftKanExtensionCompIsoOfPreserves, pointwiseLeftKanExtensionCompIsoOfPreserves, pointwiseRightKanExtensionCompIsoOfPreserves, ranCompIsoOfPreserves, rightKanExtensionCompIsoOfPreserves	22
Theorems coconeAtWhiskerRightIso_hom_hom, coconeAtWhiskerRightIso_inv_hom, mk', mk_of_preserves_isLeftKanExtension, mk_of_preserves_isUniversal, preserves, mk', preserves, mk', preserves, mk', mk_of_preserves_isRightKanExtension, mk_of_preserves_isUniversal, preserves, coneAtWhiskerRightIso_hom_hom, coneAtWhiskerRightIso_inv_hom, hasLeftKanExtension_of_preserves, hasPointwiseLeftKanExtension_of_preserves, hasPointwiseRightKanExtension_of_preserves, hasRightKanExtension_of_preserves, lanCompIsoOfPreserves_hom_app, lanCompIsoOfPreserves_inv_app, leftKanExtensionCompIsoOfPreserves_hom_fac, leftKanExtensionCompIsoOfPreserves_hom_fac_app, leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac, leftKanExtensionCompIsoOfPreserves_inv_fac_app, leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise, preservesPointwiseLeftKanExtensionAtOfPreservesColimit, preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise, preservesPointwiseRightKanExtensionAtOfPreservesLimit, ranCompIsoOfPreserves_hom_app, ranCompIsoOfPreserves_inv_app, rightKanExtensionCompIsoOfPreserves_hom_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac, rightKanExtensionCompIsoOfPreserves_inv_fac_app, rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc	60
Total	82

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PreservesLeftKanExtension 📖	CompData	4 math math: preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise, PreservesLeftKanExtension.mk', PreservesLeftKanExtension.mk_of_preserves_isUniversal, PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension
PreservesLeftKanExtensions 📖	MathDef	—
PreservesPointwiseLeftKanExtension 📖	MathDef	—
PreservesPointwiseLeftKanExtensionAt 📖	CompData	2 math math: preservesPointwiseLeftKanExtensionAtOfPreservesColimit, PreservesPointwiseLeftKanExtensionAt.mk'
PreservesPointwiseLeftKanExtensions 📖	MathDef	—
PreservesPointwiseRightKanExtension 📖	MathDef	—
PreservesPointwiseRightKanExtensionAt 📖	CompData	2 math math: PreservesPointwiseRightKanExtensionAt.mk', preservesPointwiseRightKanExtensionAtOfPreservesLimit
PreservesPointwiseRightKanExtensions 📖	MathDef	—
PreservesRightKanExtension 📖	CompData	4 math math: PreservesRightKanExtension.mk', PreservesRightKanExtension.mk_of_preserves_isRightKanExtension, PreservesRightKanExtension.mk_of_preserves_isUniversal, preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise
PreservesRightKanExtensions 📖	MathDef	—
lanCompIsoOfPreserves 📖	CompOp	2 math math: lanCompIsoOfPreserves_inv_app, lanCompIsoOfPreserves_hom_app
leftKanExtensionCompIsoOfPreserves 📖	CompOp	10 math math: leftKanExtensionCompIsoOfPreserves_hom_fac_app, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac, lanCompIsoOfPreserves_inv_app, leftKanExtensionCompIsoOfPreserves_inv_fac, lanCompIsoOfPreserves_hom_app, leftKanExtensionCompIsoOfPreserves_inv_fac_app
pointwiseLeftKanExtensionCompIsoOfPreserves 📖	CompOp	8 math math: pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseRightKanExtensionCompIsoOfPreserves 📖	CompOp	8 math math: pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac
ranCompIsoOfPreserves 📖	CompOp	2 math math: ranCompIsoOfPreserves_inv_app, ranCompIsoOfPreserves_hom_app
rightKanExtensionCompIsoOfPreserves 📖	CompOp	10 math math: rightKanExtensionCompIsoOfPreserves_inv_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, ranCompIsoOfPreserves_inv_app, ranCompIsoOfPreserves_hom_app, rightKanExtensionCompIsoOfPreserves_hom_fac, rightKanExtensionCompIsoOfPreserves_inv_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLeftKanExtension_of_preserves 📖	mathematical	—	HasLeftKanExtension comp	—	PreservesLeftKanExtension.preserves instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
hasPointwiseLeftKanExtension_of_preserves 📖	mathematical	HasPointwiseLeftKanExtension PreservesPointwiseLeftKanExtension	comp	—	LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension
hasPointwiseRightKanExtension_of_preserves 📖	mathematical	HasPointwiseRightKanExtension PreservesPointwiseRightKanExtension	comp	—	RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension
hasRightKanExtension_of_preserves 📖	mathematical	—	HasRightKanExtension comp	—	PreservesRightKanExtension.preserves instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit
lanCompIsoOfPreserves_hom_app 📖	mathematical	PreservesLeftKanExtensions HasLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp lan obj whiskeringRight CategoryTheory.Iso.hom lanCompIsoOfPreserves leftKanExtensionCompIsoOfPreserves	—	—
lanCompIsoOfPreserves_inv_app 📖	mathematical	PreservesLeftKanExtensions HasLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp obj whiskeringRight lan CategoryTheory.Iso.inv lanCompIsoOfPreserves leftKanExtensionCompIsoOfPreserves	—	—
leftKanExtensionCompIsoOfPreserves_hom_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension hasLeftKanExtension_of_preserves whiskerRight leftKanExtensionUnit CategoryTheory.Iso.hom associator whiskerLeft leftKanExtensionCompIsoOfPreserves	—	hasLeftKanExtension_of_preserves leftKanExtensionUnique_hom PreservesLeftKanExtension.preserves instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit CategoryTheory.Category.assoc descOfIsLeftKanExtension_fac
leftKanExtensionCompIsoOfPreserves_hom_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp leftKanExtension hasLeftKanExtension_of_preserves map CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Iso.hom CategoryTheory.Functor category leftKanExtensionCompIsoOfPreserves	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app leftKanExtensionCompIsoOfPreserves_hom_fac
leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftKanExtension map CategoryTheory.NatTrans.app comp leftKanExtensionUnit hasLeftKanExtension_of_preserves CategoryTheory.Iso.hom CategoryTheory.Functor category leftKanExtensionCompIsoOfPreserves	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftKanExtensionCompIsoOfPreserves_hom_fac_app
leftKanExtensionCompIsoOfPreserves_hom_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension whiskerRight leftKanExtensionUnit CategoryTheory.Iso.hom associator hasLeftKanExtension_of_preserves whiskerLeft leftKanExtensionCompIsoOfPreserves	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftKanExtensionCompIsoOfPreserves_hom_fac
leftKanExtensionCompIsoOfPreserves_inv_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension hasLeftKanExtension_of_preserves leftKanExtensionUnit whiskerLeft CategoryTheory.Iso.inv leftKanExtensionCompIsoOfPreserves whiskerRight CategoryTheory.Iso.hom associator	—	hasLeftKanExtension_of_preserves leftKanExtensionUnique_inv descOfIsLeftKanExtension_fac
leftKanExtensionCompIsoOfPreserves_inv_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp leftKanExtension hasLeftKanExtension_of_preserves CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Iso.inv CategoryTheory.Functor category leftKanExtensionCompIsoOfPreserves map	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.comp_id CategoryTheory.NatTrans.congr_app leftKanExtensionCompIsoOfPreserves_inv_fac
leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftKanExtension comp hasLeftKanExtension_of_preserves CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Iso.inv CategoryTheory.Functor category leftKanExtensionCompIsoOfPreserves map	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftKanExtensionCompIsoOfPreserves_inv_fac_app
leftKanExtensionCompIsoOfPreserves_inv_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension hasLeftKanExtension_of_preserves leftKanExtensionUnit whiskerLeft CategoryTheory.Iso.inv leftKanExtensionCompIsoOfPreserves whiskerRight CategoryTheory.Iso.hom associator	—	hasLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp pointwiseLeftKanExtension hasPointwiseLeftKanExtension_of_preserves CategoryTheory.NatTrans.app pointwiseLeftKanExtensionUnit CategoryTheory.Iso.inv CategoryTheory.Functor category pointwiseLeftKanExtensionCompIsoOfPreserves map	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.comp_id CategoryTheory.NatTrans.congr_app pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj pointwiseLeftKanExtension comp hasPointwiseLeftKanExtension_of_preserves CategoryTheory.NatTrans.app pointwiseLeftKanExtensionUnit CategoryTheory.Iso.inv CategoryTheory.Functor category pointwiseLeftKanExtensionCompIsoOfPreserves map	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app
pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseLeftKanExtension hasPointwiseLeftKanExtension_of_preserves whiskerRight pointwiseLeftKanExtensionUnit CategoryTheory.Iso.hom associator whiskerLeft pointwiseLeftKanExtensionCompIsoOfPreserves	—	hasPointwiseLeftKanExtension_of_preserves leftKanExtensionUnique_hom PreservesLeftKanExtension.preserves preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit CategoryTheory.Category.assoc descOfIsLeftKanExtension_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp pointwiseLeftKanExtension hasPointwiseLeftKanExtension_of_preserves map CategoryTheory.NatTrans.app pointwiseLeftKanExtensionUnit CategoryTheory.Iso.hom CategoryTheory.Functor category pointwiseLeftKanExtensionCompIsoOfPreserves	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj pointwiseLeftKanExtension map CategoryTheory.NatTrans.app comp pointwiseLeftKanExtensionUnit hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Iso.hom CategoryTheory.Functor category pointwiseLeftKanExtensionCompIsoOfPreserves	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app
pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseLeftKanExtension whiskerRight pointwiseLeftKanExtensionUnit CategoryTheory.Iso.hom associator hasPointwiseLeftKanExtension_of_preserves whiskerLeft pointwiseLeftKanExtensionCompIsoOfPreserves	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseLeftKanExtension hasPointwiseLeftKanExtension_of_preserves pointwiseLeftKanExtensionUnit whiskerLeft CategoryTheory.Iso.inv pointwiseLeftKanExtensionCompIsoOfPreserves whiskerRight CategoryTheory.Iso.hom associator	—	hasPointwiseLeftKanExtension_of_preserves leftKanExtensionUnique_inv descOfIsLeftKanExtension_fac
pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc 📖	mathematical	PreservesPointwiseLeftKanExtension HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseLeftKanExtension hasPointwiseLeftKanExtension_of_preserves pointwiseLeftKanExtensionUnit whiskerLeft CategoryTheory.Iso.inv pointwiseLeftKanExtensionCompIsoOfPreserves whiskerRight CategoryTheory.Iso.hom associator	—	hasPointwiseLeftKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseRightKanExtension hasPointwiseRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.hom pointwiseRightKanExtensionCompIsoOfPreserves pointwiseRightKanExtensionCounit CategoryTheory.Iso.inv associator whiskerRight	—	hasPointwiseRightKanExtension_of_preserves rightKanExtensionUnique_hom liftOfIsRightKanExtension_fac
pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp pointwiseRightKanExtension hasPointwiseRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category pointwiseRightKanExtensionCompIsoOfPreserves pointwiseRightKanExtensionCounit map	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac
pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj pointwiseRightKanExtension comp hasPointwiseRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category pointwiseRightKanExtensionCompIsoOfPreserves pointwiseRightKanExtensionCounit map	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app
pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseRightKanExtension hasPointwiseRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.hom pointwiseRightKanExtensionCompIsoOfPreserves pointwiseRightKanExtensionCounit CategoryTheory.Iso.inv associator whiskerRight	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac
pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseRightKanExtension hasPointwiseRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.inv pointwiseRightKanExtensionCompIsoOfPreserves associator whiskerRight pointwiseRightKanExtensionCounit	—	hasPointwiseRightKanExtension_of_preserves rightKanExtensionUnique_inv liftOfIsRightKanExtension_fac
pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj pointwiseRightKanExtension comp hasPointwiseRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category pointwiseRightKanExtensionCompIsoOfPreserves map pointwiseRightKanExtensionCounit	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac
pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj pointwiseRightKanExtension comp hasPointwiseRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category pointwiseRightKanExtensionCompIsoOfPreserves map pointwiseRightKanExtensionCounit	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app
pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc 📖	mathematical	PreservesPointwiseRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp pointwiseRightKanExtension hasPointwiseRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.inv pointwiseRightKanExtensionCompIsoOfPreserves associator whiskerRight pointwiseRightKanExtensionCounit	—	hasPointwiseRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac
preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise 📖	mathematical	HasPointwiseLeftKanExtension PreservesPointwiseLeftKanExtension	PreservesLeftKanExtension	—	LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
preservesPointwiseLeftKanExtensionAtOfPreservesColimit 📖	mathematical	—	PreservesPointwiseLeftKanExtensionAt	—	CategoryTheory.Limits.PreservesColimit.preserves
preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise 📖	mathematical	HasPointwiseRightKanExtension PreservesPointwiseRightKanExtension	PreservesRightKanExtension	—	RightExtension.IsPointwiseRightKanExtension.isRightKanExtension
preservesPointwiseRightKanExtensionAtOfPreservesLimit 📖	mathematical	—	PreservesPointwiseRightKanExtensionAt	—	CategoryTheory.Limits.PreservesLimit.preserves
ranCompIsoOfPreserves_hom_app 📖	mathematical	PreservesRightKanExtensions HasRightKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp ran obj whiskeringRight CategoryTheory.Iso.hom ranCompIsoOfPreserves rightKanExtensionCompIsoOfPreserves	—	—
ranCompIsoOfPreserves_inv_app 📖	mathematical	PreservesRightKanExtensions HasRightKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp obj whiskeringRight ran CategoryTheory.Iso.inv ranCompIsoOfPreserves rightKanExtensionCompIsoOfPreserves	—	—
rightKanExtensionCompIsoOfPreserves_hom_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension hasRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.hom rightKanExtensionCompIsoOfPreserves rightKanExtensionCounit CategoryTheory.Iso.inv associator whiskerRight	—	hasRightKanExtension_of_preserves rightKanExtensionUnique_hom liftOfIsRightKanExtension_fac
rightKanExtensionCompIsoOfPreserves_hom_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp rightKanExtension hasRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category rightKanExtensionCompIsoOfPreserves rightKanExtensionCounit map	—	hasRightKanExtension_of_preserves rightKanExtensionUnique_hom liftOfIsRightKanExtension_fac_app CategoryTheory.Category.id_comp
rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightKanExtension comp hasRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category rightKanExtensionCompIsoOfPreserves rightKanExtensionCounit map	—	hasRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightKanExtensionCompIsoOfPreserves_hom_fac_app
rightKanExtensionCompIsoOfPreserves_hom_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension hasRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.hom rightKanExtensionCompIsoOfPreserves rightKanExtensionCounit CategoryTheory.Iso.inv associator whiskerRight	—	hasRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightKanExtensionCompIsoOfPreserves_hom_fac
rightKanExtensionCompIsoOfPreserves_inv_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension hasRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.inv rightKanExtensionCompIsoOfPreserves associator whiskerRight rightKanExtensionCounit	—	hasRightKanExtension_of_preserves rightKanExtensionUnique_inv liftOfIsRightKanExtension_fac
rightKanExtensionCompIsoOfPreserves_inv_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightKanExtension comp hasRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category rightKanExtensionCompIsoOfPreserves map rightKanExtensionCounit	—	hasRightKanExtension_of_preserves CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app rightKanExtensionCompIsoOfPreserves_inv_fac
rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightKanExtension comp hasRightKanExtension_of_preserves CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category rightKanExtensionCompIsoOfPreserves map rightKanExtensionCounit	—	hasRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightKanExtensionCompIsoOfPreserves_inv_fac_app
rightKanExtensionCompIsoOfPreserves_inv_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension hasRightKanExtension_of_preserves whiskerLeft CategoryTheory.Iso.inv rightKanExtensionCompIsoOfPreserves associator whiskerRight rightKanExtensionCounit	—	hasRightKanExtension_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightKanExtensionCompIsoOfPreserves_inv_fac

CategoryTheory.Functor.LeftExtension

Definitions

Name	Category	Theorems
coconeAtWhiskerRightIso 📖	CompOp	2 math math: coconeAtWhiskerRightIso_inv_hom, coconeAtWhiskerRightIso_hom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeAtWhiskerRightIso_hom_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj coconeAt CategoryTheory.Functor.obj CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft postcompose₂ CategoryTheory.Functor.mapCocone CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category coconeAtWhiskerRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
coconeAtWhiskerRightIso_inv_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.mapCocone coconeAt CategoryTheory.Functor.obj CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft postcompose₂ CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category coconeAtWhiskerRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension

Definitions

Name	Category	Theorems
postcompose 📖	CompOp	—

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt

Definitions

Name	Category	Theorems
postcompose 📖	CompOp	—

CategoryTheory.Functor.PreservesLeftKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.StructuredArrow.IsUniversal CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.LeftExtension.postcompose₂	CategoryTheory.Functor.PreservesLeftKanExtension	—	CategoryTheory.Functor.IsLeftKanExtension.nonempty_isUniversal
mk_of_preserves_isLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.PreservesLeftKanExtension	—	CategoryTheory.Functor.isLeftKanExtension_of_iso CategoryTheory.NatTrans.ext' CategoryTheory.Functor.leftKanExtensionUnique_hom CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app CategoryTheory.Category.comp_id
mk_of_preserves_isUniversal 📖	mathematical	—	CategoryTheory.Functor.PreservesLeftKanExtension	—	mk'
preserves 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator	—	—

CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	—	CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt	—	—
preserves 📖	mathematical	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension.postcompose₂	—	—

CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	—	CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt	—	—
preserves 📖	mathematical	—	CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.RightExtension.postcompose₂	—	—

CategoryTheory.Functor.PreservesRightKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.CostructuredArrow.IsUniversal CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.RightExtension.postcompose₂	CategoryTheory.Functor.PreservesRightKanExtension	—	CategoryTheory.Functor.IsRightKanExtension.nonempty_isUniversal
mk_of_preserves_isRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.PreservesRightKanExtension	—	CategoryTheory.Functor.isRightKanExtension_of_iso CategoryTheory.NatTrans.ext' CategoryTheory.Functor.rightKanExtensionUnique_hom CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app
mk_of_preserves_isUniversal 📖	mathematical	—	CategoryTheory.Functor.PreservesRightKanExtension	—	mk'
preserves 📖	mathematical	—	CategoryTheory.Functor.IsRightKanExtension CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight	—	—

CategoryTheory.Functor.RightExtension

Definitions

Name	Category	Theorems
coneAtWhiskerRightIso 📖	CompOp	2 math math: coneAtWhiskerRightIso_inv_hom, coneAtWhiskerRightIso_hom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneAtWhiskerRightIso_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj coneAt CategoryTheory.Functor.obj CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft postcompose₂ CategoryTheory.Functor.mapCone CategoryTheory.Iso.hom CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category coneAtWhiskerRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
coneAtWhiskerRightIso_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.mapCone coneAt CategoryTheory.Functor.obj CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft postcompose₂ CategoryTheory.Iso.inv CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category coneAtWhiskerRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension

Definitions

Name	Category	Theorems
postcompose 📖	CompOp	—

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt

Definitions

Name	Category	Theorems
postcompose 📖	CompOp	—

---

← Back to Index