category theory

Stream: general

[Floris van Doorn]

I'm working a bit on the category theory library in the branch limits-isos. My initial goal was to show that if C has products/coproducts/..., then Cᵒᵖ has coproducts/products/..., but I've also been changing some other things, like the definition of equivalence (now it's an adjoint equivalence).

One thing I want to change is that if we have a natural transformation α : F ⟶ G, I would like to write α.app for its action on objects. The problem is that the type of α is has_hom.hom and the full name of app is nat_trans.app, so it often doesn't work (it works sometimes, but not reliably, and I don't know why it sometimes doesn't work).
I tried to add a declaration

@[reducible] def has_hom.hom.app {F G : C ⥤ D} (α : F ⟶ G) (X : C) : F.obj X ⟶ G.obj X := nat_trans.app α X

This works, but now we have two versions of app which are not syntactically equal, which causes major headaches when rewriting/simplifying. In the branch limits-isos tried to get it to work, but in some rare cases α.app will actually use nat_trans.app, which is undesirable.

Any suggestions to resolve this? I'm now leaning towards removing has_hom.hom.app and live with the fact that we sometimes have to write nat_trans.app α instead of α.app

[Mario Carneiro]

shouldn't it unfold to nat_trans in this example, so α.app means nat_trans.app α?

[Mario Carneiro]

I think adding has_hom.hom.app will not make this better

[Mario Carneiro]

but I'm curious to see your problem cases where α.app doesn't work

[Floris van Doorn]

I'll undo the change and double check where I ran into problems. Maybe it was a case where the category instance wasn't synthesized yet.

[Floris van Doorn]

@[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F).app X = 𝟙 (F.obj X) := rfl

gives (with pp.implicit set to true)

invalid field notation, 'app' is not a valid "field" because environment does not contain 'category_theory.has_hom.hom.app'
  𝟙 F
which has type
  F ⟶ F
Additional information:
d:\projects\mathlib\src\category_theory\functor_category.lean:42:48: context: invalid field notation, 'app' is not a valid "field" because environment does not contain 'category_theory.has_hom.rec.app'
  𝟙 F
which has type
  @has_hom.rec (C ⥤ D) (λ [c : has_hom (C ⥤ D)], C ⥤ D → C ⥤ D → Sort ?)
    (λ (hom : C ⥤ D → C ⥤ D → Sort ?), hom)
    (@category_struct.to_has_hom (C ⥤ D) ?m_1)
    F
    F

Using (𝟙 F : F ⟶ F).app does work.

[Floris van Doorn]

So it seems that sometimes the functor category instance wasn't synthesized yet. But so far this happens only a couple of times, so it seems very manageable.