feat(order/category/DecLinOrder): updates to concrete_category, and instances for order categories

[semorrison]

This is stacked on top of @urkud's #1380, refactoring concrete categories.

The only additional commit beyond that is 0107097.

I wanted to test that refactor out, by adding the categories Preorder, PartialOrder, LinOrder, DecLinOrder, as an experiment with a (slightly) deep algebraic hierarchy.

I did end up making one substantive change to Yury's work on concrete categories, in particular there are now two main sources of has_coe_to_sort instances. As well as

instance : has_coe_to_sort (bundled c) :=	
{ S := Type u, coe := bundled.α }	

we have

instance induced_category.has_coe_to_sort {C D : Type (u+1)} [concrete_category D] (f : C → D) :
  has_coe_to_sort (induced_category D f) :=
concrete_category.has_coe_to_sort (induced_category D f)

Using this, I've switch to defining many concrete categories directly via induced_category, rather than providing additional bundled_hom instances. (A small change here -- I made the "origin category" argument of induced_category explicit, as it's very often useful to be able to give it by hand.)

There is also the more general

def concrete_category.has_coe_to_sort (C : Type u) [concrete_category C] : has_coe_to_sort C :=
{ S := Sort u, coe := (concrete_category.forget C).obj }

which would work too, but because it applies to any type is too expensive to have as a global instance.

Defining DecLinOrder worked very smoothly! I've also tweaked all the constructions of concrete categories.

[semorrison]

Yes, I'll have a look at the summary. I'm doing some experiments on making def Ring := only locally reducible, at the moment, but I think either way we're very close now on this one.

[semorrison]

Okay, @urkud and @jcommelin, one more change (sorry this has been a constantly evolving PR...) We now only mark bundled types as [reducible] locally. It seems to work out okay, and is easy to reverse if needed.

[rwbarton]

I'm surprised you want to make D an explicit argument. Shouldn't it normally be inferable from F? Are there specific places where this change is needed?

[rwbarton]

Are the categories defined in this file intended to be permanently [reducible]? I'm not really sure what the ramifications are here, but this PR does go to the trouble of making a bunch of other categories not [reducible]...

[semorrison]

No, this was just an oversight. After the discussion of Zulip I’m now second guessing this whole local attribute [reducible] business. In particular I’m worried that it may be contributing to the problems in CommRing/adjunction.lean.

[rwbarton]

Was there any particular reason to change this one and the next, but not the one above?

[rwbarton]

This clearly indicates that something is wrong. Do you understand the error in adj that occurs without this definition?

[rwbarton]

I spent a while tracking down the cause of the failures in algebra.category.CommRing.adjunctions and the basic issue is that when we "exit the category theory world" and want to apply a mathlib lemma about an unbundled commutative ring, the underlying type of that commutative ring might be spelled in many different ways. For example, it might be ↥R (with a coercion, R : CommRing) or R.α or (forget CommRing).obj R or even ↥(bundled.map ring.to_semiring (bundled.map comm_ring.to_ring R)) depending on which particular category-theory definitions were unfolded. Then we need to find the comm_ring instance by type class inference, and getting that to work in all cases is not an easy task.

• One approach is to try to write a lot of instances which together match all the forms that could appear. It's not clear how to do this without an explosion of instances. For example, in the instance problem comm_ring ↥(bundled.map ring.to_semiring (bundled.map comm_ring.to_ring R)), the outermost part bundled.map ring.to_semiring doesn't have anything to do with comm_ring; we need to go deeper. On the other hand, if we only wanted a semiring instance, we should presumably not look any further.
• The other potential approach, which I hope can be made to work, is to make these trivial unbundling/rebundling operations like ↥ and forget and bundled.map reducible, so that instance search can see that they are all the same. Then we only need a single instance instance (R : CommRing) : comm_ring R := R.str. Simiarly stuff like instance separated_forget (X) : separated ((forget₂ CpltSepUniformSpace UniformSpace).obj X) should be simplified to instance separated_forget (X : CpltSepUniformSpace) : separated X.

[semorrison]

Note to self: reopen #1439 if/when this gets merged.

[jcommelin]

@rwbarton Thanks for this investigation! Sounds good. I hope that it works.

[rwbarton]

This PR became awkwardly large, so I've re-PRed the core bit as #1491; once that lands we should be able to split this into small, easy independent pieces.

[semorrison]

I'm going to close this in the meantime to reduce clutter. (I'm also not really sure there's anything worth salvaging post #1491.)

[semorrison]

Except for the actual content on DecLinOrder, which has now been split off into the branch DecLinOrder_2, everything else here has now made it into another PR.