prove that parallelPair commutes with functor?

Stream: new members

[Shanghe Chen]

Hi in a recent exercise I reached a situation like:

import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

noncomputable section
universe v u v' u'

set_option autoImplicit false
-- set_option pp.all true

open CategoryTheory Functor Limits

variable {C: Type u} [Category.{v} C]
variable {D: Type u'} [Category.{v'} D]
variable [HasFiniteLimits D]
variable (F: C ⥤ D)
variable (X Y : C) (f g : X ⟶ Y)
example : (parallelPair f g) ⋙ F ≅ (parallelPair (F.map f) (F.map g)) := by
  sorry

example : limit ((parallelPair f g) ⋙ F) ≅ limit (parallelPair (F.map f) (F.map g)) := by
  sorry

I tried but failed to prove this. Any idea please? the limit version should be enough for me but rewriting parallePair or using eqToIso seems makeing the goal more complicated.

[Andrew Yang]

Maybe docs#CategoryTheory.Limits.parallelPair.ext ?

[Andrew Yang]

Or

example : (parallelPair f g) ⋙ F ≅ (parallelPair (F.map f) (F.map g)) :=
  CategoryTheory.Limits.diagramIsoParallelPair _

[Shanghe Chen]

Thank you very much! Yeah the diagramIsoParallelPair is very nice!

[Shanghe Chen]

Hi I found that it can be proved equal using CategoryTheory.Functor.ext directly, that chained <;> using simp prove subgoals in a bunch:

import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.EqToHom
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits



noncomputable section
universe v u v' u'

set_option autoImplicit false
-- set_option pp.all true

open CategoryTheory Functor Limits

variable {C: Type u} [Category.{v} C]
variable {D: Type u'} [Category.{v'} D]
variable [HasFiniteLimits D]
variable (F: C ⥤ D)
variable (X Y : C) (f g : X ⟶ Y)
example : (parallelPair f g) ⋙ F = (parallelPair (F.map f) (F.map g)) := by
  apply CategoryTheory.Functor.ext
  rintro (_|_|_) <;> rintro (_|_|_) <;> rintro f <;> cases f <;> simp
  rintro (_|_|_) <;> simp

example : limit ((parallelPair f g) ⋙ F) = limit (parallelPair (F.map f) (F.map g)) := by
  congr 1
  apply CategoryTheory.Functor.ext
  rintro (_|_|_) <;> rintro (_|_|_) <;> rintro f <;> cases f <;> simp
  rintro (_|_|_) <;> simp

[Shanghe Chen]

Don’t know if it’s a good practice for using CategoryTheory.Functor.ext or not but the equality rather than isomorphism seems working more convenient in my case :tada: