LocallyConstant preserves colimits

Stream: condensed mathematics

[Adam Topaz]

I added a sorry'd instance that LocallyConstant.obj M preserves filtered colimits.
If anyone would like to help filling this in, it would be very helpful!
Here's the location:
https://github.com/leanprover-community/lean-liquid/blob/e3cf2a9a1c59eacf220860d1a67b65bef614133c/src/locally_constant/NormedGroup.lean#L59

[Adam Topaz]

On a somewhat note, it seems that mathlib is missing the dual to docs#category_theory.limits.preserves_limits_of_preserves_equalizers_and_products

[Scott Morrison]

Adam Topaz said:

On a somewhat related note, it seems that mathlib is missing the dual to docs#category_theory.limits.preserves_limits_of_preserves_equalizers_and_products

#7391

[Scott Morrison]

Adam Topaz said:

I added a sorry'd instance that LocallyConstant.obj M preserves filtered colimits.
If anyone would like to help filling this in, it would be very helpful!
Here's the location:
https://github.com/leanprover-community/lean-liquid/blob/e3cf2a9a1c59eacf220860d1a67b65bef614133c/src/locally_constant/NormedGroup.lean#L59

Did you have an informal argument in mind for this?

[Adam Topaz]

Scott Morrison said:

Did you have an informal argument in mind for this?

The rough idea I had in mind is this:

Unless I'm missing something, this assertion boils down to proving that any locally constant map $\lim_i X_i \to M$ (where the $X_i$ are profinite) factors through one of the $X_i$. I already proved that any locally constant map from a profinite set factors through a finite quotient here:
https://github.com/leanprover-community/lean-liquid/blob/f2ef6c5db252828b9733c2cda66795b15068048e/src/for_mathlib/Profinite/locally_constant.lean#L14
(Ignore the cocone def on that page, I don't think it's useful for this.)
So finally one should show that any finite quotient of $\lim_i X_i$ factors through one of the $X_i$, which should be doable given that we're working with a cofiltered system.

[Peter Scholze]

Incidentally, I think the claim is very close to what @Patrick Massot recently proved about extending maps from closed subsets

[Peter Scholze]

Or maybe I misunderstood. I thought you wanted to prove that for any cofiltered limit $X=\mathrm{lim}_i X_i$ of profinite sets $X_i$, the locally constant functions from $X$ to $M$ are the filtered colimit of the locally constant functions from $X_i$ to $M$.

[Peter Scholze]

But I think you only need the version where all $X_i$ are finite, which should indeed work in the way you write

[Adam Topaz]

Yes, I only need the version where the X_i are finite, that's right. But I think it works even with X_i profinite, no?

[Peter Scholze]

One way to deduce it in general would be to argue about Kan extensions from finite sets to profinite sets

[Adam Topaz]

Oh you mean that LocallyConstant.obj M is a right Kan extension along Fintype_to_Profinite?

[Peter Scholze]

Yes

[Johan Commelin]

Hah, so now you have a reason for a predicate version of Kan extensions (-;

[Adam Topaz]

Ping @Bhavik Mehta

[Johan Commelin]

Except that in LTE the type is def LocallyConstant : NormedGroup ⥤ Profiniteᵒᵖ ⥤ NormedGroup

[Johan Commelin]

Which is of course a bit specialised...

[Adam Topaz]

Yeah, but you can always precompose LocallyConstant.obj M with Fintype_to_Profinite

[Adam Topaz]

(or it's opposite)

[Adam Topaz]

And this is where the characteristic predicate would come in... it would show that LocallyConstant.obj M is isomorphic to the Kan extension of the composition

[Adam Topaz]

Well, unfortunately I have some grading to do :expressionless: , so I won't be able to work on this until that's done.

[Peter Scholze]

(If you try to do it naively in the case where the $X_i$ are profinite, you will run into the problem that $X\to X_i$ may not be surjective, not even in the pro-sense. So one can't argue about the question "does the map from $X$ factor over the quotient $X_i$"; rather factoring over $X_i$ is a priori more structure. One way to argue directly is to use what Patrick Massot proved, that maps to finite sets can always be extended from closed subsets. Alternatively, and this is what the Kan extension argument comes down to, you write any $X_i$ itself as a cofiltered limit of finite sets $X_{ij}$, use this to rewrite locally constant maps from $X_i$ in terms of maps from $X_{ij}$, and then go to $X$ via $X=\mathrm{lim}_{i,j} X_{ij}$.)

[Peter Scholze]

So @Adam Topaz I think for what you're trying to prove, maybe a useful first step is to prove that for fixed $i$ the image of $X_j\to X_i$ stabilizes for large $j$, and then agrees with the image of $X\to X_i$.

[Peter Scholze]

(Maybe this is more relevant for injectivity of $\varinjlim_i M(X_i)\to \mathrm{LocConst}(X,M)$ whereas you looked at surjectivity so far?)

[Adam Topaz]

I think it might be slightly easier to prove that this functor is isomorphic to the Kan extension, given what's already been formalized. I'm not sure. I'll have to think about this...

[Peter Scholze]

That may well be possible!

[Adam Topaz]

I'm confused...

Suppose I write $X = \varprojlim_i X_i$ with $X_i$ varying over the finite quotients of $X$, say, and let $M$ be a normed gorup. Consider $M(X)$, as well as the canonical maps $M(X_i) \to M(X)$. The claim is that $M(X)$ is the colimit of the $M(X_i)$.

So suppose that $N$ is another normed group endowed with morphisms $M(X_i) \to N$. The idea is to use the fact that for every $f \in M(X)$ there exists some $X_i$ (in fact the $X_i$ is unique in some sense) such that $f$ is in the image of $M(X_i) \to M(X)$. We then define the image of $f$ in $N$ to be the image of $f$ under the given map $M(X_i) \to N$. This is all fine, and one can show that this defines an additive map $\eta : M(X) \to N$.

My issue is with the norm. The claim is that there exists a constant $c$ such that for all $f \in M(X)$ one has $| \eta(f) | \le c \cdot |f|$. But a priori for each $f \in M(X_i) \subset M(X)$ there is a constant $c_i$ depending on $i$ such that $|\eta(f)| \le c_i \cdot |f|$. I don't see how to get a single $c$ that works for everything. If we instead work in the category of normed groups with norm nonincreasing morphisms, then this is not an issue as the constants $c_i$ can all be taken to be $1$.

Am I missing something obvious or do we need to work in the category with norm nonincreasing morphisms (to obtain a colimit)?

[Johan Commelin]

I guess you need bounds on the norms of the $M(X_i) \to N$.

[Johan Commelin]

So it won't be a colimit in general, I'm afraid :sad:

[Adam Topaz]

Sure, that's fine, but then it's not a cocone in the category NormedGroup

[Johan Commelin]

Sounds like we need to set up an API for StrictNormedGroup

[Adam Topaz]

Or NormedGroupNonInc

[Johan Commelin]

That's a better name, yes.

[Adam Topaz]

Do we have a (semi)normed_group instance on the homsets of NormedGroup? (edit: yes)

[Riccardo Brasca]

Yes, and in case you need it we also have a normed_group instance if both are normed groups.

[Adam Topaz]

So I would like to introduce this:

import normed_group.NormedGroup

namespace NormedGroup

open category_theory

universe u

structure bounded_cocone {J : Type u} [small_category J]
  (F : J ⥤ NormedGroup.{u}) extends limits.cocone F :=
(bounded : ∃ c : ℝ, ∀ j : J, ∥ ι.app j ∥ ≤ c)

structure is_bounded_colimit {J : Type u} [small_category J]
  {F : J ⥤ NormedGroup.{u}} (t : bounded_cocone F) :=
(desc : Π (S : bounded_cocone F), t.X ⟶ S.X)
(fac'  : ∀ (s : bounded_cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j . obviously)
(uniq' : ∀ (s : bounded_cocone F) (m : t.X ⟶ s.X) (w : ∀ j : J, t.ι.app j ≫ m = s.ι.app j),
  m = desc s . obviously)

restate_axiom is_bounded_colimit.fac'
attribute [simp,reassoc] is_bounded_colimit.fac
restate_axiom is_bounded_colimit.uniq'

end NormedGroup

[Adam Topaz]

As an alternative to working with the category of normed groups with non normincreasing morphisms...

[Johan Commelin]

How bad would it be to define NormedGroupNoninc?

[Adam Topaz]

Of course, the correct thing to do would be to introduce some new structure approximately like this:

class normed_category (C : Type u) extends category.{v} C, preadditive C :=
(norm : Π {X Y : C}, (X ⟶ Y) → ℝ)
(submultiplicative : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), norm (f ≫ g) ≤ norm f * norm g)
(triangle : ∀ {X Y : C} (f g : X ⟶ Y), norm (f+g) ≤ norm f + norm g)
(zero : ∀ {X Y : C}, norm (0 : X ⟶ Y) = 0)

and have an API for bounded (co)limits in such categories, but I don't know how useful that would be in other applications?

[Johan Commelin]

I think you can mostly just copy-paste the NormedGroup api.

[Adam Topaz]

Johan Commelin said:

How bad would it be to define NormedGroupNoninc?

It's not bad to define, but the arguments will have to go back and forth a lot between NormedGroupNoninc and NormedGroup, and I feel like it would get annoying fast!

[Johan Commelin]

Hmm, but defining bounded limits etc also sounds like it might get annoying fast...

[Peter Scholze]

Finding a good categorical framework for this kind of "normed homological algebra" is a question that's been bugging me quite a bit... I feel that Scott Morrison's realization on pseudonormed monoids may be relevant. Actually, just today, I was thinking again about a problem leading to questions about homological algebra with pseudonormed abelian groups, and I wished I knew how to think about it conceptually.

[Peter Scholze]

Making Hom's (pseudo)normed definitely seems to be part of it, and in what I was doing today, it may even be necessary to have some theory of "bounded (co)limits"...

[Adam Topaz]

The above definition can probably be seen as a category enriched over SemiNormedGroups or something like that...

[Adam Topaz]

For the problem at hand, the main annoyance I see about using NormedGroupNoninc is that the differentials in the Cech complex are not norm nonincreasing (as they involve some sums of norm nonincreasing morphisms), while the splittings (when the cover is split) are norm nonincreasing, and one wants to obtain exactness by taking some filtered colimits (and these colimits a priori only make sense if the homs in the diagram are all bounded by a single constant)

[Johan Commelin]

In the columns of thm95.double_complex those differentials are norm-noninc

[Johan Commelin]

Because we rescale the norms in every degree

[Adam Topaz]

So why even allow for non-norm-noninscreasing morphisms?

[Johan Commelin]

Because when you write down the complex for Mbar you need to take these equalizers to get the objects.

[Johan Commelin]

Before taking equalizers, the differentials in the complex are potentially norm-inc.

[Johan Commelin]

But only on the equalizers can you show that they are norm-noninc.

[Johan Commelin]

So we could, a posteriori, redefine it to be a complex in NormedGroupNoninc

[Johan Commelin]

But aiming for that category directly seemed really awkward. (And back when I was young I didn't realise we would hit all these subtleties like bounded colimits.)

[Adam Topaz]

So it sounds from @Johan Commelin 's comments that we need to be able to rescale the norm on objects, and compare such objects with objects constructed as colimits. So this only makes me think MORE that we should be thinking about bounded (co)limits. Note that there is no functor NormedGroup \to NormedGroupNoninc which is the "identity" on objects...

[Johan Commelin]

Hmm... @Adam Topaz is it helpful if I quickly walk you through what's happening in the construction of the double complex?

[Johan Commelin]

Then you know exactly what is going on there.

[Adam Topaz]

Yes, that would be helpful.

[Johan Commelin]

Let me quickly check when dinner is planned.

[Adam Topaz]

But I'll be busy for about an hour starting essentially now. Does 2021-04-29T10:15:00-06:00 work for you?

[Johan Commelin]

Hmm, not really. How about 1hr later?

[Adam Topaz]

2021-04-29T11:00:00-06:00 ?

[Johan Commelin]

I think that can work.

[Adam Topaz]

I added a definition of a semi_normed_category in the semi-normed-category branch of lean-liquid, in case anyone wants to experiment with it.

https://github.com/leanprover-community/lean-liquid/compare/semi-normed-category

[Adam Topaz]

This is a preliminary definition, but it has the components one needs to define "bounded" (co)limits.

[Adam Topaz]

Here is what bounded limits look like in a semi_normed_categetory:
https://github.com/leanprover-community/lean-liquid/blob/d99d114dd592be77492be2982898ccc62a974df7/src/for_mathlib/seminormed_category/limits.lean#L62

[Scott Morrison]

Your cone.bounded_by definition would ideally be (I don't actually see how to achieve this) just the statement that S.\pi itself is a bounded morphism in the functor category. I guess what is going on here is that you are actually thinking about limits in the two category of semi-normed-categories, semi-normed-functors and semi-normed-natural-transformations.

Perhaps there is a way to generalize the entire limits framework so that you don't need to do it by hand here.

Almost surely this would only be possible after we have 2-categories, of course!

[Adam Topaz]

If we define the norm of a natural transformation $\eta$ as the sup of the norm of \eta.app X as X varies, I think that cone.bounded_by c becomes the condition that the norm of C.\pi is bounded by c.

[Adam Topaz]

There's this notion of "weighted" limits for enriched categories. I wonder if this fits in that framework?

[Adam Topaz]

Scott Morrison said:

Perhaps there is a way to generalize the entire limits framework so that you don't need to do it by hand here.

Almost surely this would only be possible after we have 2-categories, of course!

One concern about trying to generalize the (co)limits framework to work in this more general 2-categorical context is that it would probably make universes even more restrictive when dealing with (co)limits, so I'm not sure this is the right approach...

[Scott Morrison]

Ooh, yes. :-(

[Peter Scholze]

Well I'm inclined to think that the problem at hand should not require new 2-categorical foundations :wink:

[Adam Topaz]

If we had some way to tell lean that the classes [semi_normed_category C], [norm_compat_functor F] and [bounded_natural_transformation \eta] were somehow related to eachother, there might be a way to use the typeclass system to simulate the 2-categorical approach without (additional) universe issues.

[Peter Scholze]

Actually, can someone spell out the math behind the 2-categorical approach?

[Peter Scholze]

I was getting a bit lost, as we are trying to do (co)limits in a specific category, not in a 2-category, so I'm not exactly sure what the proposal is

[Adam Topaz]

If I understand correctly, Scott was suggesting to replace all categories/functors/natural-transformations with semi_normed_categories/norm-compatible-functors/bounded-natural-transformations (which is really working in a specific 2-category of such things).

[Adam Topaz]

So a cone would become a bounded natural transformation of between certain norm-compatible functors, etc.

[Scott Morrison]

Instead of having some terminal natural transformation from F to a "constant X" functor, we only want something that is terminal amongst bounded natural transformations.

[Scott Morrison]

(ugh, my tos and froms are all wonky)

[Adam Topaz]

Is there always an analogue of a constant functor in any 2-category?

[Adam Topaz]

I guess one should model a constant functor as a 1-morphism from the one-point category sorry that's wrong

[Peter Scholze]

OK, yeah, I guess I see what is meant, thanks!

[Peter Scholze]

I would think about it in terms of adding a cone point to the index category

[Scott Morrison]

I wonder if (I think this is your suggestion above, Adam) we can just hack the existing limits set up to just ask for initial cocones amongst some class of cocones (i.e. the bounded ones).

[Adam Topaz]

Peter Scholze said:

I would think about it in terms of adding a cone point to the index category

Doesn't this break the idea that a cone is a bounded natural transformation?

[Peter Scholze]

Let me try to see whether I can formulate how I want to think about it, one second...

[Scott Morrison]

A colimit cocone for F : J \func C is "just" an initial object in the comma category for the two functors C \func (J \func C), the first of which sends everything to F, then second of which sends X to the constant-valued-X functor J \func C. In this description you can replace the category J \func C with the category of bounded functors and bounded natural transformations.

[Scott Morrison]

(And I think this is what you mean by bounded colimits.)

[Scott Morrison]

(Strangely this statement doesn't appear to be in mathlib...)

[Scott Morrison]

In particular if you do this replacement of J \func C, there's absolutely no mention of 2-categories, so we can do it today. :-)

[Bhavik Mehta]

Scott Morrison said:

(Strangely this statement doesn't appear to be in mathlib...)

I think this statement is ultimately about costructured arrows which (as you well know!) we only got in mathlib recently, which is why it's not there yet

[Bhavik Mehta]

I have a partial result in this direction, that if we have a functor (G : D ⥤ C) such that each category (comma (functor.from_punit A) G) has an initial object, then G is a right adjoint; I think specialising this to C = (J ⥤ D) and G as the diagonal functor gives one direction of the statement you're talking about?

[Adam Topaz]

Per the discussion above, I've updated the definition of bounded (co)cones to use norms on natural transformations.
https://github.com/leanprover-community/lean-liquid/blob/02ed3ed5e3031b72a5ebf658a352fc1fb1122cb7/src/for_mathlib/seminormed_category/functor.lean#L55

The bounds on bounded_cone.is_limit.lift, for example, now becomes:

lemma lift_norm_le {F : J ⥤ C} {t s : bounded_cone F}
  (h : t.is_limit) : s.cone.π.norm ≤ ∥ h.lift s ∥ * t.cone.π.norm :=