ConcreteCategory.instFunLike became a global instance

Stream: mathlib4

[Kim Morrison]

During the port we accidentally made ConcreteCategory.instFunLike a global instance in Mathlib/Topology/Category/TopCat/Basic.lean:

-- Porting note: cannot find a coercion to function otherwise
attribute [instance] ConcreteCategory.instFunLike in
instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
  coe f := f

Despite the in, this makes it a global instance (we desperately need a linter for this!!!).

[Kim Morrison]

I've started to try to fix this on branch#TopCat_cleanup2, but there's still a lot that is broken.

[Kim Morrison]

Advice welcome. :-)

[Kim Morrison]

(There appears to be only one other such case, in src#ExteriorAlgebra.GradedAlgebra.ι_sq_zero, which is trivially fixed in #13144.)

[Dagur Asgeirsson]

@Kim Morrison I just filled in the sorry in TopCat/Limits/Products and pushed it to your branch

[Dagur Asgeirsson]

Looking at the pullback file now

[Kim Morrison]

Thanks! I was wondering about asking you, as you are very much working downstream of this problem!

[Dagur Asgeirsson]

Pullback file is error-free now as well. The problem seems to be that there are some lemmas that simp isn't seeing, such as docs#CategoryTheory.comp_apply, and I had to use erw instead

[Dagur Asgeirsson]

In many of the CompHaus-related files, you've added the line

attribute [local instance] ConcreteCategory.instFunLike -- TODO remove this?

and everything works. Is this bad? I mean, would it be better to refactor the files to not use this instance?

[Kim Morrison]

Yes, it would be better.

[Kim Morrison]

But it's better than the current situation where we accidentally made it global.

[Dagur Asgeirsson]

Kim Morrison said:

Yes, it would be better.

Why is that better?

[Kim Morrison]

Hmm... Let me think on that one. I agree it is not obvious that wanting to turn off the global instance implies we should not want to use it locally either.

[Kim Morrison]

Is this branch building now? If so I think we should PR it. We can either just remove the -- TODO remove this? comments,

[Kim Morrison]

or change the comment too -- Previously, this had accidentally been made a global instance, and we now turn it on locally as convenient.

[Dagur Asgeirsson]

No there are still lots of new files with errors appearing in CI after every fix. There are some in Topology/Gluing which aren't fixed by adding the local instance. I'm not very familiar with the API so I'm having trouble fixing that one.

[Kim Morrison]

I wonder if we can tempt @Andrew Yang into having a look. I think cleaning up the basic setup of TopCat is going to be key to resolving the suffering in AG at present.

[Dagur Asgeirsson]

TopCat.pullbackIsoProdSubtype_inv_fst_apply and the snd version are simp lemmas that are frequently failing and I have to use erw instead. Any idea why this might be?

[Kim Morrison]

Can you see if they work with simp (config := {index := false})?

[Kim Morrison]

Oh, hrm, that is only available on nightly-testing.

[Kim Morrison]

The problem is going to be that some implicit argument (e.g. of TopCat.of (X : TopCat)) has dsimp'd "the wrong amount". It may be that going into those lemmas that aren't firing and putting no_index in front of some of the implicit arguments will help. But it's a pretty manual/painful process to discover if anything helps.

[Dagur Asgeirsson]

Dagur Asgeirsson said:

No there are still lots of new files with errors appearing in CI after every fix. There are some in Topology/Gluing which aren't fixed by adding the local instance. I'm not very familiar with the API so I'm having trouble fixing that one.

I managed to fix the gluing file after all

[Andrew Yang]

I just got home. Is there anything (maybe a problematic file?) I could help?

[Dagur Asgeirsson]

I just pushed a commit fixing the last two files with errors in CI. You can see if there are other files with errors after CI runs on the latest commit, I'm taking a break now

[Andrew Yang]

Some rw errors come from the fact that there are two funlike instances on homs in TopCat.
I think making ConcreteCategory.hasCoeToSort and ConcreteCategory.instFunLike fields of ConcreteCategory might solve some of the problems we are facing?

[Matthew Ballard]

Can't you get rid of one?

[Andrew Yang]

One is precisely ConcreteCategory.instFunLike, which is the reason why it cannot be a global instance.

[Andrew Yang]

But even if it is not a global instance, it makes applying general lemmas about concrete categories (where this instance is on) difficult.

[Kim Morrison]

Yes, it was while trying to get rid of this duplication that I noticed we had accidentally made ConcreteCategory.instFunLike a global instance.

[Andrew Yang]

Something like

class ConcreteCategory (C : Type u) [Category.{v} C] where
  hasCoeSort : CoeSort C (Type w)
  funLike : ∀ X Y : C, FunLike (X ⟶ Y) X Y
  map_id : ∀ X : C, (𝟙 X : X → X) = id
  map_comp : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g : X → Z) = g ∘ f
  map_injective : ∀ {X Y} {f f' : X ⟶ Y} (e : (f : X → Y) = (f' : X → Y)), f = f'

[Kim Morrison]

I think this is going to be a pretty radical change. I'm not saying I'm against it, but I think life we be easier if we make the existing concrete categories more uniform first, and than try changes like this.

[Andrew Yang]

Maybe docs#ConcreteCategory.hasCoeToSort should be reducible?

[Matthew Ballard]

Not sure but worth a shot.

[Dagur Asgeirsson]

Kim's branch is now PR #13170. I'm expecting everything to build now, but I don't know if we want to merge this and then do some more radical refactor of concrete categories, or the other way around

[Matthew Ballard]

We should at least mark the erw regressions with an identifier (eg issue) so we can rip them all out with a fix

[Dagur Asgeirsson]

Ok that makes sense. At least all the errors are gone now

[Dagur Asgeirsson]

I don't have more time for this today unfortunately

[Kim Morrison]

Thanks very much for the help on this. I was starting to get intimidated by the problems in ConcreteCategory land, so I'm excited to see everyone is interested! I think we should merge this, and then start experimenting with deeper fixes.

[Matthew Ballard]

It builds now. The PR number is attached as tracker. Benchmarking is in progress.

My choice of linting was to delete a few simp's so I cannot call bors

[Matthew Ballard]

-162B

[Andrew Yang]

Andrew Yang said:

Something like

class ConcreteCategory (C : Type u) [Category.{v} C] where
  hasCoeSort : CoeSort C (Type w)
  funLike : ∀ X Y : C, FunLike (X ⟶ Y) X Y
  map_id : ∀ X : C, (𝟙 X : X → X) = id
  map_comp : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g : X → Z) = g ∘ f
  map_injective : ∀ {X Y} {f f' : X ⟶ Y} (e : (f : X → Y) = (f' : X → Y)), f = f'

For the record, this does not work. If we have instance : CoeSort (Bundled c) (Type w) = ⟨Bundled.α⟩, then for X : Bundled c, X : Type w will (reducibly) become Bundled.α X, but via the instance in ConcreteCategory it is CoeSort.coe X, and they are not reducibly equal.

[Michael Rothgang]

I wrote a syntax linter for this, in #13190. Careful review by something whose meta skills are less cargo-culted than mine welcome.

[Kim Morrison]

Okay, shall we merge this? Obviously the additional erws are sad, but I think this is a case where we have to go backwards in order to go forwards.

[Dagur Asgeirsson]

I merged master to get rid of a merge conflict -- should be good to go (it builds, but CI is still linting)

[Dagur Asgeirsson]

We should probably try to merge this pretty quickly, I've just fixed another merge conflict (awaiting CI)

[Kevin Buzzard]

I made a bunch of pernickety comments but I agree that if we're merging this then it should be merged quickly!