eqToHom and pullback

Stream: new members

[Shanghe Chen]

Hi I am stuck at the following lemma:

import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Preserves.Limits

open CategoryTheory Category Functor Limits IsLimit
universe v u
variable {C: Type u} [Category.{v} C]
variable {D: Type u} [Category.{v} D]

variable {C: Type u} [Category.{v} C] [HasLimits C]
variable {D: Type u} [Category.{v} D] [HasLimits D]
variable {X₁ X₂ Y Z : C}
variable (f₁: X₁ ⟶ Y) (f₂: X₂ ⟶ Y) (g: Y ⟶ Z)
variable (F: C ⥤ D)
lemma eq1 :  pullback (F.map (f₁ ≫ g)) (F.map (f₂ ≫ g)) = pullback (F.map f₁ ≫ F.map g) (F.map f₂ ≫ F.map g) := by
  congr 1 <;> apply F.map_comp

lemma eq2: (eqToHom (eq1 f₁ f₂ g F)) ≫ pullback.fst = pullback.fst := by
  sorry

Is it any way to prove this? Directly rewrite eqToHom seems giving a harder goal

[Joël Riou]

It is possible to prove, but a better approach would be to use pullback.congrHom.

[Shanghe Chen]

Oh I didn't notice it before. Thank you very much for mentioning pullback.congrHom. Yeah I am switching to use it.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Why is congrHom preferrable? Is that always the case? I have found the following lemma useful:

@[simp]
lemma pullback.map_id' {W X S : C}
    (f₁ f₂ : W ⟶ S) (g₁ g₂ : X ⟶ S) [HasPullback f₁ g₁] [HasPullback f₂ g₂] (h) (h') :
    pullback.map f₁ g₁ f₂ g₂ (𝟙 W) (𝟙 X) (𝟙 S) h h' = eqToHom (by simp at h h'; simp [h, h'])

but maybe in some cases it is bad because it moves from 'pullback comparison map land' to 'eqToHom land'?

[Adam Topaz]

I think this is probably a bad lemma indeed. There will be no way for simp to make further progress once that lemma is used.

[Adam Topaz]

What’s the context for needing this lemma?

[Adam Topaz]

Also, for completely unrelated reasons, I don’t think expensive tactics should be used to state lemmas

[Adam Topaz]

IMO a better formulation would be

@[simp]
lemma pullback.map_id' {W X S : C}
    (f₁ f₂ : W ⟶ S) (g₁ g₂ : X ⟶ S) [HasPullback f₁ g₁] [HasPullback f₂ g₂] (h) (h') (h'') :
    pullback.map f₁ g₁ f₂ g₂ (𝟙 W) (𝟙 X) (𝟙 S) h h' = eqToHom h''

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Adam Topaz said:

Also, for completely unrelated reasons, I don’t think expensive tactics should be used to state lemmas

In your formulation, simp would have to invent h'' when using this lemma, no? So you really couldn't use it with simp then.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Adam Topaz said:

What’s the context for needing this lemma?

It's a little complicated to contextualize, but I have some goals of the form pullback.map .. ≫ g = eqToHom .. ≫ g that arise in the proof of some universal property (this one specifically). What about having the opposite direction as a simp lemma, then? I.e. if an eqToHom happens to equate two pullbacks, then it's pullback.map. Then maybe simp can make further progress with pullback.map?

[Adam Topaz]

yes, you're right, but I also don't think it should be a simp lemma :)

[Adam Topaz]

but essentially the only way to continue with such an eqToHom h'' is to subst h'' to convert it to an identity map.

[Shanghe Chen]

Wojciech Nawrocki said:

Why is congrHom preferrable? Is that always the case?

It has been a while for me and I forgot the concrete detail. But I came across this while I am trying to use to prove the diagram docs#Mathlib.CategoryTheory.Limits.pullbackDiagonalMapIdIso in the yoneda style, where it has lots of preserving limits and creating limits stuffs. In that case congrHom seems quite suitable. But finally I seemed getting rid of congrHom too for using more results from mathlib