pseudonormed hierarchy

Stream: condensed mathematics

[Johan Commelin]

We have pseudonormed groups. For the second part, it will be useful to have pseudonormed rings as well.
It's not clear to me whether this should move to mathlib at some point. But it looks like it will be useful to develop (at least a partial) hierarchy of pseudonormed foobars.

[Adam Topaz]

We seem to have docs#semi_normed_comm_ring

[Adam Topaz]

What other foobars do we need?

[Adam Topaz]

Oh nevermind, I guess you really do mean pseudo and not semi.

[Johan Commelin]

Right, so we want rings $R$ with a filtration but subsets $R_c$ ($c \in \R_{\ge 0}$), such that

• $0 \in R_c$
• $-R_c = R_c$
• $R_{c_1} + R_{c_2} \subset R_{c_1 + c_2}$
• $R_{c_1} \cdot R_{c_2} \subset R_{c_1c_2}$,

[Johan Commelin]

Ooh, and probably $1 \in R_1$ ?

[Adam Topaz]

It feels like there is some general thing underlying such structures here, something between a seminorm and a bornology...

[Johan Commelin]

Scott had this categorical remark right? That these things were some sort of monoidal functors or something.

[Adam Topaz]

Right, but I don't see how the pseudo-normed rings would fit with that point of view

[Eric Wieser]

Does mathlib or LTE have any form of filtered algebras right now?

[Adam Topaz]

@Eric Wieser these objects are of a somewhat different nature -- $R_c$ are not even additive subgroups.

[Johan Commelin]

I guess it makes sense to develop a bit of pseudonormed (add_)monoids, and plug that before the stuff on pseudonormed add_groups that we already have. And then combine all of this into pseudonormed (semi_)rings.

[Johan Commelin]

We will also want to have pseudonormed condensed foobars. This brings a question to the front that we've had some discussions about in the past, but now we need to get serious about it: how do we model (pseudonormed) groups/rings/monoids/modules in a topos?

Is a sheaf of abelian groups a sheaf with values in the category Ab, or do we want an abelian group object in the sheaf topos?

@Mario Carneiro Do you have any wisdom to inject in this design decision?

[Peter Scholze]

To my naive eyes, defining it as an abelian group object sounds like one has to rebuild all the definitions from scratch. Defining it as a sheaf with values in some category makes it look more like diagrams of known things, so one probably doesn't have to rebuild so much.

On the other hand, it may be that some more subtle things will be easier with the "internal" definition...

[Kevin Buzzard]

There has been discussion on the Discord about the merits of defining condensed abelian groups as group objects in condensed sets v functors to groups.

[Peter Scholze]

What was the conclusion?

[Bhavik Mehta]

My take is that we want to define it as a sheaf with values in Ab, and prove an equivalence to the internal version

[Adam Topaz]

Woudn't the dream be to be able to write something like

variables (A : CondensedType) [condensed_add_comm_group A]
...

[Johan Commelin]

That looks very tempting, especially if we can invoke some topos-meta-tactic-fu to port the entire (constructive part of the) algebraic hierarchy over to internal algebraic hierarchies in a topos.

[Johan Commelin]

But I'm not very well-versed in topos-meta-tactic-fu.

[Peter Scholze]

Maybe this will be the time when the Coq and Lean communities will come together ;-)

[Adam Topaz]

Does coq have topos-meta-tactic-fu?

[Peter Scholze]

@Adam Topaz Wouldn't the dream rather be variables (A : CondensedType) [add_comm_group A]?

[Peter Scholze]

I don't know, but they do make the point that everything they do automatically ports to any topos

[Johan Commelin]

@Cyril Cohen Do you have experience with auto-porting stuff from Type to a topos? (In our case we want to work with a very specific topos, not just an arbitrary one.)

[Cyril Cohen]

Johan Commelin said:

Cyril Cohen Do you have experience with auto-porting stuff from Type to a topos? (In our case we want to work with a very specific topos, not just an arbitrary one.)

:joy: :joy: I may have plans for that
If you internalize (parts of ?) the lambda calculus and/or tactics, then I guess you can replay the normal proof scripts inside your topos :shrug:

[Bhavik Mehta]

There was quite a bit of discussion about these things a while ago (perhaps @Reid Barton can chime in), see eg https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/externalization and also very recent discussions on this in the discord, I think auto-porting results in Lean as it stands is hard. Firstly we'd need to figure out how to take existing Lean proofs and interpret them in a topos, which would involve some nontrivial meta code), but also have enough topos theory to work with these things in practice

[Bhavik Mehta]

I think in my topos project I had just enough to interpret some parts of dependent type theory, but no guarantees that it's usable. I remember Reid also had some concerns that pullbacks might not behave nicely enough (eg that pulling back twice isn't the same on the nose as pulling back along a composition) for dependent type theory to work nicely internal to a topos in Lean

[Johan Commelin]

@Cyril Cohen You are also involved in this hierarchy builder project, right? Could that be put to use here?

[Johan Commelin]

Of course it would create a hierarchy that is a priori disjoint from the existing one in mathlib. Which will probably bite us.

[Cyril Cohen]

Yes, the hierarchy would be disjoint. But maybe you can generate them quantifying on an abstract topos and use them in Lean? I don't know

[Bhavik Mehta]

Ah here's the full thread: https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/How.20to.20get.20HoTT.20people.20into.20Lean/near/197486222, specifically https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/How.20to.20get.20HoTT.20people.20into.20Lean/near/197495583

[Johan Commelin]

@Bhavik Mehta thanks for digging up all those pointers

[Bhavik Mehta]

This is something I've dreamt about having in Lean for years :D

[Bhavik Mehta]

There's one approach I've been discussing with @Ken Lee which I feel might be accessible as well as useful: defining an internal monoid on X : C as Π δ, monoid (δ ⟶ X) such that precomposition is a monoid hom. Then we can automatically re-use all of mathlib's algebraic hierarchy, specifically it's easy to generalise this to internal rings, modules etc without a lot of boilerplate code; and we can then work with generalised elements in a category as if they're just elements of some type

[Bhavik Mehta]

This doesn't let you auto-port all results, but I think it could make it easy to transfer results: for instance here when I defined internal natural numbers in a cartesian closed category, the proof of some lemmas were just "unfold definitions then repeat the natural numbers proof", and some were almost exactly a natural numbers proof including using ring

[Bhavik Mehta]

Admittedly that file as a whole isn't a great example since it has muddled APIs for natural number objects, generalised elements all in one; ideally it should be three separate files

[Johan Commelin]

One thing that might help with guiding our decision is actually how to define pseudonormed insides a topos.

• We could work with sheaves taking values in pseudonormed foobars
• We could work with families of subobjects. Here we have two options:
  • Using the subobject API developed by Bhavik. I think this will give a feel that is pretty close to the handson definition that we have in Type
  • Using families of objects and compatible monomorphisms between them. I fear that we will quickly run into a huge slew of canonical isomorphisms that aren't defeqs.

[Adam Topaz]

I was actually wondering about this. Consider the category of pseudonormed sets. Is it possible to define, say, pseudonormed groups as something like an abelian group object in this category?

[Adam Topaz]

(The answer is, of course, no. E.g one has to specify that the operation is additive and hence use addition on the reals which index the filtration.)

[Johan Commelin]

Does it make sense to generalize the indexing set of the filtration?

[Johan Commelin]

To something like linearly ordered commutative groups with zero?

[Adam Topaz]

For the case of pseudonormed rings, it seems we really need an ordered semiring as the indexing type

[Johan Commelin]

Good point.

[Adam Topaz]

Modulo the distinction between rings and semirings, it seems that the indexing type for a pseudonormed foo should be an ordered foo

[Damiano Testa]

Why ordered foo? Isn't the order on the filtration determined by inclusion of sets?

[Damiano Testa]

Maybe foo below is enough?

[Johan Commelin]

@Damiano Testa You want $V_{\le c_1} \subset V_{\le c_2}$ for $c_1 \le c_2$.

[Damiano Testa]

Oops, sorry! My mistake! And we did not even need Lean to expose this one!

[Damiano Testa]

Maybe I should not add another comment, but, if the base of the filtration satisfieshas_exist_add_of_le, then the inclusion is a consequence of the remaining containments, right? If a ≤ b, then b = c+a (by exist_...), so R_b contains R_c + R_a and R_c contains 0. If the hypothesis that Johan mentioned is the only place where an order of the filtering foo plays a role, it may not be needed that there is an order on it. I'm not sure if this is useful or not, but it is less structure to carry around, if the eventual application is with ℝ≥0.

[Damiano Testa]

At least, this might allow to split the arguments into a multiplicative one, the corresponding to_additive and a further layer dealing with a monotone map of ordered stuff, right?

[Peter Scholze]

I think I agree with Damiano's comment. In fact, I never explicitly asked for this monotonicity (but did check for myself that it follows, as Damiano observes)

[Damiano Testa]

While we are at it, should the union of the R_a equal R? I guess that I always assume this in my mental picture, but it probably should be a requirement, right?

[Adam Topaz]

How would this work for, say, pseudonormed multiplicative monoids?

[Adam Topaz]

don't we need to be able to say something like $1 \in R_a$ if $1 \le a$?

[Adam Topaz]

There might be a trick along the lines that Damiano is suggesting, but I don't see it.

[Peter Scholze]

Hmm. Good question. I never considered the purely multiplicative version... it seems a bit strange.

[Peter Scholze]

@Damiano Testa I didn't put the condition as I didn't need it, even though it's satisfied in all examples.

Generally, feel free to change the definition to what you feel is best or is most easily formalized.

[Damiano Testa]

Adam, I had not fully developed the idea of splitting algebraic operations and order, it just seemed like it might be a good way of separating different parts of the argument. I am not sure what is a good answer to your question on monoids. With the additive version, you can invoke the "opposite" axiom, but the multiplicative version seems trickier...

[Damiano Testa]

Maybe this is one of those cases where you might want to assume the monotonicity in general, since in the applications you have it...

[Damiano Testa]

Peter, interesting that the condition on the union is not needed!

[Damiano Testa]

Anyway, I'm off to bed: good night all!

[Peter Scholze]

I guess that's like an enorm, that can take the value $\infty$.

[Damiano Testa]

Mostly for my own sake, I thought of making a definition. Feel free to disregard!

import algebra.algebra.basic

variables {R F : Type*} (filtr : F → set R)

class mul_filtr [has_mul R] [has_mul F] :=
(mul : ∀ f₁ f₂ : F, (filtr f₁) * (filtr f₂) ⊆ filtr (f₁ * f₂))

class add_filtr [has_add R] [has_add F] :=
(add : ∀ f₁ f₂ : F, (filtr f₁) + (filtr f₂) ⊆ filtr (f₁ + f₂))

attribute [to_additive] mul_filtr

class semiring_filtration [semiring R] [semiring F] [add_filtr filtr] [mul_filtr filtr] :=
(zero_mem : (0 : R) ∈ filtr (0 : F))
(one_mem : (1 : R) ∈ filtr (1 : F))

class filtration [ring R] [ring F] [add_filtr filtr] [mul_filtr filtr] :=
(neg : ∀ f, - filtr f = filtr f)
(one_mem : (1 : R) ∈ filtr (1 : F))

[Johan Commelin]

That indeed looks like the thing we want in Type. Next challenge: wite these defs in Cond :lol:

[Damiano Testa]

At least, I am glad that I learned enough Lean to formulate the easy version of definitions!

[Johan Commelin]

Maybe sheaves of modules are a good example to keep in mind. A sheaf of rings/abelian groups can be described in two ways: as a sheaf taking values in the category of rings/abelian groups, or as a ring/ab_group object in the category of set-valued sheaves.
But if you have a sheaf of rings $\mathcal O$, then a sheaf of $\mathcal O$-modules is not a "sheaf valued in foo-modules" (I guess you could take values in $\sum_R \mathrm{Mod}_R$, but that will be a tricky definition). So a sheaf of modules seems to push us in the directions of "module object over the ring object $\mathcal O$".

[Kevin Buzzard]

Note that we still don't have sheaves of modules in mathlib.

[Kevin Buzzard]

Note also that the sigma type trick is what we ultimately used when defining the structure sheaf on an affine scheme (we defined sections on U\sub Spec(R) to be a map from U to the disjoint union of the R_P with some properties -- this is not the definition in the stacks project

[Scott Morrison]

I thought we had all the ingredients available to say:

[Scott Morrison]

• A ring is a monoid object in Ab, so
• A sheaf of rings is the same as a sheaf of monoid objects in Ab
• A sheaf of monoid objects in C is a monoid object in sheaves in C
• Hence a sheaf of rings is a monoid object in sheaves in Ab
• and we have module objects for monoid objects, hence we have sheaves of modules?

[Scott Morrison]

I haven't looked at this recently, maybe one or more of these ingredients is still missing.

[Johan Commelin]

@Scott Morrison Ooh, I forgot that we already had module objects!
Anyway, I guess that we will still need a bit of API around this to make it usable. Stacking all those constructions on top of each other, it will be quite annoying (for example) to write down $M(S)$ for some sheaf of modules $M$.

[Scott Morrison]

Yes, I agree this is only a "in principle the definition can be built out of existing lego" statement, nothing stronger about that being a good idea. :-)

[Scott Morrison]

somewhat similar to Adam's singular_homology definition :-)

[Bhavik Mehta]

Scott Morrison said:

• A ring is a monoid object in Ab, so
• A sheaf of rings is the same as a sheaf of monoid objects in Ab
• A sheaf of monoid objects in C is a monoid object in sheaves in C
• Hence a sheaf of rings is a monoid object in sheaves in Ab
• and we have module objects for monoid objects, hence we have sheaves of modules?

I don't think we have your second point or third point yet? I'd definitely like to see these though

[Adam Topaz]

Do we even have the tensor product of sheaves in Ab?

[Adam Topaz]

I'm assuming we don't, since we can't sheafify yet.

[Scott Morrison]

Hmm, okay. I was being wildly optimistic. I'm hoping to get back to mathlib soon, maybe I'll look in this direction for a bit.