Zulip Chat Archive

Stream: mathlib4

Topic: Porting CategoryTheory.NaturalIso


Richard Osborn (Dec 02 2022 at 02:09):

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 (Dec 02 2022 at 02:17):

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 (Dec 02 2022 at 02:18):

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

Scott Morrison (Dec 02 2022 at 02:19):

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 (Dec 02 2022 at 02:24):

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 (Dec 02 2022 at 02:37):

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

Richard Osborn (Dec 02 2022 at 02:48):

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

Kevin Buzzard (Dec 02 2022 at 17:04):

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 (Dec 02 2022 at 17:09):

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 (Dec 02 2022 at 17:45):

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

Scott Morrison (Dec 02 2022 at 17:45):

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.


Last updated: Dec 20 2023 at 11:08 UTC