Commutative diagrams for diagram chasing

Stream: maths

[Robert Maxton]

As part of a general personal project to get diagrammatic reasoning in various forms into Mathlib, I'm thinking about how one might implement commutative diagrams in a more general form than the current CommSq and CommTriag, in such a way that they can be easily (but correctly) composed and desired properties easily extracted.

The first step, of course, is to pin down what the type of commutative diagrams should be, which.. is actually something I realized I'm not terribly certain of! My current outline is that a general CommDiag C in a category C should consist of:

• a Set C of objects in the diagram
• a generating Set (X ⟶ Y) for every X, Y ∈ obj
• and a proof that the resulting subcategory generated from composition by the given morphisms is thin

i.e. something like

import Mathlib.CategoryTheory.Widesubcategory
import Mathlib.CategoryTheory.FullSubcategory


universe v u

namespace CategoryTheory

namespace MorphismProperty

inductive CompClosure {C} [Category.{v, u} C] (r : MorphismProperty C) : ⦃X Y : C⦄ → (X ⟶ Y) → Prop where
| id (X : C) : CompClosure r (𝟙 X)
| of {X Y : C} (f : X ⟶ Y) (h : r f) : CompClosure r f
| comp_left {X Y Z : C} (f : X ⟶ Y) (i : Y ⟶ Z) (h : CompClosure r i) : CompClosure r (f ≫ i)
| comp_right {X Y Z : C} (i : X ⟶ Y) (g : Y ⟶ Z) (h : CompClosure r i) : CompClosure r (i ≫ g)

variable {C} [Category.{v, u} C] (r : MorphismProperty C)

instance : IsMultiplicative (CompClosure r) where
id_mem X := .id X
comp_mem f g hf _ := .comp_right f g hf

end MorphismProperty

structure CommDiagStruct (C : Type u) [Category.{v} C] where
  obj' : Set C
  hom' : ∀ X ∈ obj', ∀ Y ∈ obj', Set (X ⟶ Y)

namespace CommDiagStruct
variable {C} [Category.{v, u} C] (diag : CommDiagStruct C)

def hom : MorphismProperty (FullSubcategory diag.obj') :=
  fun {X Y} f ↦ diag.hom' X.obj X.property Y.obj Y.property f

abbrev obj := WideSubcategory diag.hom.CompClosure
end CommDiagStruct

structure CommDiag (C : Type u) [Category.{v} C] extends CommDiagStruct C where
  thin : (inferInstanceAs <| Quiver toCommDiagStruct.obj).IsThin

Is this in fact mathematically correct? Or can I get more exotic commutative diagrams that rely more subtly on precisely what arrows are and aren't depicted -- I vaguely recall being confused by equalizer diagrams at one point for some related reason, maybe?

[Kevin Buzzard]

Yes my working definition for "does this diagram commute" was "are all ways of getting from A to B the same map?" and equalizer diagrams don't satisfy this.

[Joël Riou]

Instead of using Set C, it would probably be better to use a parametrizing type ι and a map obj : ι → C.

[Robert Maxton]

Kevin Buzzard said:

Yes my working definition for "does this diagram commute" was "are all ways of getting from A to B the same map?" and equalizer diagrams don't satisfy this.

Mm... well, it's a bit clunky, but I think we can salvage the definition by just permitting a fixed set of exceptions, with the idea being that even if A ⟶ B isn't thin, A ⟶ B ⟶ C is thin again. Of course, it makes the gluing rules more complicated, but not by too much, I don't think?

[Robert Maxton]

Joël Riou said:

Instead of using Set C, it would probably be better to use a parametrizing type ι and a map obj : ι → C.

My motivation for using Set C was that I wanted gluing diagrams together to be trivial, and Set has a very ergonomic union. It also automatically imposes the requirement that every object and hom appears at most once in the underlying representation; maybe for display purposes we can allow the user to have a single object appear in multiple places, but I want that to be purely a QoL convenience

[Johan Commelin]

Please look at the recent work of Assia Mahboubi, Matthieu Piquerez et al. They describe a DSL of sorts for diagrammatic reasoning

[Robert Maxton]

https://arxiv.org/abs/2402.14485 ?

[Johan Commelin]

Yes, exactly! (Sorry, I was on a rush on the phone, so I didn't search for a link.)