port Algebra.Category.Ring.Basic !4#3901

Stream: mathlib4

[Scott Morrison]

I would like to refactor how we have set up the concrete categories MonCat, GroupCat, and ModuleCat, see !4#3900.

Using that refactor, I have then unstuck the port of Algebra.Category.Ring.Basic (originally in !4#3105) in !4#3901. (I made a separate PR rather than just pushing, because of the big refactor to earlier files. If the refactor PR is okay, I can just recombine them.)

It would be great if these could be reviewed soon, as I would really like to renew progress on this part of the port. @Adam Topaz, @Joël Riou, @Johan Commelin, anyone else. :-)

It is not the most complete refactor ever, there are still things to clean up, but I would like to get Algebra.Category.Ring.Basic merged asap so people can start porting again, and I can to a further "make everything uniform" PR again soon.

[Johan Commelin]

I've only looked at the PR briefly, but I like the gist of it!

[Johan Commelin]

@Scott Morrison Do we need the coe_id and coe_comp for every bundled category? Can't we have two lemmas for concrete categories that abstract all of these?

[Scott Morrison]

Not that I could get to work, but yes, I was really hoping so! Happy if someone can get this to work, or I can try again later.

[Matthew Ballard]

Making Bundled.\areducible didn’t break anything here. I haven’t had a chance to see if it helps.

[Adam Topaz]

I took a quick look at !4#3900 and overall it looks good to me! Concerning the repetition of coe_id, coe_comp etc., I bet we could write a macro to add these lemmas quite easily.

Looking ahead, what do you think about making morphisms in, say, GroupCat a structure with a single MonoidHom field? I often find it quite annoying when lean gets confused between morphisms in GroupCat or similar bundled categories and the associated morphisms from the algebra library. With the correct CoeFun instance (which it seems we need to add anyway!) and ext lemmas, etc., the user experience wouldn't be much different.

[Matthew Ballard]

Is this a reasonable thing?

instance {α β : Type u} [I : BundledHom hom] (Iα : c α) (Iβ : c β) : CoeFun (hom Iα Iβ) fun _ => α → β where
  coe := I.toFun Iα Iβ

[Adam Topaz]

I think lean would still get confused between hom and Quiver.hom.

[Matthew Ballard]

Making TopCat an abbrev seems to remove some dsimp's and doesn't break anything so far

[Matthew Ballard]

Also what is going on with ModuleCat ℤ it seems like an odd duck

[Matthew Ballard]

example : (forget TopCat).obj X = X := rfl is fine but

instance topologicalSpace_forget (X : TopCat) : TopologicalSpace <| (forget TopCat).obj X :=
  inferInstance

still fails. It seems like this rfl was applied in ML3 automatically

[Adam Topaz]

That's after forget was made reducible, right?

[Matthew Ballard]

Yes. I think I am working there

[Adam Topaz]

well that's not great

[Matthew Ballard]

My understanding of Scott's PR is that all coercions should flow through Bundled and not ConcreteCategory since most (?) ConcreteCategory's are bundled up.

[Matthew Ballard]

So we wouldn't see forget any more

[Matthew Ballard]

Changing from

attribute [instance] ConcreteCategory.hasCoeToFun in
instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe f := f

to

instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
  coe f := BundledHom.toFun bundledHom X.str Y.str f

let's me remove topologicalSpace_forget completely from TopCat.Basic at the price of breaking composition results in homeoOfIso (which can be fixed in a standard manner).

[Matthew Ballard]

Statements like OpenEmbedding ((forget TopCat).map f >> (forget TopCat).map g) can be written as OpenEmbedding (f >> g).

[Scott Morrison]

@Matthew Ballard, would it be okay if we made the changes to TopCat in a separate PR? I'd like to keep this moving.

[Matthew Ballard]

I mentioned these things because it supports moving the coercions from ConcreteCategory to Bundled/BundleHom as the PR does. So it looks like a good start to me! (though it is already merged now lol)