ExponentiableMorphism

📁 Source: Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean

Statistics

Metric	Count
Definitions ExponentiableMorphism, OverMkHom, coev, comp, ev, id, instChosenPullbacksAlongHomDiscretePUnitMk, pullbackPushforwardAdj, pushforward, pushforwardComp, pushforwardCurry, pushforwardId, pushforwardUncurry, IsExponentiable	14
Theorems coev_def, coev_ev, coev_ev_assoc, coev_naturality, coev_naturality_assoc, comp_pushforward, ev_coev, ev_coev_assoc, ev_def, ev_naturality, ev_naturality_assoc, homEquiv_apply_eq, homEquiv_symm_apply_eq, id_pushforward, isExponentiable, pushforwardComp_hom_counit, pushforwardComp_hom_counit_assoc, pushforwardId_hom_counit, pushforwardId_hom_counit_assoc, pushforward_curry_uncurry, pushforward_uncurry_curry, unit_pushforwardComp_hom, unit_pushforwardComp_hom_assoc, unit_pushforwardId_hom, unit_pushforwardId_hom_assoc	25
Total	39

CategoryTheory

Definitions

Name	Category	Theorems
ExponentiableMorphism 📖	CompData	—
IsExponentiable 📖	CompOp	1 math math: ExponentiableMorphism.isExponentiable

CategoryTheory.ExponentiableMorphism

Definitions

Name	Category	Theorems
OverMkHom 📖	CompOp	—
coev 📖	CompOp	7 math math: ev_coev, ev_coev_assoc, coev_def, coev_ev_assoc, coev_naturality_assoc, coev_naturality, coev_ev
comp 📖	CompOp	5 math math: comp_pushforward, pushforwardComp_hom_counit_assoc, pushforwardComp_hom_counit, unit_pushforwardComp_hom, unit_pushforwardComp_hom_assoc
ev 📖	CompOp	7 math math: ev_coev, ev_def, ev_coev_assoc, ev_naturality_assoc, coev_ev_assoc, ev_naturality, coev_ev
id 📖	CompOp	5 math math: id_pushforward, pushforwardId_hom_counit_assoc, unit_pushforwardId_hom, unit_pushforwardId_hom_assoc, pushforwardId_hom_counit
instChosenPullbacksAlongHomDiscretePUnitMk 📖	CompOp	—
pullbackPushforwardAdj 📖	CompOp	12 math math: homEquiv_symm_apply_eq, pushforwardId_hom_counit_assoc, ev_def, pushforwardComp_hom_counit_assoc, coev_def, pushforwardComp_hom_counit, unit_pushforwardId_hom, unit_pushforwardId_hom_assoc, unit_pushforwardComp_hom, pushforwardId_hom_counit, homEquiv_apply_eq, unit_pushforwardComp_hom_assoc
pushforward 📖	CompOp	22 math math: homEquiv_symm_apply_eq, id_pushforward, comp_pushforward, pushforwardId_hom_counit_assoc, ev_coev, ev_def, ev_coev_assoc, pushforwardComp_hom_counit_assoc, coev_def, ev_naturality_assoc, coev_ev_assoc, coev_naturality_assoc, pushforwardComp_hom_counit, coev_naturality, unit_pushforwardId_hom, unit_pushforwardId_hom_assoc, ev_naturality, unit_pushforwardComp_hom, pushforwardId_hom_counit, coev_ev, homEquiv_apply_eq, unit_pushforwardComp_hom_assoc
pushforwardComp 📖	CompOp	4 math math: pushforwardComp_hom_counit_assoc, pushforwardComp_hom_counit, unit_pushforwardComp_hom, unit_pushforwardComp_hom_assoc
pushforwardCurry 📖	CompOp	3 math math: pushforward_curry_uncurry, homEquiv_apply_eq, pushforward_uncurry_curry
pushforwardId 📖	CompOp	4 math math: pushforwardId_hom_counit_assoc, unit_pushforwardId_hom, unit_pushforwardId_hom_assoc, pushforwardId_hom_counit
pushforwardUncurry 📖	CompOp	3 math math: homEquiv_symm_apply_eq, pushforward_curry_uncurry, pushforward_uncurry_curry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coev_def 📖	mathematical	—	coev CategoryTheory.Adjunction.unit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.ChosenPullbacksAlong.pullback pushforward pullbackPushforwardAdj	—	—
coev_ev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id pushforward CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.NatTrans.app coev CategoryTheory.Functor.map ev CategoryTheory.CategoryStruct.id	—	CategoryTheory.Adjunction.right_triangle_components
coev_ev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj pushforward CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev CategoryTheory.Functor.map ev	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' coev_ev
coev_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.NatTrans.app CategoryTheory.Functor.id coev CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
coev_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj pushforward CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coev_naturality
comp_pushforward 📖	mathematical	—	pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver	—	—
ev_coev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.Functor.id CategoryTheory.Functor.comp pushforward CategoryTheory.Functor.map CategoryTheory.NatTrans.app coev ev CategoryTheory.CategoryStruct.id	—	CategoryTheory.Adjunction.left_triangle_components
ev_coev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev ev	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ev_coev
ev_def 📖	mathematical	—	ev CategoryTheory.Adjunction.counit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.ChosenPullbacksAlong.pullback pushforward pullbackPushforwardAdj	—	—
ev_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp ev	—	CategoryTheory.NatTrans.naturality
ev_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id ev	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ev_naturality
homEquiv_apply_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Over CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.pullback pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv pullbackPushforwardAdj pushforwardCurry	—	—
homEquiv_symm_apply_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Over CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj pushforward CategoryTheory.ChosenPullbacksAlong.pullback EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv pullbackPushforwardAdj pushforwardUncurry	—	—
id_pushforward 📖	mathematical	—	pushforward CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct id CategoryTheory.Functor.id CategoryTheory.Over CategoryTheory.instCategoryOver	—	—
isExponentiable 📖	mathematical	—	CategoryTheory.IsExponentiable	—	—
pushforwardComp_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pushforwardComp CategoryTheory.Adjunction.counit comp pullbackPushforwardAdj	—	pushforwardComp.eq_1 CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
pushforwardComp_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pushforwardComp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit comp pullbackPushforwardAdj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushforwardComp_hom_counit
pushforwardId_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.id CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pushforwardId CategoryTheory.Adjunction.counit id pullbackPushforwardAdj	—	pushforwardId.eq_1 CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
pushforwardId_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.id CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pushforwardId CategoryTheory.Adjunction.counit id pullbackPushforwardAdj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushforwardId_hom_counit
pushforward_curry_uncurry 📖	mathematical	—	pushforwardCurry pushforwardUncurry	—	Equiv.right_inv
pushforward_uncurry_curry 📖	mathematical	—	pushforwardUncurry pushforwardCurry	—	Equiv.left_inv
unit_pushforwardComp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.Adjunction.unit pullbackPushforwardAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pushforwardComp comp	—	pushforwardComp.eq_1 CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
unit_pushforwardComp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback pushforward CategoryTheory.Adjunction.unit pullbackPushforwardAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pushforwardComp comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_pushforwardComp_hom
unit_pushforwardId_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.CategoryStruct.id pushforward CategoryTheory.Adjunction.unit pullbackPushforwardAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pushforwardId id	—	pushforwardId.eq_1 CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
unit_pushforwardId_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ChosenPullbacksAlong.pullback CategoryTheory.CategoryStruct.id pushforward CategoryTheory.Adjunction.unit pullbackPushforwardAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pushforwardId id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_pushforwardId_hom

---

← Back to Index