Porting CategoryTheory.NaturalIso

Stream: mathlib4

[Richard Osborn]

I've started the initial work for porting over CategoryTheory.NaturalIsomorphism and noticed that we had renamed category_theory.isomorphism to CategoryTheory.Iso. Should this name change be reflected in other uses of the word isomorphism? Also, I have been running into issues with lean4 not being able use category.assoc in rewrites. Has anyone else ran into this issue? Seems like category.assoc's type is more general over universes, but it isn't clear how lean is getting confused.

[Scott Morrison]

Sorry, that file rename was my doing, and probably ill-considered. The type has always been named iso (now Iso), so it shouldn't be too much trouble. But we can also just change the name back.

[Scott Morrison]

We should either rename CategoryTheory.NaturalIsomorphism to CategoryTheory.NatIso, or rename CategoryTheory.Iso back to CategoryTheory.Isomorphism.

[Scott Morrison]

I'm a bit surprised about the rewrite issues with assoc, I hadn't see that yet. Is there a branch to look at?

[Richard Osborn]

It seems like the convention is shortening the names (NatTrans.lean), so I will follow that for now. Will push a branch momentarily

[Richard Osborn]

Ok, I've created the PR mathlib4#820. Will continue to work around the category.assoc errors.

[Richard Osborn]

lean4 is also having trouble using Iso.inv_hom_id_app_assoc and Iso.inv_hom_id_assoc . Probably a similar issue.

[Kevin Buzzard]

My understanding of the error in mathlib4#820 is that it is the reassoc attribute which is at fault. Right now it's auto-generating X_assoc errors which do not correspond to the Lean 3 declarations (are these being auto-aligned BTW?). I didn't observe any problems rewriting with category.assoc itself. In the file NatIso.lean in the branch:

@[simp, reassoc]
theorem inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
    α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
  congr_fun (congr_arg NatTrans.app α.inv_hom_id) X
#align category_theory.iso.inv_hom_id_app CategoryTheory.Iso.inv_hom_id_app

#check inv_hom_id_app_assoc
/-
NatTrans.app (α.inv ≫ α.hom) X ≫ h = NatTrans.app (𝟙 ?m.1943) X ≫ h
-/
-- this is definitely wrong: for example the 𝟙 should have been cancelled.
-- The below lemma is what I believe should have been generated:
@[simp] lemma inv_hom_id_app_assoc' {F G : C ⥤ D} (α : F ≅ G) (X : C) {Z : D} (h : G.obj X ⟶ Z) :
    α.inv.app X ≫ α.hom.app X ≫ h = h := by
  rw [← Category.assoc, inv_hom_id_app, Category.id_comp]

And now simp works fine to close the goal in naturality_1 later on. Unfortunately I can't understand how reassoc works but this I believe is the core issue.

[Scott Morrison]

Great, thanks for diagnosing. The reassoc attribute is a completely different implementation than in mathlib3, so likely I missed something. I'll look later today.

[Scott Morrison]

Okay, I've pushed a fix to reassoc directly to this branch.

[Scott Morrison]

reassoc was reading the proof, and inferring the type it was meant to be reassociating from that, and I just needed to tell it to read the declared type instead.