proving commutativity of diagrams

Stream: Is there code for X?

[Anthony Bordg]

Has Mathlib something more direct than using docs#CategoryTheory.Functor.map_comp to prove that a functor maps a commutative diagram to a commutative diagram?

[Markus Himmel]

What is your notion of "commutative diagram" here? If a commutative diagram in C is just a functor I ⥤ C, then the fact that a functor C ⥤ D preserves commutative diagrams is docs#CategoryTheory.Functor.comp

[Anthony Bordg]

Markus Himmel said:

What is your notion of "commutative diagram" here?

I want to prove F f ≫ F g = F f' ≫ F g', knowing that I have a proof of f ≫ g = f' ≫ g'.

[Markus Himmel]

You might be interested in docs#CategoryTheory.CommSq.map, i.e.,

import Mathlib

open CategoryTheory

variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
variable  {X Y Z W : C} {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X ⟶ W} {g' : W ⟶ Z}

example (h : f ≫ g = f' ≫ g') : F.map f ≫ F.map g = F.map f' ≫ F.map g' := by
  simp [← Functor.map_comp, h]

example (h : f ≫ g = f' ≫ g') : F.map f ≫ F.map g = F.map f' ≫ F.map g' :=
  ((CommSq.mk h).map F).w