Commit 2024-02-14 11:28 73913b69

View on Github →

feat(CategoryTheory/Bicategory): adjunctions as Kan extensions (#10045) We also show that a left adjoint commutes with left Kan extensions.

depends on: #10178

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/Extension.lean

modified def CategoryTheory.Bicategory.LeftExtension.alongId

added theorem CategoryTheory.Bicategory.LeftExtension.w

added def CategoryTheory.Bicategory.LeftExtension.whisker

added def CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel

added theorem CategoryTheory.Bicategory.LeftExtension.whisker_extension

added theorem CategoryTheory.Bicategory.LeftExtension.whisker_unit

added def CategoryTheory.Bicategory.LeftExtension.whiskering

modified def CategoryTheory.Bicategory.LeftLift.alongId

added theorem CategoryTheory.Bicategory.LeftLift.w

added def CategoryTheory.Bicategory.LeftLift.whisker

added def CategoryTheory.Bicategory.LeftLift.whiskerIdCancel

added theorem CategoryTheory.Bicategory.LeftLift.whisker_lift

added theorem CategoryTheory.Bicategory.LeftLift.whisker_unit

added def CategoryTheory.Bicategory.LeftLift.whiskering

modified def CategoryTheory.Bicategory.RightExtension.alongId

added theorem CategoryTheory.Bicategory.RightExtension.w

modified def CategoryTheory.Bicategory.RightLift.alongId

added theorem CategoryTheory.Bicategory.RightLift.w

Created Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

added def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKan

added def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKanLift

added def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction

added def CategoryTheory.Bicategory.LeftExtension.IsKan.adjunction

added def CategoryTheory.Bicategory.LeftExtension.isKanOfWhiskerLeftAdjoint

added def CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction

added def CategoryTheory.Bicategory.LeftLift.IsKan.adjunction

Modified Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean

added def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.isKan

added theorem CategoryTheory.Bicategory.LeftExtension.IsKan.fac

added theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext

added def CategoryTheory.Bicategory.LeftLift.IsAbsKan.isKan

added theorem CategoryTheory.Bicategory.LeftLift.IsKan.fac

added theorem CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext