Zulip Chat Archive

Stream: Lean Together 2025

Topic: Emily Riehl: The infty-cosmos project

Emily Riehl (Jan 14 2025 at 15:46):

I've posted my slides here.

Johan Commelin (Jan 14 2025 at 15:47):

Looking forward to your talk!

Johan Commelin (Jan 14 2025 at 16:29):

I think at some point we also really need an interactive widget for displaying these pasting diagrams and doing proofs with them.

Johan Commelin (Jan 14 2025 at 16:30):

In particular, the readability of the proof without the widget should then maybe be less of a concern, and could contain metadata for replaying the proof in the widget.

Johan Commelin (Jan 14 2025 at 16:30):

But this is all just a dream atm.

Dagur Asgeirsson (Jan 14 2025 at 16:31):

Here are the category theory exercises I was referring to: https://github.com/adamtopaz/CopenhagenMasterclass2023/tree/master/CategoryTheoryExercises

Emily Riehl (Jan 14 2025 at 16:34):

I wrote a message to @Rob Lewis over the summer describing some automation I'd love to see for proving pasting equalities in 2-categories. I have no idea what is feasable.

Examples of proofs that should be achievable in this way can be found in the Mates file in Mathlib. In the talk I referred to mateEquiv_vcomp.

Section B.1 of this https://emilyriehl.github.io/files/elements.pdf explains what is going on from a 2-categorical point of view, like we explored today. But more basically, if α : F -> G is a natural transformation the naturality implies you can do a rewrite whenever you see something of the form F _ >> α _ or something of the form α _ >> G _ (where the functors are in application order but the composition is in diagrammatic order). A right whiskering of α by a functor H is a natural transformation of the form Hα : HF -> HG (application order again), so now we can use naturality whenever we see HF _ >> Hα or Hα >> ΗG _. Right now you have to first rewrite to move the H outside the composite, which is one of the things that should be automated. You also have to do some rewriting if any of H F and G are composites of other functors. The mates file contains lots of examples of this.

Rob Lewis (Jan 14 2025 at 17:06):

Emily Riehl said:

I wrote a message to @Rob Lewis over the summer describing some automation I'd love to see for proving pasting equalities in 2-categories. I have no idea what is feasable.

I have some notes somewhere from our conversation about this in Bonn! It's not fresh in my mind, so sorry if this is wrong/vague, but I sort of remember wondering if we could treat this as a normalization tactic/how we'd describe the normal form of these expressions?

Yuma Mizuno (Jan 14 2025 at 17:13):

I'm interested in the 2-category challenge in the talk, since I have done some formalizations of adjunctions in bicategoryes before.

The 2-category challenge in lean (with a sorry proof) is like this:

import Mathlib.CategoryTheory.Bicategory.Adjunction
import Mathlib.Tactic.Widget.StringDiagram

universe w v u

namespace CategoryTheory

namespace Bicategory

open Bicategory

variable {B : Type u} [Bicategory.{w, v} B]

section mateEquiv

variable {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c} {l₂ : e ⟶ f} {r₂ : f ⟶ e}
variable (adj₁ : l₁ ⊣ r₁) (adj₂ : l₂ ⊣ r₂)

@[simps]
def mateEquiv : (g ≫ l₂ ⟶ l₁ ≫ h) ≃ (r₁ ≫ g ⟶ h ≫ r₂) where
  toFun α :=
    𝟙 _ ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 _
  invFun β :=
    𝟙 _ ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 _
  left_inv α := by sorry
  right_inv β := by sorry

end mateEquiv

variable {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d} {h₂ : d ⟶ f}
variable {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} {l₃ : e ⟶ f} {r₃ : f ⟶ e}
variable (adj₁ : l₁ ⊣ r₁) (adj₂ : l₂ ⊣ r₂) (adj₃ : l₃ ⊣ r₃)

def leftAdjointSquare.vcomp (α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁) (β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂) :
    ((g₁ ≫ g₂) ≫ l₃ ⟶ l₁ ≫ h₁ ≫ h₂) :=
  (α_ _ _ _).hom ≫ g₁ ◁ β ≫ (α_ _ _ _).inv ≫ α ▷ h₂ ≫ (α_ _ _ _).hom

def rightAdjointSquare.vcomp (α : r₁ ≫ g₁ ⟶ h₁ ≫ r₂) (β : r₂ ≫ g₂ ⟶ h₂ ≫ r₃) :
    (r₁ ≫ (g₁ ≫ g₂) ⟶ (h₁ ≫ h₂) ≫ r₃) :=
  (α_ _ _ _).inv ≫ α ▷ g₂ ≫ (α_ _ _ _).hom ≫ h₁ ◁ β ≫ (α_ _ _ _).inv

theorem mateEquiv_vcomp (α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁) (β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂) :
    (mateEquiv (g := g₁ ≫ g₂) (h := h₁ ≫ h₂) adj₁ adj₃) (leftAdjointSquare.vcomp α β) =
      rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ β) := by
  dsimp only [leftAdjointSquare.vcomp, mateEquiv_apply, rightAdjointSquare.vcomp]
  -- This allow us to see string diagrams in the tactic state
  with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram]
    sorry

end Bicategory

end CategoryTheory

Jireh Loreaux (Jan 14 2025 at 17:14):

This is not exactly the same topic, but I recently saw this paper about diagram chasing in abelian categories. Apologies if this was already mentioned elsewhere, as I had to miss the talk due to my teaching schedule.

Emily Riehl (Jan 14 2025 at 18:40):

@Yuma Mizuno thanks for setting this up. It would be great if everything in the Mates file were generalized in this way.

Emily Riehl (Jan 14 2025 at 18:40):

Jireh Loreaux said:

This is not exactly the same topic, but I recently saw this paper about diagram chasing in abelian categories. Apologies if this was already mentioned elsewhere, as I had to miss the talk due to my teaching schedule.

Thanks. I'm not familiar with this paper but am happy to know about it!

Emily Riehl (Jan 14 2025 at 18:48):

Rob Lewis said:

Emily Riehl said:

I wrote a message to @Rob Lewis over the summer describing some automation I'd love to see for proving pasting equalities in 2-categories. I have no idea what is feasable.

I have some notes somewhere from our conversation about this in Bonn! It's not fresh in my mind, so sorry if this is wrong/vague, but I sort of remember wondering if we could treat this as a normalization tactic/how we'd describe the normal form of these expressions?

I stole the above paragraph from a DM to you ;)

I don't have a solid theoretical understanding of normal forms but my instinct is that the normal form of a whiskered natural transformation is (Ηα)Κ (in application order) because the Ηα bit indicates where naturality applies (to morphisms in the image of HF or HG (in application order)), while the precomposition by K is often less important than the postcomposition by H.

A normal form might also move the postcomposition by a functor past a composite, privileging Hα >> Ηβ  over H(α >> β). It would be nice though if there were something like the @[assoc] tag (eg @[func]) that could take a proof that eg f >> g = h >> k  and automatically generate a proof that Hf >> Hg = Hh >> Hk.

Yuma Mizuno (Jan 14 2025 at 19:30):

I've completed the 2-category challenge!

mateEquiv_vcomp

A few comments:

I used the bicategory tactic, which is a kind of partial automation. It automatically proves that 2-morphisms with the same string diagram are equal in a strict sense. (My talk on Friday is somewhat related to such a tactic.). By strict, I mean that no topological identifications are allowed.

String diagrams (in this strict sense) are less flexible than pasting diagrams in that the order of the 2-cells must be specified. In the proof above, exchanges of 2-cells are done manually. This is why the proof contains many rw [← whisker_exchange]s.

The proof above is not very long, but actually we don't want to write such proofs by hand. Ideally, it should be more automated. I think at least it would be nice to have a tactic that solves the equation between 2-morphisms that differ only in the composition orders.

Pietro Monticone (Jan 14 2025 at 22:48):

:video_camera: Video recording: https://youtu.be/pV6BIImkToU?si=0DHXxrFkqreAM3d9

Yuma Mizuno (Jan 15 2025 at 03:09):

Emily Riehl said:

I don't have a solid theoretical understanding of normal forms but my instinct is that the normal form of a whiskered natural transformation is (Ηα)Κ (in application order) because the Ηα bit indicates where naturality applies (to morphisms in the image of HF or HG (in application order)), while the precomposition by K is often less important than the postcomposition by H.

A normal form might also move the postcomposition by a functor past a composite, privileging Hα >> Ηβ  over H(α >> β). It would be nice though if there were something like the @[assoc] tag (eg @[func]) that could take a proof that eg f >> g = h >> k  and automatically generate a proof that Hf >> Hg = Hh >> Hk.

Actually, a normal form is already defined in mathlib docs#Mathlib.Tactic.BicategoryLike.NormalExpr. In this definition, the normal form of a whiskered 2-morphism is K (α H) in diagrammatic order. This choice can be arbitrary, though.

What bicategory tactic does is rewrite any 2-morphism into its normal form.

Emily Riehl (Jan 17 2025 at 16:52):

@Yuma Mizuno congrats! I need to spend time figuring out how all of this works. Looking forward to your talk.

Yuma Mizuno (Jan 17 2025 at 16:55):

Emily Riehl said:

Yuma Mizuno congrats! I need to spend time figuring out how all of this works. Looking forward to your talk.

Thanks. I won't go into too much detail, but I'll give a rough outline how it works.

Last updated: May 02 2025 at 03:31 UTC