Comma

📁 Source: Mathlib/CategoryTheory/Adjunction/Comma.lean

Statistics

Metric	Count
Definitions adjunctionOfCostructuredArrowTerminals, adjunctionOfStructuredArrowInitials, leftAdjointOfStructuredArrowInitials, leftAdjointOfStructuredArrowInitialsAux, mkInitialOfLeftAdjoint, mkTerminalOfRightAdjoint, rightAdjointOfCostructuredArrowTerminals, rightAdjointOfCostructuredArrowTerminalsAux	8
Theorems isLeftAdjoint_iff_hasTerminal_costructuredArrow, isLeftAdjoint_of_costructuredArrowTerminals, isRightAdjointOfStructuredArrowInitials, isRightAdjoint_iff_hasInitial_structuredArrow, leftAdjointOfStructuredArrowInitialsAux_apply, leftAdjointOfStructuredArrowInitialsAux_symm_apply, rightAdjointOfCostructuredArrowTerminalsAux_apply, rightAdjointOfCostructuredArrowTerminalsAux_symm_apply	8
Total	16

CategoryTheory

Definitions

Name	Category	Theorems
adjunctionOfCostructuredArrowTerminals 📖	CompOp	—
adjunctionOfStructuredArrowInitials 📖	CompOp	—
leftAdjointOfStructuredArrowInitials 📖	CompOp	—
leftAdjointOfStructuredArrowInitialsAux 📖	CompOp	2 math math: leftAdjointOfStructuredArrowInitialsAux_apply, leftAdjointOfStructuredArrowInitialsAux_symm_apply
mkInitialOfLeftAdjoint 📖	CompOp	—
mkTerminalOfRightAdjoint 📖	CompOp	—
rightAdjointOfCostructuredArrowTerminals 📖	CompOp	—
rightAdjointOfCostructuredArrowTerminalsAux 📖	CompOp	2 math math: rightAdjointOfCostructuredArrowTerminalsAux_apply, rightAdjointOfCostructuredArrowTerminalsAux_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftAdjoint_iff_hasTerminal_costructuredArrow 📖	mathematical	—	Functor.IsLeftAdjoint Limits.HasTerminal CostructuredArrow instCategoryCostructuredArrow	—	Limits.IsTerminal.hasTerminal isLeftAdjoint_of_costructuredArrowTerminals
isLeftAdjoint_of_costructuredArrowTerminals 📖	mathematical	Limits.HasTerminal CostructuredArrow instCategoryCostructuredArrow	Functor.IsLeftAdjoint	—	—
isRightAdjointOfStructuredArrowInitials 📖	mathematical	Limits.HasInitial StructuredArrow instCategoryStructuredArrow	Functor.IsRightAdjoint	—	—
isRightAdjoint_iff_hasInitial_structuredArrow 📖	mathematical	—	Functor.IsRightAdjoint Limits.HasInitial StructuredArrow instCategoryStructuredArrow	—	Limits.IsInitial.hasInitial isRightAdjointOfStructuredArrowInitials
leftAdjointOfStructuredArrowInitialsAux_apply 📖	mathematical	Limits.HasInitial StructuredArrow instCategoryStructuredArrow	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Comma.right Discrete discreteCategory Functor.fromPUnit Limits.initial Functor.obj EquivLike.toFunLike Equiv.instEquivLike leftAdjointOfStructuredArrowInitialsAux CategoryStruct.comp Comma.hom Functor.map	—	—
leftAdjointOfStructuredArrowInitialsAux_symm_apply 📖	mathematical	Limits.HasInitial StructuredArrow instCategoryStructuredArrow	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj Comma.right Discrete discreteCategory Functor.fromPUnit Limits.initial EquivLike.toFunLike Equiv.instEquivLike Equiv.symm leftAdjointOfStructuredArrowInitialsAux CommaMorphism.right Limits.initial.to	—	—
rightAdjointOfCostructuredArrowTerminalsAux_apply 📖	mathematical	Limits.HasTerminal CostructuredArrow instCategoryCostructuredArrow	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj Comma.left Discrete discreteCategory Functor.fromPUnit Limits.terminal EquivLike.toFunLike Equiv.instEquivLike rightAdjointOfCostructuredArrowTerminalsAux CommaMorphism.left Limits.terminal.from	—	—
rightAdjointOfCostructuredArrowTerminalsAux_symm_apply 📖	mathematical	Limits.HasTerminal CostructuredArrow instCategoryCostructuredArrow	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Comma.left Discrete discreteCategory Functor.fromPUnit Limits.terminal Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm rightAdjointOfCostructuredArrowTerminalsAux CategoryStruct.comp Functor.map Comma.hom	—	—

---

← Back to Index