Commit 2026-10-20 15:02 707d52d6

View on Github →

feat(CategoryTheory): kan extensions from isos (#41484) This PR constructs lifts out of isomorphisms of 1-cells, and shows that being (abs) Kan is preserved by this. This is done for all four notions of left/right lifts/extensions. This is needed for the oo-cosmos project.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Extension.lean

added def CategoryTheory.Bicategory.LeftExtension.mapIso

added theorem CategoryTheory.Bicategory.LeftExtension.ofIso_extension

added theorem CategoryTheory.Bicategory.LeftExtension.ofIso_unit

added def CategoryTheory.Bicategory.LeftExtension.whiskerOfIso

added def CategoryTheory.Bicategory.LeftLift.mapIso

added theorem CategoryTheory.Bicategory.LeftLift.ofIso_lift

added theorem CategoryTheory.Bicategory.LeftLift.ofIso_unit

modified theorem CategoryTheory.Bicategory.LeftLift.w

added def CategoryTheory.Bicategory.LeftLift.whiskerOfIso

added def CategoryTheory.Bicategory.RightExtension.mapIso

added def CategoryTheory.Bicategory.RightExtension.ofCompId

added theorem CategoryTheory.Bicategory.RightExtension.ofIso_counit

added theorem CategoryTheory.Bicategory.RightExtension.ofIso_extension

modified theorem CategoryTheory.Bicategory.RightExtension.w

added def CategoryTheory.Bicategory.RightExtension.whisker

added def CategoryTheory.Bicategory.RightExtension.whiskerHom

added def CategoryTheory.Bicategory.RightExtension.whiskerIdCancel

added def CategoryTheory.Bicategory.RightExtension.whiskerIso

added def CategoryTheory.Bicategory.RightExtension.whiskerOfCompIdIsoSelf

added def CategoryTheory.Bicategory.RightExtension.whiskerOfIso

added theorem CategoryTheory.Bicategory.RightExtension.whisker_counit

added theorem CategoryTheory.Bicategory.RightExtension.whisker_extension

added def CategoryTheory.Bicategory.RightExtension.whiskering

added def CategoryTheory.Bicategory.RightLift.mapIso

added theorem CategoryTheory.Bicategory.RightLift.ofIso_counit

added theorem CategoryTheory.Bicategory.RightLift.ofIso_lift

modified theorem CategoryTheory.Bicategory.RightLift.w

added def CategoryTheory.Bicategory.RightLift.whiskerOfIso

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

added def CategoryTheory.Bicategory.RightExtension.IsAbsKan.isKan

added def CategoryTheory.Bicategory.RightExtension.IsAbsKan.ofIsoAbsKan

added theorem CategoryTheory.Bicategory.RightExtension.IsKan.fac

added theorem CategoryTheory.Bicategory.RightExtension.IsKan.hom_ext

added def CategoryTheory.Bicategory.RightExtension.IsKan.ofCompId

added def CategoryTheory.Bicategory.RightExtension.IsKan.ofIsoKan

added def CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso

added theorem CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_hom_left

added theorem CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_inv_left

added def CategoryTheory.Bicategory.RightExtension.IsKan.whiskerOfCommute