limits in Ab

Stream: condensed mathematics

[Johan Commelin]

We need something like

-- show that `Ab.{u}` has limits indexed by `ℕ`.
instance (f : ℕ → Ab) : has_product f := sorry

We know that Ab has all limits, but they indexed by types in the wrong universe. Anyone interested in relaxing the universe conditions in mathlib?

[Scott Morrison]

Ooh, it's worse than that, it goes back to the constructions for Type

[Scott Morrison]

I think I'm getting it working, but it is more complicated than one might hope.

[Johan Commelin]

Hmm, sorry to hear that.

[Scott Morrison]

Okay, #13990

[Scott Morrison]

I'm concerned about the extra universe annotations needed in places. Please consider this an RFC for now.

[Scott Morrison]

@Andrew Yang, if you're able to look at this PR sometime, you are probably most expert in this material (universe flexibility in limits!).

[Scott Morrison]

This PR touches lots of files, and just saw some merge conflicts. If we want it, I'd prefer to decide this sooner rather than later.

[Johan Commelin]

I'm happy with merging it. I don't mind the extra universe annotations.

[Johan Commelin]

The extra flexibility is worth it.

[Scott Morrison]

Okay, we'll see if we regret it later. :-)