abstract nonsense about pseudo-normed groups

Stream: condensed mathematics

[Scott Morrison]

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 ℝ≥0is 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]

(It seems the Tinv action has a nice interpretation in this set up, too.)

[Scott Morrison]

(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]

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

[Adam Topaz]

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]

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

[Damiano Testa]

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]

So what's a pseudo-normed monoid?

[Johan Commelin]

A pseudo-normed group minus the neg axiom?

[Kevin Buzzard]

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

[Peter Scholze]

Now you're just making up words, right?

[Peter Scholze]

@Scott Morrison I like this nonsense!

[Johan Commelin]

Do we ever even use the negation?

[Scott Morrison]

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]

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

[Scott Morrison]

Call these the "lax groupoidal functors"!

[Scott Morrison]

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

[Scott Morrison]

But I absolutely haven't checked this.

[Scott Morrison]

Just thinking out loud, so probably actual nonsense.

[Scott Morrison]

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]

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

[Johan Commelin]

We only apply it to f = g + _ anyways

[Peter Scholze]

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]

yeah, that's totally true

[Johan Commelin]

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

[Peter Scholze]

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]

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]

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]

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]

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]

@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]

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.

[Filippo A. E. Nuccio]

Do we have the notion of equivalence between png? I am in particolar looking for a statement like

lemma foo (M1 M2 : Type*) [pseudo_normed_group M1] [pseudo_normed_group M2] (h : M1 ≃ M2) (c : ℝ) :=
  filtration M1 c ≃ filtration M2 c :=

but of course Lean wants to know what M1 ≃ M2 means. Also... do we have the above lemma?

[Johan Commelin]

I see that we have the following functor:

src/pseudo_normed_group/category/ProFiltPseuNormGrpWithTinv.lean
84:-- @[simps] def Filtration (c : ℝ≥0) : ProFiltPseuNormGrp ⥤ Profinite :=

[Johan Commelin]

And it's even commented out

[Johan Commelin]

But you would want a more general version anyways

[Filippo A. E. Nuccio]

Let me have a look at it

[Filippo A. E. Nuccio]

Well, may be actually playing with f.level would be enough for my purpose, no?

[Filippo A. E. Nuccio]

I guess that there f is a PNGWTinv-morphism.

[Johan Commelin]

There should be a version of level in a more general setting

[Johan Commelin]

src/pseudo_normed_group/basic.lean
163:@[simps] def level {M₁ M₂ : Type*} [pseudo_normed_group M₁] [pseudo_normed_group M₂]

[Filippo A. E. Nuccio]

OK, I'll try to work with it, thanks.

[Adam Topaz]

I'm fairly sure I defined a functor called level (or some other approximation) from PFPNG_1 to Profinite