Commit 2024-07-05 18:16 363b8176

View on Github →

feat(CategoryTheory/Bicategory): existence of Kan extensions (#10981) This PR introduces propositional type classes for the existence of left Kan extensions/lifts, mimicking HasColimit instance in the category theory library.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

added def CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint

added def CategoryTheory.Bicategory.Adjunction.ofIsRightAdjoint

added theorem CategoryTheory.Bicategory.IsLeftAdjoint.mk

added theorem CategoryTheory.Bicategory.IsRightAdjoint.mk

added structure CategoryTheory.Bicategory.LeftAdjoint

added structure CategoryTheory.Bicategory.RightAdjoint

added def CategoryTheory.Bicategory.getLeftAdjoint

added def CategoryTheory.Bicategory.getRightAdjoint

added def CategoryTheory.Bicategory.leftAdjoint

added def CategoryTheory.Bicategory.rightAdjoint

Modified Mathlib/CategoryTheory/Bicategory/Extension.lean

added def CategoryTheory.Bicategory.LeftExtension.ofCompId

modified theorem CategoryTheory.Bicategory.LeftExtension.w

added def CategoryTheory.Bicategory.LeftExtension.whiskerHom

modified def CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel

added def CategoryTheory.Bicategory.LeftExtension.whiskerIso

added def CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf

added def CategoryTheory.Bicategory.LeftLift.ofIdComp

modified theorem CategoryTheory.Bicategory.LeftLift.w

added def CategoryTheory.Bicategory.LeftLift.whiskerHom

modified def CategoryTheory.Bicategory.LeftLift.whiskerIdCancel

added def CategoryTheory.Bicategory.LeftLift.whiskerIso

added def CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf

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

modified def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction

modified def CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction

added theorem CategoryTheory.Bicategory.isLeftAdjoint_TFAE

added theorem CategoryTheory.Bicategory.isRightAdjoint_TFAE

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

added def CategoryTheory.Bicategory.Lan.CommuteWith.isKan

added def CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker

added def CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso

added def CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker

added theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right

added theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right

added theorem CategoryTheory.Bicategory.Lan.CommuteWith.of_isKan_whisker

added theorem CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_iso

added theorem CategoryTheory.Bicategory.Lan.existsUnique

added def CategoryTheory.Bicategory.LanLift.CommuteWith.isKan

added def CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker

added def CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso

added def CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker

added theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right

added theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right

added theorem CategoryTheory.Bicategory.LanLift.CommuteWith.of_isKan_whisker

added theorem CategoryTheory.Bicategory.LanLift.CommuteWith.of_lanLift_comp_iso

added theorem CategoryTheory.Bicategory.LanLift.existsUnique

added theorem CategoryTheory.Bicategory.LeftExtension.IsAbsKan.hasAbsLeftKanExtension

added theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension

added theorem CategoryTheory.Bicategory.LeftLift.IsAbsKan.hasAbsLeftKanLift

added theorem CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift

added def CategoryTheory.Bicategory.lan

added def CategoryTheory.Bicategory.lanDesc

added def CategoryTheory.Bicategory.lanIsKan

added theorem CategoryTheory.Bicategory.lanIsKan_desc

added def CategoryTheory.Bicategory.lanLeftExtension

added theorem CategoryTheory.Bicategory.lanLeftExtension_extension

added theorem CategoryTheory.Bicategory.lanLeftExtension_unit

added def CategoryTheory.Bicategory.lanLift

added def CategoryTheory.Bicategory.lanLiftDesc

added def CategoryTheory.Bicategory.lanLiftIsKan

added theorem CategoryTheory.Bicategory.lanLiftIsKan_desc

added def CategoryTheory.Bicategory.lanLiftLeftLift

added theorem CategoryTheory.Bicategory.lanLiftLeftLift_lift

added theorem CategoryTheory.Bicategory.lanLiftLeftLift_unit

added def CategoryTheory.Bicategory.lanLiftUnit

added theorem CategoryTheory.Bicategory.lanLiftUnit_desc

added def CategoryTheory.Bicategory.lanUnit

added theorem CategoryTheory.Bicategory.lanUnit_desc

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

added def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKan

added def CategoryTheory.Bicategory.LeftExtension.IsKan.ofCompId

added def CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan

added def CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso

added theorem CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_hom_right

added theorem CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_inv_right

added def CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommute

added def CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKan

added def CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp

added def CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan

added def CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso

added theorem CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_hom_right

added theorem CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_inv_right

added def CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommute

Modified Mathlib/CategoryTheory/Comma/Basic.lean

added def CategoryTheory.Comma.leftIso

added def CategoryTheory.Comma.rightIso