[Merged by Bors] - feat(CategoryTheory/Bicategory): define left Kan extensions

[yuma-mizuno]

The basic design follows the API for colimits in the category theory library.

The dictionary looks like:
Current PR
LeftExtension <-> Limits.Cocone
LeftExtension.IsKan <-> Limits.IsColimit
Future PR
LeftExtension.HasKan <-> Limits.HasColimit
lan <-> Limits.colimit

The diagrams in the docs are far from ideal, but I hope it helps for the time being. I would be very happy to have a graphical visualization by e.g. the widgets.

---

[joelriou]

With suitable imports, I would suggest using the existing limits API:

Suggested change

	structure IsKan (t : LeftExtension f g) where
	/-- The family of morphisms out of a left Kan extension. -/
	descHom : ∀ s : LeftExtension f g, t ⟶ s
	/-- The uniqueness of the family of morphisms out of a left Kan extension. -/
	uniq : ∀ (s : LeftExtension f g) (τ : t ⟶ s), τ = descHom s
	structure IsKan (t : LeftExtension f g) where
	/-- a left Kan extension is initial in `LeftExtension f g` -/
	isInitial : Limits.IsInitial t

[yuma-mizuno]

How about stating the equivalence to IsInitial as a lemma instead of putting in the default consructor?
The constructor of IsInitial (defined as a specific IsColimit) unfolds descHom into desc and fac, but I find in the current situation it's more convenient to bundle them when providing a term of IsKan t.

[joelriou]

As it seems to me that your definitions/lemmas are not at all specific to the category LeftExtension, I think the overall situation would be better if the general IsInitial API was improved instead, and then IsKan could be made an abbreviation of IsInitial. Indeed, I believe that for the future development of Kan extensions, it shall be convenient to use the Limits API, e.g. when two objects in LeftExtension are isomorphic, then one is initial iff the other is, etc. This should avoid some unnecessary duplication of code.

[yuma-mizuno]

I see. Maybe it is enough to just define abbrev IsKan (t : LeftExtension f g) := Limits.IsInitial t? I will try it.

[joelriou]

If we introduce the whiskering functors, the category LeftExtension identifies to a suitable category StructuredArrow. Recent PRs by @TwoFX like #6248 contain useful results about these categories. I know that this type of results about (Co)structuredArrow categories will be very useful when proving things about Kan extensions (e.g. total derived functors for which I have done some experiments). Then, again, in order to avoid duplication of code, it would be great to base the definition of Left/RightExtension using this so that we can later use the existing and future developments of the StructuredArrow API. Still, you may introduce more convenient specialized abbreviations like "LeftExtension.extension" or "LeftExtension.unit" instead of Comma.right and Comma.hom.

@[simps]
def whiskeringLeft (a b c : B) : (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c) where
  obj f :=
    { obj := fun e => f ≫ e
      map := fun φ => f ◁ φ }
  map ψ :=
    { app := fun e => ψ ▷ e
      naturality := fun {e₁ e₂} φ => whisker_exchange _ _ }

def LeftExtension (f : a ⟶ b) (g : a ⟶ c) :=
  StructuredArrow g ((whiskeringLeft a b c).obj f)

[yuma-mizuno]

This looks great! I think we need to develop an API for the initial object of StructuredArrow first. Does mathlib already have this?

(It should be similar to the colimit API, which would suggest the possibility of refactoring the colimit files.)

[joelriou]

I think that this design is good. As you have developed the API for both StructuredArrow and CostructuredArrow, I believe you may also add the dual definition RightExtension.IsKan.

[joelriou]

Thanks!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style