for_mathlib/wide_pullback

Stream: condensed mathematics

[Johan Commelin]

Is there a reasonable generalization of https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/wide_pullback.lean ?

[Adam Topaz]

@Bhavik Mehta had a WIP PR in this direction a while ago, which is why I've been holding off on PRing this file

[Adam Topaz]

I guess for now we can just use the fact that the forgetful functor to types preserves limits.

[Adam Topaz]

So we could prove something for any concrete category where the forgetful functor preserves limits

[Bhavik Mehta]

Yup, this is what my PR #7436 should do, it covers concrete categories where the forgetful functor is representable (this is a stronger condition than preserving limits, but it covers Profinite as well as most of the concrete categories in mathlib) - I've already cut up and PR'd parts of it since it was getting too large

[Adam Topaz]

@Johan Commelin @Bhavik Mehta How would you like to proceed here? It might be worthwhile to add something about concrete categories where forget preserves limits, because it's a priori more general. I could try to cook up a PR this afternoon if it helps.

[Johan Commelin]

I don't have a strong opinion. I guess both approaches are useful in the end. So let's just have both.

[Bhavik Mehta]

Adam Topaz said:

Johan Commelin Bhavik Mehta How would you like to proceed here? It might be worthwhile to add something about concrete categories where forget preserves limits, because it's a priori more general. I could try to cook up a PR this afternoon if it helps.

Do you know any examples of concrete categories where forget preserves limits but isn't representable?

[Bhavik Mehta]

Johan Commelin said:

I don't have a strong opinion. I guess both approaches are useful in the end. So let's just have both.

I think the breakdown is like this: if the forgetful functor creates limits, it should be easy to show a particular cone is a limit; if the forgetful functor is representable, it should be easy to construct elements of limits; if the forgetful functor preserves limits, it should be easy to show elements of the limit are equal. The original code does the latter (and I presume this is what Adam plans to do) and my PR does the middle, I think all are worth having

[Adam Topaz]

#8130

[Adam Topaz]

I assume that we already have the fact that the forgetful functor from Profinte to Type*preserves limits, but I'll double check this later today and add it if it's missing

[Adam Topaz]

Turns out I had to add that forget Profinite preserves limits (which is now done in the same PR)

[Adam Topaz]

I just bumped and used the new docs#category_theory.limits.concrete.wide_pullback_ext' in one of the lemmas about the Cech nerve, and it seems pretty reasonably usable. I might have a go at cleaning up for_mathlib/wide_pullback.leanif I find some time later.

[Adam Topaz]

Alright, for_mathlib/wide_pullback is gone!

[Johan Commelin]

great! thanks a lot!