PartialAdjoint

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

Statistics

Metric	Count
Definitions PartialLeftAdjointSource, PartialRightAdjointSource, corepresentableByCompCoyonedaObjOfIsColimit, leftAdjointObjIsDefined, partialLeftAdjoint, partialLeftAdjointHomEquiv, partialLeftAdjointMap, partialLeftAdjointObj, partialRightAdjoint, partialRightAdjointHomEquiv, partialRightAdjointMap, partialRightAdjointObj, representableByCompYonedaObjOfIsLimit, rightAdjointObjIsDefined	14
Theorems instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined, instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined, isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top, isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top, leftAdjointObjIsDefined_colimit, leftAdjointObjIsDefined_iff, leftAdjointObjIsDefined_of_adjunction, leftAdjointObjIsDefined_of_isColimit, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_comp_symm, partialLeftAdjointHomEquiv_comp_symm_assoc, partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_map_comp, partialLeftAdjointHomEquiv_symm_comp, partialLeftAdjointHomEquiv_symm_comp_assoc, partialLeftAdjoint_map, partialLeftAdjoint_obj, partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_comp_symm, partialRightAdjointHomEquiv_comp_symm_assoc, partialRightAdjointHomEquiv_map, partialRightAdjointHomEquiv_map_comp, partialRightAdjointHomEquiv_symm_comp, partialRightAdjointHomEquiv_symm_comp_assoc, partialRightAdjoint_map, partialRightAdjoint_obj, rightAdjointObjIsDefined_iff, rightAdjointObjIsDefined_limit, rightAdjointObjIsDefined_of_adjunction, rightAdjointObjIsDefined_of_isLimit	32
Total	46

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PartialLeftAdjointSource 📖	CompOp	2 math math: partialLeftAdjoint_obj, partialLeftAdjoint_map
PartialRightAdjointSource 📖	CompOp	2 math math: partialRightAdjoint_obj, partialRightAdjoint_map
corepresentableByCompCoyonedaObjOfIsColimit 📖	CompOp	—
leftAdjointObjIsDefined 📖	CompOp	13 math math: partialLeftAdjointHomEquiv_comp_symm_assoc, partialLeftAdjointHomEquiv_symm_comp, leftAdjointObjIsDefined_of_adjunction, partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_map_comp, instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined, partialLeftAdjoint_obj, partialLeftAdjointHomEquiv_symm_comp_assoc, isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_comp_symm, leftAdjointObjIsDefined_iff, partialLeftAdjoint_map
partialLeftAdjoint 📖	CompOp	2 math math: partialLeftAdjoint_obj, partialLeftAdjoint_map
partialLeftAdjointHomEquiv 📖	CompOp	7 math math: partialLeftAdjointHomEquiv_comp_symm_assoc, partialLeftAdjointHomEquiv_symm_comp, partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_map_comp, partialLeftAdjointHomEquiv_symm_comp_assoc, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_comp_symm
partialLeftAdjointMap 📖	CompOp	5 math math: partialLeftAdjointHomEquiv_comp_symm_assoc, partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_map_comp, partialLeftAdjointHomEquiv_comp_symm, partialLeftAdjoint_map
partialLeftAdjointObj 📖	CompOp	8 math math: partialLeftAdjointHomEquiv_comp_symm_assoc, partialLeftAdjointHomEquiv_symm_comp, partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_map_comp, partialLeftAdjoint_obj, partialLeftAdjointHomEquiv_symm_comp_assoc, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_comp_symm
partialRightAdjoint 📖	CompOp	2 math math: partialRightAdjoint_obj, partialRightAdjoint_map
partialRightAdjointHomEquiv 📖	CompOp	7 math math: partialRightAdjointHomEquiv_comp_symm, partialRightAdjointHomEquiv_symm_comp, partialRightAdjointHomEquiv_comp_symm_assoc, partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map, partialRightAdjointHomEquiv_symm_comp_assoc, partialRightAdjointHomEquiv_map_comp
partialRightAdjointMap 📖	CompOp	5 math math: partialRightAdjointHomEquiv_symm_comp, partialRightAdjointHomEquiv_map, partialRightAdjoint_map, partialRightAdjointHomEquiv_symm_comp_assoc, partialRightAdjointHomEquiv_map_comp
partialRightAdjointObj 📖	CompOp	8 math math: partialRightAdjointHomEquiv_comp_symm, partialRightAdjointHomEquiv_symm_comp, partialRightAdjointHomEquiv_comp_symm_assoc, partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map, partialRightAdjoint_obj, partialRightAdjointHomEquiv_symm_comp_assoc, partialRightAdjointHomEquiv_map_comp
representableByCompYonedaObjOfIsLimit 📖	CompOp	—
rightAdjointObjIsDefined 📖	CompOp	13 math math: partialRightAdjointHomEquiv_comp_symm, partialRightAdjointHomEquiv_symm_comp, rightAdjointObjIsDefined_iff, partialRightAdjointHomEquiv_comp_symm_assoc, isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top, partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map, partialRightAdjoint_obj, instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined, partialRightAdjoint_map, rightAdjointObjIsDefined_of_adjunction, partialRightAdjointHomEquiv_symm_comp_assoc, partialRightAdjointHomEquiv_map_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined 📖	mathematical	—	IsCorepresentable comp CategoryTheory.types obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category CategoryTheory.coyoneda Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined 📖	mathematical	—	IsRepresentable comp Opposite CategoryTheory.Category.opposite CategoryTheory.types op obj CategoryTheory.Functor category CategoryTheory.yoneda CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined	—	CategoryTheory.ObjectProperty.FullSubcategory.property
isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top 📖	mathematical	—	IsLeftAdjoint rightAdjointObjIsDefined Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	rightAdjointObjIsDefined_of_adjunction isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top
isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top 📖	mathematical	rightAdjointObjIsDefined Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	IsLeftAdjoint	—	CategoryTheory.Adjunction.isLeftAdjoint RepresentableBy.comp_homEquiv_symm
isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top 📖	mathematical	—	IsRightAdjoint leftAdjointObjIsDefined Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	leftAdjointObjIsDefined_of_adjunction isRightAdjoint_of_leftAdjointObjIsDefined_eq_top
isRightAdjoint_of_leftAdjointObjIsDefined_eq_top 📖	mathematical	leftAdjointObjIsDefined Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	IsRightAdjoint	—	CategoryTheory.Adjunction.isRightAdjoint CorepresentableBy.homEquiv_comp
leftAdjointObjIsDefined_colimit 📖	mathematical	leftAdjointObjIsDefined obj	CategoryTheory.Limits.colimit	—	leftAdjointObjIsDefined_of_isColimit
leftAdjointObjIsDefined_iff 📖	mathematical	—	leftAdjointObjIsDefined IsCorepresentable comp CategoryTheory.types obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category CategoryTheory.coyoneda Opposite.op	—	—
leftAdjointObjIsDefined_of_adjunction 📖	mathematical	—	leftAdjointObjIsDefined	—	CorepresentableBy.isCorepresentable
leftAdjointObjIsDefined_of_isColimit 📖	mathematical	leftAdjointObjIsDefined obj	CategoryTheory.Limits.Cocone.pt	—	CorepresentableBy.isCorepresentable CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
partialLeftAdjointHomEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike partialLeftAdjointHomEquiv CategoryTheory.CategoryStruct.comp map	—	CorepresentableBy.homEquiv_comp instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined
partialLeftAdjointHomEquiv_comp_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj partialLeftAdjointMap DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialLeftAdjointHomEquiv CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	Equiv.eq_symm_apply partialLeftAdjointHomEquiv_comp partialLeftAdjointHomEquiv_map CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Equiv.apply_symm_apply
partialLeftAdjointHomEquiv_comp_symm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj partialLeftAdjointMap DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialLeftAdjointHomEquiv CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' partialLeftAdjointHomEquiv_comp_symm
partialLeftAdjointHomEquiv_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike partialLeftAdjointHomEquiv partialLeftAdjointMap CategoryTheory.CategoryStruct.comp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id	—	Equiv.apply_symm_apply
partialLeftAdjointHomEquiv_map_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike partialLeftAdjointHomEquiv CategoryTheory.CategoryStruct.comp partialLeftAdjointMap CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	partialLeftAdjointHomEquiv_comp partialLeftAdjointHomEquiv_map CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
partialLeftAdjointHomEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialLeftAdjointHomEquiv map	—	CorepresentableBy.homEquiv_symm_comp instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined
partialLeftAdjointHomEquiv_symm_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialLeftAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ObjectProperty.FullSubcategory.obj leftAdjointObjIsDefined obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialLeftAdjointHomEquiv map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' partialLeftAdjointHomEquiv_symm_comp
partialLeftAdjoint_map 📖	mathematical	—	map PartialLeftAdjointSource CategoryTheory.ObjectProperty.FullSubcategory.category leftAdjointObjIsDefined partialLeftAdjoint partialLeftAdjointMap	—	—
partialLeftAdjoint_obj 📖	mathematical	—	obj PartialLeftAdjointSource CategoryTheory.ObjectProperty.FullSubcategory.category leftAdjointObjIsDefined partialLeftAdjoint partialLeftAdjointObj	—	—
partialRightAdjointHomEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialRightAdjointObj obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike partialRightAdjointHomEquiv CategoryTheory.CategoryStruct.comp map	—	RepresentableBy.homEquiv_comp instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined
partialRightAdjointHomEquiv_comp_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialRightAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialRightAdjointHomEquiv map	—	RepresentableBy.comp_homEquiv_symm instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined
partialRightAdjointHomEquiv_comp_symm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialRightAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialRightAdjointHomEquiv map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' partialRightAdjointHomEquiv_comp_symm
partialRightAdjointHomEquiv_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialRightAdjointObj obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike partialRightAdjointHomEquiv partialRightAdjointMap CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	Equiv.apply_symm_apply
partialRightAdjointHomEquiv_map_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct partialRightAdjointObj obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike partialRightAdjointHomEquiv CategoryTheory.CategoryStruct.comp partialRightAdjointMap CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	partialRightAdjointHomEquiv_comp partialRightAdjointHomEquiv_map CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
partialRightAdjointHomEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialRightAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialRightAdjointHomEquiv partialRightAdjointMap CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	partialRightAdjointHomEquiv_map_comp Equiv.apply_symm_apply
partialRightAdjointHomEquiv_symm_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct partialRightAdjointObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver obj CategoryTheory.ObjectProperty.FullSubcategory.obj rightAdjointObjIsDefined EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partialRightAdjointHomEquiv partialRightAdjointMap CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' partialRightAdjointHomEquiv_symm_comp
partialRightAdjoint_map 📖	mathematical	—	map PartialRightAdjointSource CategoryTheory.ObjectProperty.FullSubcategory.category rightAdjointObjIsDefined partialRightAdjoint partialRightAdjointMap	—	—
partialRightAdjoint_obj 📖	mathematical	—	obj PartialRightAdjointSource CategoryTheory.ObjectProperty.FullSubcategory.category rightAdjointObjIsDefined partialRightAdjoint partialRightAdjointObj	—	—
rightAdjointObjIsDefined_iff 📖	mathematical	—	rightAdjointObjIsDefined IsRepresentable comp Opposite CategoryTheory.Category.opposite CategoryTheory.types op obj CategoryTheory.Functor category CategoryTheory.yoneda	—	—
rightAdjointObjIsDefined_limit 📖	mathematical	rightAdjointObjIsDefined obj	CategoryTheory.Limits.limit	—	rightAdjointObjIsDefined_of_isLimit
rightAdjointObjIsDefined_of_adjunction 📖	mathematical	—	rightAdjointObjIsDefined	—	RepresentableBy.isRepresentable
rightAdjointObjIsDefined_of_isLimit 📖	mathematical	rightAdjointObjIsDefined obj	CategoryTheory.Limits.Cone.pt	—	RepresentableBy.isRepresentable CategoryTheory.Limits.hasLimitOfHasLimitsOfShape

---

← Back to Index