Equality in categories

Stream: new members

[Dion Leijnse]

I am working on a proof where I need quite a lot of commutative squares of commutative algebras (or fields, to be more specific). I also need to glue these squares together, or for example say that a certain morphism in the square is already a given one. The most succinct way to write a square in a category seems to be to write

import Mathlib

open CategoryTheory

variable (C : Type) [Category C]
variable (S : Square C)

But then Lean complains if I want to do the following:

variable {X Y : C} (f : X ⟶ Y)

variable (h : S.f₁₂ = f)

I can fix this by replacing the f by Arrow.mk f, but as soon as I start trying to glue squares together (by using CategoryTheory.Square.commSq and CategoryTheory.CommSq.horiz_comp), I start running into issues by morphisms not being definitionally equal. Is there a good way to work with horizontally/vertically composing squares in CategoryTheory.Square, or is it better to just work in the context of CategoryTheory.CommSq?

[Joël Riou]

The right API for this is https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/CommSq.html for which the objects and morphisms are parameters to the CommSq structure, rather than fields. See https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.html#CategoryTheory.IsPullback.paste_vert for examples of statements about pasting squares.

[Dion Leijnse]

Thanks!