Adjunction

📁 Source: Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

Statistics

Metric	Count
Definitions Adjunction, isAbsoluteLeftKan, isAbsoluteLeftKanLift, adjunction, adjunction, isKanOfWhiskerLeftAdjoint, adjunction, adjunction	8
Theorems instCommuteWithOfIsLeftAdjoint, isLeftAdjoint_TFAE, isRightAdjoint_TFAE	3
Total	11

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
Adjunction 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftAdjoint_TFAE 📖	mathematical	—	List.TFAE IsLeftAdjoint HasAbsLeftKanExtension CategoryTheory.CategoryStruct.id toCategoryStruct HasLeftKanExtension Lan.CommuteWith	—	LeftExtension.IsAbsKan.hasAbsLeftKanExtension HasAbsLeftKanExtension.toHasLeftKanExtension instCommuteWith List.tfae_of_cycle
isRightAdjoint_TFAE 📖	mathematical	—	List.TFAE IsRightAdjoint HasAbsLeftKanLift CategoryTheory.CategoryStruct.id toCategoryStruct HasLeftKanLift LanLift.CommuteWith	—	LeftLift.IsAbsKan.hasAbsLeftKanLift HasAbsLeftKanLift.toHasLeftKanLift instCommuteWith_1 List.tfae_of_cycle

CategoryTheory.Bicategory.Adjunction

Definitions

Name	Category	Theorems
isAbsoluteLeftKan 📖	CompOp	—
isAbsoluteLeftKanLift 📖	CompOp	—

CategoryTheory.Bicategory.LeftExtension

Definitions

Name	Category	Theorems
isKanOfWhiskerLeftAdjoint 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCommuteWithOfIsLeftAdjoint 📖	mathematical	—	CategoryTheory.Bicategory.Lan.CommuteWith	—	—

CategoryTheory.Bicategory.LeftExtension.IsAbsKan

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—

CategoryTheory.Bicategory.LeftExtension.IsKan

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—

CategoryTheory.Bicategory.LeftLift.IsAbsKan

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—

CategoryTheory.Bicategory.LeftLift.IsKan

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—

---

← Back to Index