Cartesian

📁 Source: Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean

Statistics

Metric	Count
Definitions `curry`, `delabFunctorObjExp`, `mk`, `uncurry`, `«term_^^_»`, `«term_⟹_»`, `Exponentiable`, `mk`, `binaryProductExponentiable`, `cartesianClosedOfEquiv`, `exp`, `adjunction`, `coev`, `ev`, `expUnitIsoSelf`, `expUnitNatIso`, `internalHom`, `internalizeHom`, `mulZero`, `powZero`, `pre`, `prodCoprodDistrib`, `terminalExponentiable`, `zeroMul`	24
Theorems `curry_eq`, `curry_eq_iff`, `curry_id_eq_coev`, `curry_injective`, `curry_natural_left`, `curry_natural_left_assoc`, `curry_natural_right`, `curry_natural_right_assoc`, `curry_uncurry`, `eq_curry_iff`, `homEquiv_apply_eq`, `homEquiv_symm_apply_eq`, `uncurry_curry`, `uncurry_eq`, `uncurry_id_eq_ev`, `uncurry_injective`, `uncurry_natural_left`, `uncurry_natural_left_assoc`, `uncurry_natural_right`, `uncurry_natural_right_assoc`, `isLeftAdjoint_prod_functor`, `mono_to`, `coev_app_comp_pre_app`, `coev_ev`, `coev_ev_assoc`, `ev_coev`, `ev_coev_assoc`, `initial_mono`, `pre_id`, `pre_map`, `prod_map_pre_app_comp_ev`, `strict_initial`, `to_initial_isIso`, `uncurry_pre`, `zeroMul_hom`, `zeroMul_inv`	36
Total	60

CategoryTheory

Definitions

Name	Category	Theorems
`Exponentiable` 📖	CompOp	—
`binaryProductExponentiable` 📖	CompOp	—
`cartesianClosedOfEquiv` 📖	CompOp	—
`exp` 📖	CompOp	—
`expUnitIsoSelf` 📖	CompOp	—
`expUnitNatIso` 📖	CompOp	—
`internalHom` 📖	CompOp	—
`internalizeHom` 📖	CompOp	—
`mulZero` 📖	CompOp	—
`powZero` 📖	CompOp	—
`pre` 📖	CompOp	—
`prodCoprodDistrib` 📖	CompOp	—
`terminalExponentiable` 📖	CompOp	—
`zeroMul` 📖	CompOp	2 math math: `zeroMul_hom`, `zeroMul_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coev_app_comp_pre_app` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.comp` `MonoidalCategory.tensorLeft` `ihom` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `NatTrans.app` `ihom.coev` `MonoidalClosed.pre` `Functor.map` `MonoidalCategoryStruct.whiskerRight`	—	`MonoidalClosed.coev_app_comp_pre_app`
`initial_mono` 📖	mathematical	—	`Mono` `Limits.IsInitial.to`	—	`eq_of_inv_eq_inv` `strict_initial` `Limits.IsInitial.hom_ext`
`pre_id` 📖	mathematical	—	`MonoidalClosed.pre` `CategoryStruct.id` `Category.toCategoryStruct` `Functor` `Functor.category` `ihom`	—	`MonoidalClosed.pre_id`
`pre_map` 📖	mathematical	—	`MonoidalClosed.pre` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor` `Functor.category` `ihom`	—	`MonoidalClosed.pre_map`
`prod_map_pre_app_comp_ev` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `Functor.obj` `ihom` `Functor.id` `MonoidalCategoryStruct.whiskerLeft` `NatTrans.app` `MonoidalClosed.pre` `Functor.comp` `MonoidalCategory.tensorLeft` `ihom.ev` `MonoidalCategoryStruct.whiskerRight`	—	`MonoidalClosed.id_tensor_pre_app_comp_ev`
`strict_initial` 📖	mathematical	—	`IsIso`	—	`isIso_of_mono_of_isSplitEpi` `CartesianMonoidalCategory.lift_snd` `zeroMul_hom` `mono_comp` `CartesianMonoidalCategory.mono_lift_of_mono_left` `instMonoId` `mono_of_strongMono` `strongMono_of_isIso` `Iso.isIso_hom` `IsSplitEpi.mk'` `Limits.IsInitial.hom_ext`
`to_initial_isIso` 📖	mathematical	—	`IsIso` `Limits.initial`	—	`strict_initial`
`uncurry_pre` 📖	mathematical	—	`MonoidalClosed.uncurry` `Functor.obj` `ihom` `NatTrans.app` `MonoidalClosed.pre` `CategoryStruct.comp` `Category.toCategoryStruct` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `Functor.id` `MonoidalCategoryStruct.whiskerRight` `Functor.comp` `MonoidalCategory.tensorLeft` `ihom.ev`	—	`MonoidalClosed.uncurry_pre`
`zeroMul_hom` 📖	mathematical	—	`Iso.hom` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `zeroMul` `SemiCartesianMonoidalCategory.snd`	—	—
`zeroMul_inv` 📖	mathematical	—	`Iso.inv` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `zeroMul` `Limits.IsInitial.to`	—	—

CategoryTheory.CartesianClosed

Definitions

Name	Category	Theorems
`curry` 📖	CompOp	—
`delabFunctorObjExp` 📖	CompOp	—
`mk` 📖	CompOp	—
`uncurry` 📖	CompOp	—
`«term_^^_»` 📖	CompOp	—
`«term_⟹_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curry_eq` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.ihom` `CategoryTheory.NatTrans.app` `CategoryTheory.ihom.coev` `CategoryTheory.Functor.map`	—	`CategoryTheory.MonoidalClosed.curry_eq`
`curry_eq_iff` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalClosed.uncurry`	—	`CategoryTheory.MonoidalClosed.curry_eq_iff`
`curry_id_eq_coev` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.ihom` `CategoryTheory.ihom.coev`	—	`CategoryTheory.MonoidalClosed.curry_id_eq_coev`
`curry_injective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.curry`	—	`CategoryTheory.MonoidalClosed.curry_injective`
`curry_natural_left` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Functor.obj` `CategoryTheory.ihom`	—	`CategoryTheory.MonoidalClosed.curry_natural_left`
`curry_natural_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`CategoryTheory.MonoidalClosed.curry_natural_left_assoc`
`curry_natural_right` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.Functor.map`	—	`CategoryTheory.MonoidalClosed.curry_natural_right`
`curry_natural_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.map`	—	`CategoryTheory.MonoidalClosed.curry_natural_right_assoc`
`curry_uncurry` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalClosed.uncurry`	—	`CategoryTheory.MonoidalClosed.curry_uncurry`
`eq_curry_iff` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalClosed.uncurry`	—	`CategoryTheory.MonoidalClosed.eq_curry_iff`
`homEquiv_apply_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.ihom` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.ihom.adjunction` `CategoryTheory.MonoidalClosed.curry`	—	`CategoryTheory.MonoidalClosed.homEquiv_apply_eq`
`homEquiv_symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategory.tensorLeft` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.ihom.adjunction` `CategoryTheory.MonoidalClosed.uncurry`	—	`CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq`
`uncurry_curry` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.MonoidalClosed.curry`	—	`CategoryTheory.MonoidalClosed.uncurry_curry`
`uncurry_eq` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.Functor.id` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.ihom.ev`	—	`CategoryTheory.MonoidalClosed.uncurry_eq`
`uncurry_id_eq_ev` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.Functor.id` `CategoryTheory.ihom.ev`	—	`CategoryTheory.MonoidalClosed.uncurry_id_eq_ev`
`uncurry_injective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalClosed.uncurry`	—	`CategoryTheory.MonoidalClosed.uncurry_injective`
`uncurry_natural_left` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`CategoryTheory.MonoidalClosed.uncurry_natural_left`
`uncurry_natural_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc`
`uncurry_natural_right` 📖	mathematical	—	`CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	`CategoryTheory.MonoidalClosed.uncurry_natural_right`
`uncurry_natural_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.Functor.map`	—	`CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc`

CategoryTheory.CartesianMonoidalCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftAdjoint_prod_functor` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.prod.functor` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `instHasFiniteProducts` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair`	—	`CategoryTheory.Functor.isLeftAdjoint_of_iso` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `instHasFiniteProducts` `Finite.of_fintype` `CategoryTheory.ihom.instIsLeftAdjointTensorLeft`

CategoryTheory.Exponentiable

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

CategoryTheory.Initial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono_to` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Limits.initial` `CategoryTheory.Limits.initial.to`	—	`CategoryTheory.initial_mono`

CategoryTheory.exp

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	—
`coev` 📖	CompOp	—
`ev` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coev_ev` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.ihom` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.NatTrans.app` `CategoryTheory.ihom.coev` `CategoryTheory.Functor.map` `CategoryTheory.ihom.ev` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ihom.coev_ev`
`coev_ev_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.ihom.coev` `CategoryTheory.Functor.map` `CategoryTheory.ihom.ev`	—	`CategoryTheory.ihom.coev_ev_assoc`
`ev_coev` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.NatTrans.app` `CategoryTheory.ihom.coev` `CategoryTheory.ihom.ev` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ihom.ev_coev`
`ev_coev_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.ihom.coev` `CategoryTheory.ihom.ev`	—	`CategoryTheory.ihom.ev_coev_assoc`

---

← Back to Index