Limits in CompHaus..._1

Stream: condensed mathematics

[Adam Topaz]

I made some progress toward showing that CompHausFilt..._1 has limits. So far, I've defined essentially all of the comphaus_filt_pseudo_normed_group structure on what should be the limit of a diagram. There are three sorry's (all about continuity) left for this here: https://github.com/leanprover-community/lean-liquid/blob/8b5d6a422d7815f23aafa2da8ea99f04632c0297/src/pseudo_normed_group/category.lean#L451

There is also a lot of room for cleanup + deduplication in this file. If anyone has time and wants to take a crack at these sorry's and/or do some cleanup, that would be very helpful! I'm done for today and have a full day of teaching tomorrow, so I won't be able to come back to this until later this week (hopefully).

[Kevin Buzzard]

I haven't done any research level Lean for a long time now (I've just spent two months helping UGs to do Lean, and this finished a few days ago) so I might well have a look at these tomorrow (afternoon UK) (but if someone else wants to have a go at these before then, feel free!)

[Adam Topaz]

After sleeping on this, I wonder whether cone_point_type here
https://github.com/leanprover-community/lean-liquid/blob/00980af145fe97427c31ce919b11633dd2c4800c/src/pseudo_normed_group/category.lean#L113
should be defined explicitly (i.e. as a quotient of a sigma type whose terms are subtypes of a pi type, mimicking the explicit description of colimits/limits in Type). This would probably help to make things true by definition as opposed to using, e.g., the stuff from
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/concrete.lean

@Johan Commelin what do you think?

[Adam Topaz]

Although

ef cone_point_type : Type u :=
colimit (cone_point_diagram G ⋙ lim ⋙ forget _)

is a nice definition, I think.

[Johan Commelin]

I'll take a look. Although I think that @Scott Morrison has much better feeling for how to setup these things.

[Adam Topaz]

If all we care about at the end of the day is the fact that some category has limits, then it shouldn't really matter. But if we need to actually say something explicit about the elements of these limits, then we should probably set up the theory as explicitly as possible.

[Johan Commelin]

Right, mathlib does have such explicit constructions for other concrete categories as well. So it might make sense to do the same thing here.

[Kevin Buzzard]

I've just been reading this stuff in an attempt to get back into the loop. It's not just that the category we're interested in is concrete, it's that the actual category itself is defined using bundled. Do we have some sort of way of going from an explicit unbundled construction of limits in, say, groups (stated as a definition plus a theorem claiming a universal property expressed in the language of monoid_homs between groups) to a construction of limits in Group := bundled group?

[Adam Topaz]

It's not quite bundled in this case.

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/00980af145fe97427c31ce919b11633dd2c4800c/src/pseudo_normed_group/category.lean#L50

[Kevin Buzzard]

Then is it in our interests to make both objects and morphisms bundled?

[Adam Topaz]

We added the exhaustive condition on the filtration, which is not required from the typeclass.

[Adam Topaz]

The goal of this stuff is to be able to take a functor from Fintype to CompHausFiltPseuNormGroup_1 and extend it to a functor from Profinite by taking limits in the category CompHausFiltPseuNormGroup_1. We will then compose with the functor to CompHausFiltPseuNormGroup (without the _1), and eventually a functor from CompHausFiltPseuNormGroup to Cond Ab.

[Adam Topaz]

As far as I know, mathlib doesn't have a construction of limits outside of category theory, except for very special things like products, so I'm not really sure what you mean @Kevin Buzzard about taking limits of groups in an unbundled context.

[Kevin Buzzard]

I mean proving "limits exist in the category of groups" without ever mentioning categories and just formalising it using group, and then a magic function turns this into existence of limits in the category

[Adam Topaz]

How would you specify a diagram for which you want to take a limit without using a functor?

[Adam Topaz]

The closest thing we have to this is what Johan was saying above, that in certain explicit concrete categories we have an explicit description of (co)limits, e.g. docs#Group.limit_group

[Kevin Buzzard]

Meh, I was just thinking of using a poset but of course a general limit will be more general :-/ It would work for products but not limits.

[Adam Topaz]

Anyway, I think I'm convinced that it's worth trying for an explicit construction. I'll try to change this soon

[Adam Topaz]

I made some more progress here, and I remade the definitions much more explicit (hopefully this will be helpful in the future. At least for now, we can prove more things by refl).

The last few sorry's should be doable, in case anyone wants to give it a shot.
https://github.com/leanprover-community/lean-liquid/blob/7b651c4e6d56756d472aa68009606cb4146c3fe3/src/pseudo_normed_group/category.lean#L598

(This is in the branch explicit-comphaus...)

[Adam Topaz]

Okay,

instance : has_limit G := has_limit.mk ⟨limit_cone _, limit_cone_is_limit _⟩

instance : has_limits CompHausFiltPseuNormGrp₁ :=
⟨λ J hJ, { has_limit := λ G, by resetI; apply_instance }⟩

are sorry-free.

Next up we should construct the functor from CompHausFiltPseuNormGroup to Cond Ab.