# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: abstract nonsense about pseudo-normed groups

#### Scott Morrison (Apr 16 2021 at 01:12):

I noticed that if you forget the axioms involving subtraction in a pseudo-normed group, a pseudo-normed group is "just" a lax monoidal functor from `ℝ≥0`

to `Type`

, where `ℝ≥0`

is thought of as a monoidal category with homs given by `≤`

and tensor product is addition.

Since generally a monoid is the same thing as a lax monoidal functor from `punit`

to `Type`

, another way to say this is that a pseudo-normed group is a "`ℝ≥0`

-shaped generalised monoid".

However I can't work out how to build subtraction into this model. Has anyone thought about this and knows a solution?

#### Scott Morrison (Apr 16 2021 at 01:13):

(It seems the `Tinv`

action has a nice interpretation in this set up, too.)

#### Scott Morrison (Apr 16 2021 at 01:19):

(To fill in some details of the "just" claim above, this ignores the part of a pseudo-normed group that can't be seen in any filtration. Such a lax monoidal functor gives `F.obj x`

, some type for each `x : ℝ≥0`

, and coherent morphisms `F.obj x ⟶ F.obj y`

for `x ≤ y`

. I guess there's no reason, however, these need to be injections; but this is easily fixed if important. The unitor gives a morphism `punit ⟶ F.obj 0`

, picking out the zero element. The tensorator gives morphisms `(F.obj x) × (F.obj y) ⟶ F.obj (x+y)`

, which we interpret as addition. The naturality of the tensorator ensures that it's "the same" addition when you think of elements as living in later types. Associativity and unitality of addition come from exactly the same axioms for a lax monoidal functor.)

#### Adam Topaz (Apr 16 2021 at 02:02):

Can't you encode subtraction as some involution of this functor?

#### Adam Topaz (Apr 16 2021 at 02:16):

Of course, if you encode negation this way, then some axiom has to be written down to ensure the correct compatibility with the tensorator and unitor

#### Scott Morrison (Apr 16 2021 at 03:57):

Yes, I was hoping that duals or dagger structures or something similar would help, but neither fits.

#### Damiano Testa (Apr 16 2021 at 05:27):

I had never heard of unitor and tensorator before, but is what you are thinking about some form of Grothendieck group? If you started with `ℝ`

instead (or along with) `ℝ≥0`

, would the extra types be any help?

This is probably nonsense, but I would like to understand this more!

#### Kevin Buzzard (Apr 16 2021 at 06:22):

So what's a pseudo-normed monoid?

#### Johan Commelin (Apr 16 2021 at 06:26):

A pseudo-normed group minus the `neg`

axiom?

#### Kevin Buzzard (Apr 16 2021 at 06:39):

Right -- but is it equal to a lax monoidal functor? Maybe we should be considering lax groupoidal functors

#### Peter Scholze (Apr 16 2021 at 07:39):

Now you're just making up words, right?

#### Peter Scholze (Apr 16 2021 at 07:40):

@Scott Morrison I like this nonsense!

#### Johan Commelin (Apr 16 2021 at 07:42):

Do we ever even use the negation?

#### Scott Morrison (Apr 16 2021 at 07:42):

People are about to arrive for dinner here (yay no covid in Australia) but I think you can make sense of "lax groupoidal functor". Just like the lax monoidal functors are the monoid objects in functors (equipping functors with Day convolution as the tensor product), when the target is Cartesian I guess you can look at the group objects in functors.

#### Johan Commelin (Apr 16 2021 at 07:43):

Certainly in some specific examples, but not in the general theory, I think

#### Scott Morrison (Apr 16 2021 at 07:43):

Call these the "lax groupoidal functors"!

#### Scott Morrison (Apr 16 2021 at 07:43):

Now a lax groupoidal functor from nonneg reals to Type is hopefully a pseudo normed group.

#### Scott Morrison (Apr 16 2021 at 07:43):

But I absolutely haven't checked this.

#### Scott Morrison (Apr 16 2021 at 07:44):

Just thinking out loud, so probably actual nonsense.

#### Scott Morrison (Apr 16 2021 at 07:44):

I was going to ask, Johan, if you actually use negation! I did try to delete it from some files and got stuck on a pi instance.

#### Johan Commelin (Apr 16 2021 at 07:45):

We might need to restate the homotopy axiom, so that it doesn't mention `f - g`

:grinning:

#### Johan Commelin (Apr 16 2021 at 07:45):

We only apply it to `f = g + _`

anyways

#### Peter Scholze (Apr 16 2021 at 07:52):

Isn't negation used a lot when these things are plugged into BD resolutions? The BD matrices all have integral (quite possibly negative) coefficients

#### Johan Commelin (Apr 16 2021 at 07:53):

yeah, that's totally true

#### Johan Commelin (Apr 16 2021 at 07:54):

So as soon as we start building complexes we really want negation

#### Peter Scholze (Apr 16 2021 at 08:21):

I'm a bit confused about the "lax groupoidal functors". Considering the Day convolution interpretation, one has a symmetric monoidal category, and of course one can consider the monoid objects in there. But it's monoids with respect to the symmetric monoidal structure, and I'm not sure what it means to be a group object in a symmetric monoidal category. If the symmetric monoidal structure is the cartesian product, this is of course possible, but I don't think we're in this situation (even if the target of the functors has the cartesian structure).

#### Kevin Buzzard (Apr 16 2021 at 08:22):

When I was doing group cohomology in Lean with my class a month ago my instincts were to drop as many assumptions as I could, so initially I started with a monoid acting on an abelian monoid, and then I saw how far one could go. For H^0 you're fine, and the monoid never really needs to be upgraded to a group (you're doing Ext for the monoid algebra rather than the group algebra) but minuses appear in the abelian monoid the moment you move beyond H^0. You can avoid them for a while, e.g. don't define d on 1-chains (which involves a minus) but instead just define a 1-cocycle by putting things on the correct side of the equation so you don't need subtraction. However 1-coboundaries already involve subtraction, as does the boundary map from 0-cocycles to 1-cocycles, so it pretty quickly becomes hopeless. Subtraction gives you this really important "homogeneity" property which groups have and monoids lack. For example injectivity of a map of monoids is not controlled by the kernel (consider the map from the naturals to {0,1,2,3} where x+y=3 in the monoid if it's >= 3 in the naturals; trivial kernel but not injective). The concept of A -> B -> C being exact makes sense for abelian additive monoids but I'm not sure it's a useful idea, for this reason. A short exact sequence of abelian groups 0 -> A -> B -> C -> 0 is a way of saying "the monic with target B and the epic with source B are canonically related" -- this is the key extra symmetry which has been exploited so much in an abelian category -- an epimorphism from B is "the same as" a monomorphism into B, and this seems to be the key thing you lose the moment you drop inverses.

#### Scott Morrison (Apr 16 2021 at 12:13):

Peter, I agree that I was wrong here. Even if we're looking at functors into Type, where the symmetric monoidal structure is the cartesian one, that's not true of the Day convolution monoidal structure.

#### Peter Scholze (Apr 16 2021 at 12:27):

No worries! What you wrote still suggests that one ought to include a negation map on the functor, and this should satisfy some properties that are probably not so hard to guess. I'm just not seeing the right categorical context; but I also failed to see your very nice interpretation of the monoid portion!

#### David Michael Roberts (Apr 17 2021 at 03:16):

Since group cohomology is just secretly passing something about certain Kan complexes through some kind of possibly non-abelian Dold-Kan equivalence, to do it with monoids you need to go back and work with simplicial tools. Instead of a simplicial group you have a simplicial monoid, but this is not automatically a Kan complex underneath, so in principle one needs some kind of fibrant replacement as well. But for the purposes of elementary/naive attacks (esp for students), this is not helpful!

#### Kevin Buzzard (Apr 17 2021 at 08:57):

@David Michael Roberts are you talking about changing the $G$ in $H^n(G,M)$ to a monoid, or changing the $M$?

#### David Michael Roberts (Apr 21 2021 at 12:00):

I was thinking of both. But it really depends on what you want cohomology to measure. And what model category structure you use for (co)fibrant replacement.

Last updated: May 09 2021 at 23:10 UTC