Pointwise

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

Statistics

Metric	Count
Definitions HasPointwiseLeftKanExtension, HasPointwiseLeftKanExtensionAt, HasPointwiseRightKanExtension, HasPointwiseRightKanExtensionAt, IsPointwiseLeftKanExtension, homFrom, isUniversal, IsPointwiseLeftKanExtensionAt, isoColimit, coconeAt, coconeAtFunctor, isPointwiseLeftKanExtensionAt, isPointwiseLeftKanExtensionAtEquivOfIso, isPointwiseLeftKanExtensionAtEquivOfIso', isPointwiseLeftKanExtensionAtOfIso', isPointwiseLeftKanExtensionEquivOfIso, IsPointwiseRightKanExtension, homTo, isUniversal, IsPointwiseRightKanExtensionAt, isoLimit, coneAt, coneAtFunctor, isPointwiseRightKanExtensionAt, isPointwiseRightKanExtensionAtEquivOfIso, isPointwiseRightKanExtensionAtEquivOfIso', isPointwiseRightKanExtensionAtOfIso', isPointwiseRightKanExtensionEquivOfIso, costructuredArrowMapCocone, isPointwiseLeftKanExtensionOfIsLeftKanExtension, isPointwiseRightKanExtensionOfIsRightKanExtension, pointwiseLeftKanExtension, pointwiseLeftKanExtensionIsPointwiseLeftKanExtension, pointwiseLeftKanExtensionIsUniversal, pointwiseLeftKanExtensionUnit, pointwiseRightKanExtension, pointwiseRightKanExtensionCounit, pointwiseRightKanExtensionIsPointwiseRightKanExtension, pointwiseRightKanExtensionIsUniversal, structuredArrowMapCone	40
Theorems hasLeftKanExtension, hasPointwiseLeftKanExtension, hom_ext, isIso_hom, isLeftKanExtension, comp_homEquiv_symm, comp_homEquiv_symm_assoc, hasPointwiseLeftKanExtensionAt, hom_ext', isIso_hom_app, ι_isoColimit_hom, ι_isoColimit_hom_assoc, ι_isoColimit_inv, ι_isoColimit_inv_assoc, coconeAtFunctor_map_hom, coconeAtFunctor_obj, coconeAt_pt, coconeAt_ι_app, instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt, instSubsingletonIsPointwiseLeftKanExtensionAt, hasPointwiseRightKanExtension, hasRightKanExtension, hom_ext, isIso_hom, isRightKanExtension, hasPointwiseRightKanExtensionAt, hom_ext', isIso_hom_app, isoLimit_hom_π, isoLimit_hom_π_assoc, isoLimit_inv_π, isoLimit_inv_π_assoc, coneAtFunctor_map_hom, coneAtFunctor_obj, coneAt_pt, coneAt_π_app, instIsClosedUnderIsomorphismsIsPointwiseRightKanExtensionAt, instSubsingletonIsPointwiseRightKanExtensionAt, costructuredArrowMapCocone_pt, costructuredArrowMapCocone_ι_app, hasPointwiseLeftKanExtensionAt_iff_of_equivalence, hasPointwiseLeftKanExtensionAt_iff_of_iso, hasPointwiseLeftKanExtensionAt_iff_of_natIso, hasPointwiseLeftKanExtensionAt_of_equivalence, hasPointwiseRightKanExtensionAt_iff_of_equivalence, hasPointwiseRightKanExtensionAt_iff_of_iso, hasPointwiseRightKanExtensionAt_iff_of_natIso, hasPointwiseRightKanExtensionAt_of_equivalence, instHasLeftKanExtension, instHasRightKanExtension, instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit, instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit, pointwiseLeftKanExtensionUnit_app, pointwiseLeftKanExtension_desc_app, pointwiseLeftKanExtension_map, pointwiseLeftKanExtension_obj, pointwiseRightKanExtensionCounit_app, pointwiseRightKanExtension_lift_app, pointwiseRightKanExtension_map, pointwiseRightKanExtension_obj, structuredArrowMapCone_pt, structuredArrowMapCone_π_app	62
Total	102

CategoryTheory.Functor

Definitions

Name	Category	Theorems
HasPointwiseLeftKanExtension 📖	MathDef	3 math math: LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension, hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor, CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension_iff
HasPointwiseLeftKanExtensionAt 📖	MathDef	9 math math: hasPointwiseLeftKanExtensionAt_iff_of_equivalence, hasPointwiseLeftKanExtensionAt_iff_of_natIso, CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff, HasPointwiseRightDerivedFunctorAt.hasColimit, hasPointwiseLeftKanExtensionAt_iff_of_iso, HasPointwiseRightDerivedFunctorAt.hasColimit', hasPointwiseRightDerivedFunctorAt_iff, LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt, hasPointwiseLeftKanExtensionAt_of_equivalence
HasPointwiseRightKanExtension 📖	MathDef	2 math math: hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor, RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension
HasPointwiseRightKanExtensionAt 📖	MathDef	8 math math: HasPointwiseLeftDerivedFunctorAt.hasLimit', RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt, hasPointwiseRightKanExtensionAt_iff_of_natIso, hasPointwiseRightKanExtensionAt_iff_of_iso, hasPointwiseLeftDerivedFunctorAt_iff, hasPointwiseRightKanExtensionAt_iff_of_equivalence, HasPointwiseLeftDerivedFunctorAt.hasLimit, hasPointwiseRightKanExtensionAt_of_equivalence
costructuredArrowMapCocone 📖	CompOp	3 math math: costructuredArrowMapCocone_pt, pointwiseLeftKanExtension_desc_app, costructuredArrowMapCocone_ι_app
isPointwiseLeftKanExtensionOfIsLeftKanExtension 📖	CompOp	—
isPointwiseRightKanExtensionOfIsRightKanExtension 📖	CompOp	—
pointwiseLeftKanExtension 📖	CompOp	15 math math: instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseLeftKanExtension_obj, pointwiseLeftKanExtension_map, pointwiseLeftKanExtensionUnit_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseLeftKanExtension_desc_app, CategoryTheory.MonoidalCategory.DayFunctor.η_comp_isoPointwiseLeftKanExtension_hom, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, CategoryTheory.MonoidalCategory.DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseLeftKanExtensionIsPointwiseLeftKanExtension 📖	CompOp	—
pointwiseLeftKanExtensionIsUniversal 📖	CompOp	—
pointwiseLeftKanExtensionUnit 📖	CompOp	11 math math: instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseLeftKanExtensionUnit_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseLeftKanExtension_desc_app, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
pointwiseRightKanExtension 📖	CompOp	13 math math: pointwiseRightKanExtension_lift_app, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app, pointwiseRightKanExtensionCounit_app, pointwiseRightKanExtension_obj, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtension_map, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac, instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit
pointwiseRightKanExtensionCounit 📖	CompOp	11 math math: pointwiseRightKanExtension_lift_app, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app, pointwiseRightKanExtensionCounit_app, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac, instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit
pointwiseRightKanExtensionIsPointwiseRightKanExtension 📖	CompOp	—
pointwiseRightKanExtensionIsUniversal 📖	CompOp	—
structuredArrowMapCone 📖	CompOp	3 math math: pointwiseRightKanExtension_lift_app, structuredArrowMapCone_pt, structuredArrowMapCone_π_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
costructuredArrowMapCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj costructuredArrowMapCocone obj	—	—
costructuredArrowMapCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj obj CategoryTheory.Functor category const CategoryTheory.Limits.Cocone.ι costructuredArrowMapCocone CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit map CategoryTheory.Comma.hom	—	—
hasPointwiseLeftKanExtensionAt_iff_of_equivalence 📖	mathematical	—	HasPointwiseLeftKanExtensionAt	—	hasPointwiseLeftKanExtensionAt_of_equivalence
hasPointwiseLeftKanExtensionAt_iff_of_iso 📖	mathematical	—	HasPointwiseLeftKanExtensionAt	—	CategoryTheory.Limits.hasColimit_equivalence_comp
hasPointwiseLeftKanExtensionAt_iff_of_natIso 📖	mathematical	—	HasPointwiseLeftKanExtensionAt	—	CategoryTheory.Limits.hasColimit_of_iso CategoryTheory.Limits.hasColimit_equivalence_comp
hasPointwiseLeftKanExtensionAt_of_equivalence 📖	mathematical	—	HasPointwiseLeftKanExtensionAt	—	hasPointwiseLeftKanExtensionAt_iff_of_natIso hasPointwiseLeftKanExtensionAt_iff_of_iso CategoryTheory.CostructuredArrow.isEquivalence_post CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor CategoryTheory.Limits.hasColimit_of_equivalence_comp
hasPointwiseRightKanExtensionAt_iff_of_equivalence 📖	mathematical	—	HasPointwiseRightKanExtensionAt	—	hasPointwiseRightKanExtensionAt_of_equivalence
hasPointwiseRightKanExtensionAt_iff_of_iso 📖	mathematical	—	HasPointwiseRightKanExtensionAt	—	CategoryTheory.Limits.hasLimit_equivalence_comp
hasPointwiseRightKanExtensionAt_iff_of_natIso 📖	mathematical	—	HasPointwiseRightKanExtensionAt	—	CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.Limits.hasLimit_equivalence_comp
hasPointwiseRightKanExtensionAt_of_equivalence 📖	mathematical	—	HasPointwiseRightKanExtensionAt	—	hasPointwiseRightKanExtensionAt_iff_of_natIso hasPointwiseRightKanExtensionAt_iff_of_iso CategoryTheory.StructuredArrow.isEquivalence_post CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor CategoryTheory.Limits.hasLimit_of_equivalence_comp
instHasLeftKanExtension 📖	mathematical	HasPointwiseLeftKanExtension	HasLeftKanExtension	—	instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit
instHasRightKanExtension 📖	mathematical	HasPointwiseRightKanExtension	HasRightKanExtension	—	instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit
instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit 📖	mathematical	HasPointwiseLeftKanExtension	IsLeftKanExtension pointwiseLeftKanExtension pointwiseLeftKanExtensionUnit	—	—
instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit 📖	mathematical	HasPointwiseRightKanExtension	IsRightKanExtension pointwiseRightKanExtension pointwiseRightKanExtensionCounit	—	—
pointwiseLeftKanExtensionUnit_app 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.NatTrans.app comp pointwiseLeftKanExtension pointwiseLeftKanExtensionUnit CategoryTheory.Limits.colimit.ι CategoryTheory.CostructuredArrow obj CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
pointwiseLeftKanExtension_desc_app 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.NatTrans.app pointwiseLeftKanExtension descOfIsLeftKanExtension pointwiseLeftKanExtensionUnit instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj costructuredArrowMapCocone	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Limits.colimit.ι_desc map_comp CategoryTheory.Category.assoc instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit hom_ext_of_isLeftKanExtension descOfIsLeftKanExtension_fac CategoryTheory.NatTrans.ext' map_id CategoryTheory.Category.comp_id CategoryTheory.NatTrans.congr_app
pointwiseLeftKanExtension_map 📖	mathematical	HasPointwiseLeftKanExtension	map pointwiseLeftKanExtension CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.colimit obj CategoryTheory.Functor category const CategoryTheory.Limits.colimit.ι CategoryTheory.CostructuredArrow.map	—	—
pointwiseLeftKanExtension_obj 📖	mathematical	HasPointwiseLeftKanExtension	obj pointwiseLeftKanExtension CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj	—	—
pointwiseRightKanExtensionCounit_app 📖	mathematical	HasPointwiseRightKanExtension	CategoryTheory.NatTrans.app comp pointwiseRightKanExtension pointwiseRightKanExtensionCounit CategoryTheory.Limits.limit.π CategoryTheory.StructuredArrow obj CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
pointwiseRightKanExtension_lift_app 📖	mathematical	HasPointwiseRightKanExtension	CategoryTheory.NatTrans.app pointwiseRightKanExtension liftOfIsRightKanExtension pointwiseRightKanExtensionCounit instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit CategoryTheory.Limits.limit.lift CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj structuredArrowMapCone	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π map_comp instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit hom_ext_of_isRightKanExtension liftOfIsRightKanExtension_fac CategoryTheory.NatTrans.ext' map_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.congr_app
pointwiseRightKanExtension_map 📖	mathematical	HasPointwiseRightKanExtension	map pointwiseRightKanExtension CategoryTheory.Limits.limit.lift CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj CategoryTheory.Limits.limit obj CategoryTheory.Functor category const CategoryTheory.Limits.limit.π CategoryTheory.StructuredArrow.map	—	—
pointwiseRightKanExtension_obj 📖	mathematical	HasPointwiseRightKanExtension	obj pointwiseRightKanExtension CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj	—	—
structuredArrowMapCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj structuredArrowMapCone obj	—	—
structuredArrowMapCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow obj CategoryTheory.Functor category const comp CategoryTheory.StructuredArrow.proj CategoryTheory.Limits.Cone.π structuredArrowMapCone CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit map CategoryTheory.Comma.hom	—	—

CategoryTheory.Functor.LeftExtension

Definitions

Name	Category	Theorems
IsPointwiseLeftKanExtension 📖	CompOp	1 math math: CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension
IsPointwiseLeftKanExtensionAt 📖	CompOp	3 math math: instSubsingletonIsPointwiseLeftKanExtensionAt, nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff, CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.preserves
coconeAt 📖	CompOp	9 math math: coconeAtFunctor_map_hom, coconeAtWhiskerRightIso_inv_hom, CategoryTheory.Functor.isDenseAt_iff, coconeAtFunctor_obj, coconeAtWhiskerRightIso_hom_hom, IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, coconeAt_pt, coconeAt_ι_app, IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc
coconeAtFunctor 📖	CompOp	2 math math: coconeAtFunctor_map_hom, coconeAtFunctor_obj
isPointwiseLeftKanExtensionAt 📖	CompOp	2 math math: CategoryTheory.Functor.isDenseAt_eq_isPointwiseLeftKanExtensionAt, instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt
isPointwiseLeftKanExtensionAtEquivOfIso 📖	CompOp	—
isPointwiseLeftKanExtensionAtEquivOfIso' 📖	CompOp	—
isPointwiseLeftKanExtensionAtOfIso' 📖	CompOp	—
isPointwiseLeftKanExtensionEquivOfIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeAtFunctor_map_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj coconeAt CategoryTheory.Functor.map CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category coconeAtFunctor CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.right	—	—
coconeAtFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.Cocone CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.Cocone.category coconeAtFunctor coconeAt	—	—
coconeAt_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj coconeAt CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft	—	—
coconeAt_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.Cocone.ι coconeAt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	—
instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms isPointwiseLeftKanExtensionAt	—	—
instSubsingletonIsPointwiseLeftKanExtensionAt 📖	mathematical	—	IsPointwiseLeftKanExtensionAt	—	CategoryTheory.Limits.IsColimit.subsingleton

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension

Definitions

Name	Category	Theorems
homFrom 📖	CompOp	—
isUniversal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasLeftKanExtension	—	isLeftKanExtension
hasPointwiseLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasPointwiseLeftKanExtension	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt
hom_ext 📖	—	—	—	—	CategoryTheory.StructuredArrow.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.congr_app CategoryTheory.StructuredArrow.w CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality Mathlib.Tactic.Reassoc.eq_whisker'
isIso_hom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app CategoryTheory.NatIso.isIso_of_isIso_app
isLeftKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt

Definitions

Name	Category	Theorems
isoColimit 📖	CompOp	4 math math: ι_isoColimit_hom, ι_isoColimit_hom_assoc, ι_isoColimit_inv_assoc, ι_isoColimit_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_homEquiv_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map DFunLike.coe Equiv Quiver.Hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.LeftExtension.coconeAt EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Limits.IsColimit.homEquiv	—	CategoryTheory.Category.assoc CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm
comp_homEquiv_symm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map DFunLike.coe Equiv Quiver.Hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.LeftExtension.coconeAt EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Limits.IsColimit.homEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_homEquiv_symm
hasPointwiseLeftKanExtensionAt 📖	mathematical	—	CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt	—	—
hom_ext' 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Category.assoc
isIso_hom_app 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal
ι_isoColimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Iso.hom isoColimit CategoryTheory.Limits.colimit.ι	—	CategoryTheory.Category.assoc CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
ι_isoColimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.hom isoColimit CategoryTheory.Limits.colimit.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_isoColimit_hom
ι_isoColimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.colimit CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv isoColimit CategoryTheory.Comma.left CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
ι_isoColimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Limits.colimit.ι CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.inv isoColimit CategoryTheory.Comma.left CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_isoColimit_inv

CategoryTheory.Functor.RightExtension

Definitions

Name	Category	Theorems
IsPointwiseRightKanExtension 📖	CompOp	—
IsPointwiseRightKanExtensionAt 📖	CompOp	2 math math: instSubsingletonIsPointwiseRightKanExtensionAt, CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.preserves
coneAt 📖	CompOp	6 math math: coneAt_pt, coneAt_π_app, coneAtFunctor_obj, coneAtWhiskerRightIso_inv_hom, coneAtFunctor_map_hom, coneAtWhiskerRightIso_hom_hom
coneAtFunctor 📖	CompOp	2 math math: coneAtFunctor_obj, coneAtFunctor_map_hom
isPointwiseRightKanExtensionAt 📖	CompOp	1 math math: instIsClosedUnderIsomorphismsIsPointwiseRightKanExtensionAt
isPointwiseRightKanExtensionAtEquivOfIso 📖	CompOp	—
isPointwiseRightKanExtensionAtEquivOfIso' 📖	CompOp	—
isPointwiseRightKanExtensionAtOfIso' 📖	CompOp	—
isPointwiseRightKanExtensionEquivOfIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneAtFunctor_map_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj coneAt CategoryTheory.Functor.map CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category coneAtFunctor CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	—
coneAtFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.Cone CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Limits.Cone.category coneAtFunctor coneAt	—	—
coneAt_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj coneAt CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit	—	—
coneAt_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Limits.Cone.π coneAt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
instIsClosedUnderIsomorphismsIsPointwiseRightKanExtensionAt 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms isPointwiseRightKanExtensionAt	—	—
instSubsingletonIsPointwiseRightKanExtensionAt 📖	mathematical	—	IsPointwiseRightKanExtensionAt	—	CategoryTheory.Limits.IsLimit.subsingleton

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension

Definitions

Name	Category	Theorems
homTo 📖	CompOp	—
isUniversal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPointwiseRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasPointwiseRightKanExtension	—	CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt
hasRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.HasRightKanExtension	—	isRightKanExtension
hom_ext 📖	—	—	—	—	CategoryTheory.CostructuredArrow.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.congr_app CategoryTheory.CostructuredArrow.w
isIso_hom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app CategoryTheory.NatIso.isIso_of_isIso_app
isRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsRightKanExtension CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt

Definitions

Name	Category	Theorems
isoLimit 📖	CompOp	4 math math: isoLimit_inv_π, isoLimit_inv_π_assoc, isoLimit_hom_π, isoLimit_hom_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPointwiseRightKanExtensionAt 📖	mathematical	—	CategoryTheory.Functor.HasPointwiseRightKanExtensionAt	—	—
hom_ext' 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	—	CategoryTheory.Limits.IsLimit.hom_ext
isIso_hom_app 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial
isoLimit_hom_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.hom isoLimit CategoryTheory.Limits.limit.π CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
isoLimit_hom_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.hom isoLimit CategoryTheory.Limits.limit.π CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLimit_hom_π
isoLimit_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Iso.inv isoLimit CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
isoLimit_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Iso.inv isoLimit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.limit.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLimit_inv_π

---

← Back to Index