profinitely filtered pseudo normed topological groups

Stream: condensed mathematics

[Johan Commelin]

Currently, there are a lot of statements about Mbar and Mbar_le that should be generalised to something like the category of "profinitely filtered psuedo normed topological groups". In other words:

• topological groups $M$ with an increasing filtration $(M_c)_{c \in \mathbb R_{\ge 0}}$ such that
• $M_c$ is a profinite set
• $M$ is pseudo normed, so $0 \in M_c$, $-M_c = M_c$, and $M_{c_1} + M_{c_2} \subset M_{c_1+c_2}$

Morphisms of these gadgets should be continuous and bounded homs.

[Johan Commelin]

Are these things bornological? Can does continuity follow from boundedness, or vice versa?

[Johan Commelin]

Reason for the generalisation:

• deduplicate statements of 9.4 and 9.5
• functoriality will give the implication 9.5 -> 9.4.

[Adam Topaz]

Perhaps it makes sense to generalize this concept to more general categories, so that the profinitely filtered pseudo... is the special case for the category ProFin, and pseudo-normed abelian groups is the special case for the category Type?

[Johan Commelin]

Well, I was thinking of using the predicate for compact subsets (and requiring M to be Hausdorff, totally disconnected).

[Johan Commelin]

So then it's not very modular. But maybe easier to use, because there will be only 1 carrier type involved.

[Johan Commelin]

But we should definitely experiment a bit with different approaches.

[Adam Topaz]

Oh, I see, so the issue is that the "total space" is not profinite? Then just work in locally profinite spaces, or something?

[Adam Topaz]

Okay, I guess one has to think about how to combine these two concepts in a workable way, but I feel like we could deduplicate even more if we generalize enough.

[Johan Commelin]

Well, we only need pseudo normed groups of the special form that I outlined above, as far as I can see.

[Adam Topaz]

Ah, I see.

[Johan Commelin]

Another question that I didn't see an immediate answer to: do these profinitely filtered pseudo normed groups have an internal hom?
We already know that the type of group homs between pseudo normed groups is naturally a pseudo normed group. But will it's filtration sets be profinite, if this is true for source and target?

[Peter Scholze]

definitely not!

[Peter Scholze]

Profinite sets do not have internal Hom's; the internal Hom is very far from compact

[Johan Commelin]

Oooh right.

[Johan Commelin]

So we'll need some special work to make $\mathrm{Hom}(\Lambda, \overline{\mathcal M}_{r'}(S))$ into one of these objects.
But here it works, because $\Lambda$ is a lattice, hence discrete, and all the filtration sets are finite.

[Peter Scholze]

Well yes, but it's also not really an internal Hom (or is it?). The definition is a little hand-made....

[Johan Commelin]

Right

[Johan Commelin]

Grr, I don't know what the LateX parser is unhappy about. But I guess it's clear what I mean Hooray, I found the bad }

[Johan Commelin]

I'm currently playing around with formal definitions of the objects. Lean automatically puts a (subspace) topology on the filtration sets $M_c$, if we put a topology on $M$. But if the topology on $M$ is defined in terms of topologies on $M_c$ to start with, this means we now have two topologies on $M_c$, and Lean will get confused which one we mean. Of course we mean "who cares, they are equal", but that's not something Lean will accept.

[Johan Commelin]

So my current feeling is that maybe we should avoid putting a topology on $M = \mathrm{colim} M_c$.

[Peter Scholze]

Definitely!

[Peter Scholze]

If you ever want to take products, you will start worrying whether the product topology on $\mathrm{colim} M_c\times \mathrm{colim} N_c$ is the colimit topology $\mathrm{colim} M_c\times N_c$

[Peter Scholze]

This is true, but it's a nasty and useless lemma

[Johan Commelin]

Ok, that's a good example. (We have this with metric topologies in mathlib.)

[Peter Scholze]

But it's not a metric topology!

[Peter Scholze]

It's not any kind of standard topology for which you will likely have any API

[Johan Commelin]

No, I just meant that we have a similar "problem" there. If X and Y are metric spaces, then you can put the metric topology on $X \times Y$ or the product topology (of the metric topologies on $X$ and $Y$). To make this usable, we need to use a "trick". We put a separate topology on $X$, together with a proof that it is equal to the metric topology. And then on $X \times Y$ the proof that it's a metric space includes the lemma that the two aforementioned topologies agree.

[Peter Scholze]

Oh, I see. That's a neat trick! But I think it's best to avoid mention of the topology here.

[Kevin Buzzard]

Peter Scholze said:

That's a neat trick!

Ha! When I first saw it I was horrified! It is the canonical example of a "diamond" in type theory: the product topology equals the topology defined by the product metric, but this equality is not true by definition, so it breaks the system which is supposed to be keeping track of these things automatically unless you make this hack in the definition of a metric space to also also carry around a topology and a proof that the topology is induced by the metric. In fact I think nowadays we carry around the uniform space structure instead.

[Johan Commelin]

@Peter Scholze What about the homs in this category. They should be bounded and "continuous" group homomorphisms, right?

[Johan Commelin]

But phrasing what "continuous" means will be somewhat roundabout.

[Peter Scholze]

I thought the homomorphisms should be strict, i.e. map $M_{\leq c}$ into $N_{\leq c}$

[Peter Scholze]

Otherwise the formation of this $\hat{V}$-complex wouldn't even be functorial

[Peter Scholze]

And strict morphisms are necessarily continuous. I assume you automatically ask continuity of each $M_{\leq c}\to N_{\leq c}$...

[Johan Commelin]

Ok, that makes sense. I'm now happy with this approach.

[Peter Scholze]

@Kevin Buzzard Well, in higher category theory you learn that "the same" means "up to contractible choice". And you learn that it is often wise to enlarge a point to a larger contractible space to make enough space for certain arguments. So I don't find it bad to somehow enlarge "the topology on a metric space" into an interval.

[Peter Scholze]

What I mean to say is that I've seen similar hacks being used by pure mathematicians to justify certain arguments in higher category theory

[Kevin Buzzard]

Initially I was concerned that the system would not scale at all well (e.g. maybe we would have to put five auxiliary extra structures on every scheme in order to make things work) but this seems not to be the case.

[Kevin Buzzard]

Especially when I discovered that despite the fact that these systems had been around for decades, nobody had bothered to even try and test this by making schemes...

[Kevin Buzzard]

Part of the reason we formalised the definition of a perfectoid space was just to see whether this sort of issue actually turned the problem into a nightmare, or whether type theory really did work in practice as a foundation for mathematics beyond proving sqrt(2) is irrational and all finite groups of odd order were solvable. Turns out it did.

[Peter Scholze]

One thing I find mildly confusing about type theory is that its advocates claim that when you form say $1/x$ it automatically checks for you that $x$ is not zero, and that this is a very good thing. But in practice, things seem to be the other way around: You do not want to be bothered having to check that, so instead you simply define it to be some junk value in case $x$ is not as expected. I've seen many such hacks in the code now, and it makes me believe that this whole justification for type theory is not really sound

[Johan Commelin]

I agree. In practice it's an art to find the right balance.

[Johan Commelin]

I really view the type system as a tool. It can figure out a lot of things for me, because of the implicit information carried around by types. But sometimes it gets in your way, and then we resort to "junk-value hacks".

[Johan Commelin]

I think it is in some sense an "unsolved issue". Sometimes having "correctly typed" functions really makes life a lot harder. Sometimes it just makes the code very ugly to read. I think it's worth a lot that we can just write 1/x, instead of 1/<x, proof that x \ne 0>. If we could have solid automation deriving those proofs for us, then I would be a lot happier about using 1/x as notation for div 1 x (auto-inferred proof that x \ne 0).

[Johan Commelin]

But currently such automation is typically slow or brittle.

[Johan Commelin]

On the other hand, there are still lots of places where the type system prohibits us from writing nonsense.

[Peter Scholze]

Johan Commelin said:

On the other hand, there are still lots of places where the type system prohibits us from writing nonsense.

In the sense that this is actively helpful during the coding, catching stupid slips early on?

[Johan Commelin]

Yes, I definitely think so. Before you launch into the proof, you often already make a bunch of typos that you can immediately correct.

[Johan Commelin]

But also because it will just infer a lot of information.

[Peter Scholze]

OK, I see

[Johan Commelin]

For example, we can write x + y, which is in some sense quite a miracle. We don't have to explain to lean which + we mean all the time.

[Johan Commelin]

Lean sees x + y, and thinks: "now I need to figure out what + this is. So let's look up the type of x. Aha, that is R. Now let's look for has_add R in my database. Ok, there is some _inst_3 : ring R, and I know how to turn a ring into a has_add through a series of steps."

[Peter Scholze]

Aha, I see the point. That's great!

[Johan Commelin]

Similarly, if C : system_of_complexes and $x \in C_c^i$, we can just write C.d x, and Lean will figure out which differential we mean exactly.

[Johan Commelin]

It will be able to infer c and i from the type of x, namely C.X c i (if I got the order of c and i right...)

[Johan Commelin]

But that doesn't change the fact that you are completely right that 1/x is hacky.

[Johan Commelin]

On the other hand, when I work in set theory, I just ignore the issue. I never check (ok, maybe in 1% of the cases) that $x \ne 0$. And I think I'm not the only one who "cheats" like this.

[Kevin Buzzard]

When I was doing undergraduate example sheets there were questions about square roots of real numbers, and Lean did not have square roots at that time, and so I defined sqrt(x, [proof that x>=0]) to be the usual sup, and the computer scientists laughed at me for writing a function which took two inputs and then never used one of them.

[Kevin Buzzard]

Turns out that if you feed in a set S which has no sup into the sup function, it just returns some junk value. At the time I was horrified by this, but it had got to the stage where I knew enough about what I was doing to make my square root function work anyway, and I was adamant that it was the "correct" thing to do. In the mean time, the computer scientists (who presumably could see what was about to happen) implemented a square root function which returned the correct value for x>=0 and a junk value for x<0. I then started on the example sheet questions and they drove me nuts! I was constantly having to insert proofs that e.g. 2>=0, and in proofs showing stuff like sqrt(2)+sqrt(3)<sqrt(10) it soon got tiring.

[Peter Scholze]

Johan Commelin said:

Similarly, if C : system_of_complexes and $x \in C_c^i$, we can just write C.d x, and Lean will figure out which differential we mean exactly.

Wow! Even in my very "sloppy" notes, I felt the need to put more quantifiers.

[Johan Commelin]

Yup, but in VScode, you can click on the C.d in the "Goal window", and it will tell you exactly which c and i it inferred.

[Johan Commelin]

I think this is the start of where interactive theorem provers become interactive. There is a whole lot more that can be done here... and people are working on it. I'm excited about interactive diagram chases, etc...

[Patrick Massot]

The question of $1/0$ is all about "where do you want to put proofs?". We want to talk first and apologize later (and only if really needed), because it saves a lot of typing. So, given a field $k$, we define division as a function from $k \times k$ to $k$, without any precondition, and it satisfies $1/0 = 0$. This is a definition, it can't be wrong in the sense it cannot bring a contradiction by itself. Now of course Lean won't let prove $x \times 1/x = 1$ without asking for a proof that $x$ is non-zero. The lemma simplifying this expressions asks for a proof, the definition of $1/x$ doesn't. Note that apologizing is not always needed. For instance $(a+b)/c = a/c + b/c$ is true without any condition on $c$. That's because we've clearly chosen the "junk value" $a/0 = 0$. This is simply convenient in practice.

[Johan Commelin]

I like that slogan Patrick. "speak first, apologize later".

[Patrick Massot]

This has basically no mathematical content. The other trick that Johan mentioned (with metric spaces being a packages containing a distance function, a uniform structure and a proof of the fact that the uniform structure is compatible with the distance) does have some clarifying content. We met this in a slightly more sophisticated context while working on basic infrastructure for perfectoid spaces. An abelian topological group $G$ have a unique reasonable uniform structure. Now complete this uniform structure to get a new uniform space $\hat G$ and extend the group operations to $\hat G$. The new group operations are continuous. So $\hat G$ with its group structure and the topology underlying its uniform structure is a topological group. And now we have two uniform structures on $\hat G$: the one offered by the completion functor acting on all uniform spaces and the reasonable one on a topological group. These are the same uniform structure, but this is not obvious. Bourbaki proves they are the same, but this proof is pretty well hidden inside a long discussion. This subtlety is painful for Lean if not handled through the trick described by Johan. But I claim you also get added clarity by openly defining a compatibility condition between a group structure and a uniform structure and openly stating 1) given a topological abelian group there is a unique uniform structure which is compatible with both its group structure and its topology and 2) if a group structure and a uniform structure on $G$ are compatible then the group structure and the uniform structure on $\hat G$ are compatible.

[Peter Scholze]

I can totally relate to that second trick, but remain minimally perplexed by this $1/0=0$ thing. (Another reason I remain perplexed by it is that another reason type theory is supposed to be great is that in suitable versions of type theory, you have to work constructively/continuously/internally in a topos/whatever, and $1/0=0$ is a very discontinuous extension of $1/x$. I guess in such versions of type theory, this cheat wouldn't work?) But I'm derailing this conversation, and also should do other things...!

[Mario Carneiro]

The type theory purist would indeed argue that division should have the type div : \all (x y : R), y != 0 -> R. This concession to simple types is however very useful in practice. Personally I think it's great that lean has the tools to express very dependent types even if they are used only sparingly. We know that it's possible to get by with essentially no types at all (ZFC), but you get less assistance with type errors and typing when you have to do everything by hand. Lean (and mathlib specifically) represents a compromise on that spectrum, where lean can support very precise types but it's also okay to be a little inelegant sometimes and totalize when type purism hurts more than it helps.

[Mario Carneiro]

(Actually, the real purist would replace y != 0 with y # 0 using the apartness relation on the reals, but let's not get into that.)

[Johan Commelin]

I pushed a definition of the category.

[Johan Commelin]

The downside of making everything functorial is that we need to give things names that would usually be covered by notation.

[Johan Commelin]

We used to go from $\overline{\mathcal M}_{r'}(S)_{\le c}^m \to \overline{\mathcal M}_{r'}(S)_{\le c'}^n$ to

(Mbar_le r' S c)^m -> (Mbar_le r' S c')^n

But now this has to become a natural transformation between functors that raise things to the power m and n. And so we can't use the ^m notation.

[Johan Commelin]

But I don't see how to avoid this. We'll have to think about how to make it look good later.

[David Michael Roberts]

Peter Scholze said:

(Another reason I remain perplexed by it is that another reason type theory is supposed to be great is that in suitable versions of type theory, you have to work constructively/continuously/internally in a topos/whatever, and $1/0=0$ is a very discontinuous extension of $1/x$. I guess in such versions of type theory, this cheat wouldn't work?)

Yes.
Lean's logic is classical, so you are working in a Boolean topos, where the by-cases definition is fine. Alternatively, this 1/0=0 hack means implicitly you are working with a discrete field, not one of the more the general versions (eg a Heyting field, which uses #). In other proof assistants that stick more closely to the constructive world this hack would not be ok.

Kevin has publicly said this is a big plus for Lean, and for all the "generic" mathematics he wants to see done, as it is more optimal for usability vs purity.

[Kevin Buzzard]

The reason it doesn't work in constructive settings is that given a random term representing a real number, such as $\pi^2/6-\sum_{n\geq1}1/n^2$, there's no algorithm which tells you if it's zero or not, so constructively you can't make a definition starting "if $x=0$ then..."

[Peter Scholze]

@David Michael Roberts Thanks! I definitely side with Kevin on the question of constructivity, my love for (Grothendieck) topoi notwithstanding (sorry!...).

One reason I like sets is that they are an extremely primitive language: Extremely few basic sorts of objects and relations. But you can still base everything on them, and at some point you can put some higher level languages on top of them. Type theory is much less primitive, it seems to me -- I never quite understood what a type is, I think this also depends heavily on the precise setup, and what the primitive objects and relations are is a little in flux, I believe -- often you allow yourself to produce new "methods of forming types" at will(?). This seems more like the kind of thing you would like to do on top of other foundations, not in the foundations themselves. That types are closer to how you actually think is not an argument that they are better foundations, only that you want to have some interface that has some type-like behaviour. If I want to work in a general cartesian-closed topos or whatever, I should be free to say so, but I shouldn't be forced to from the start. (Back when I was coding in C++ in my early youth, I used to appreciate C++'s "pointers" with which you could access arbitrary points in memory. I think that's a little akin to asking whether $2$ is an element of $\pi$. I assume use of pointers, if at all allowed in current languages, is considered very bad form? But somehow in the end whatever the computer is doing is saved somewhere on memory, and the question "what is the bit at this point of memory" is always a well-defined question, although often not one you should be asking as it misses context. I feel the same about the foundations of mathematics -- type theory seems to be like a way of denying that there's actually some physical memory with actual bits somewhere.)

[Johan Commelin]

Ha, you sound the same as @Mario Carneiro (-;

[Johan Commelin]

He frequently says "types are an editor feature".

[Johan Commelin]

I think I agree with what you say. But to carry on with the analogy with programming languages (which is a good one, I think): programming languages with "strong" foundations, like Rust or Lean 4 can make huge compiler optimizations because they have a very strong set of assumptions on what can and cannot be done with memory. There are benchmarks that show that Lean 4 beats the C++ stdlib on lots of common tasks.

[Johan Commelin]

Of course mathlib is only a single data point. But the speed of growth of mathlib is tremendous compared to other libraries that have been around for decades. But who knows what Mario's Metamath Zero will accomplish. It's similar to what you describe. A low level language, with a type theory bolted on top (MM1).

[Peter Scholze]

Aha, that's great!

[Johan Commelin]

About your point of "methods of forming types". I think the list is not so long, and quite natural. Basically, we have $\Pi$-types and $\Sigma$-types.
And what I really like about type theory is that it merges the "set-theoretic" part of the foundations and the "logic" part. Because "sets are types" and "propositions are types". A function between sets $X \to Y$ uses the same machinery as an implication of propositions $P \implies Q$.

[Johan Commelin]

So that seems like a simplification to me, compared to the usual foundations.

[Peter Scholze]

yes and no. There's this whole hierarchy of $n$-truncated homotopy types: For $n=-2$, just the one-point set, for $n=-1$, the empty set and the one-point set, for $n=0$ all sets, and then you get into actual homotopy types. I can see the appeal of starting directly from all homotopy types and then specializing, but I have never seen a convincing proposal for how to do this -- I think this is largely what HoTT is trying to achieve (and I think it's a very interesting and important question). So I think it's fine to instead start building it up from below, and then going in one-by-one steps seems like the good thing, instead of jumping right to $n=0$ (why not $n=1$ and allow groupoids as well? Why not $n=2$? etc.)

[Johan Commelin]

I agree, and I'm certainly rooting for HoTT. Unfortunately there are still usability issues with HoTT in practice. Where "practice" means, in a formal theorem prover.

[Johan Commelin]

I pushed some wip on "continuous" maps between profinitely filtered pseunormgrps. There are some sorrys left. They are maths-trivial... but I need to have dinner first.

[Johan Commelin]

These sorrys are now done. I just realised that the objects in this category should also have an endomorphism $T^{-1} \colon M \to M$.

[Johan Commelin]

So, I'll need to modify everything a bit. By now I no longer know how to call these objects...

[Johan Commelin]

profinitely_filtered_pseudo_normed_group_with_Tinv is a bit... long

[Kevin Buzzard]

So you went with adding the topology to the abstract algebra? You could call them profinitely filtered pseudo normed modules

[Johan Commelin]

But that doesn't mention the T

[Johan Commelin]

There is now no topology on $M$, only on the $M_c$. But I introduce a new "continuity" predicate for functions $M \to M'$, and prove the minimal amount of stuff that we need about them.

[Peter Scholze]

Note that $T^{-1}$ does not send $M_{\leq c}$ into $M_{\leq c}$. What I suggested once was to define a rescaling functor that takes some $M_{\leq \bullet}$ sends it to $M_{\leq r\bullet}$, and then $T^{-1}$ is a map from $M_{\leq r\bullet}$ to $M_{\leq \bullet}$

[Johan Commelin]

Yes, that might be the best approach

[Johan Commelin]

We need the fact that $T^{-1}$ is "additive", right?

[Johan Commelin]

It has to commute with addition, so that it commutes with the maps coming from BD.

[Peter Scholze]

Sure

[Peter Scholze]

But that ought to be automatic in what I said above

[Johan Commelin]

But this still means we need a two stage rocket. Because we can't define the rescaling functor before defining profinitely filtered pseudo normed groups

[Peter Scholze]

Yes, but that seems very reasonable to me. In fact better than cooking the $T^{-1}$ into the first stage

[Johan Commelin]

Another option would be to have non-strict maps in the first stage.

[Peter Scholze]

But that would destroy lots of functoriality, and control over constants

[Johan Commelin]

That might also help, because scalar multiplication with n would become a morphism

[Johan Commelin]

And so evaluation universal maps from BD would also become morphisms.

[Peter Scholze]

Hmm, I disagree

[Johan Commelin]

We would regain the functoriality on the subcategory with strict homs and $T^{-1}$.

[Peter Scholze]

See the appendix to lecture 9: You carefully choose constants in the BD complex to make scalar multiplication by $n$ well-defined

[Peter Scholze]

Well my experience from thinking about the pure math is that it's better to work with the strict notion, and work around the fact that certain maps are not strict by explicitly keeping track of required rescalings

[Johan Commelin]

So then multiplication by n would also use the rescaling functor, right?

[Johan Commelin]

I guess that would work

[Peter Scholze]

Yes

[Johan Commelin]

I'll start working on the second stage of the rocket (-;

[Patrick Massot]

Then we should stay abstract and not try to get down to earth because landing rockets is tricky.

[Johan Commelin]

I'm worried that the rescaling functor will lead to type theoretic motive headaches. (Yes, we wouldn't have those issues in set theory.)

[Johan Commelin]

We'll end up with types filtration M (r * (c1 + c2)) and filtration M (r * c1 + r * c2) that are not definitionally equal.

[Mario Carneiro]

$\Sigma$ = :rainbow:

[Peter Scholze]

What about the previous cheat of putting extra proofs that the rescaling factor is what you think it is?

[Johan Commelin]

That's another option

[Johan Commelin]

I'll just play around. My intuition is pushing me towards a predicate is_rescaling_hom r... but you warned against this, which is making me doubtful.

[Peter Scholze]

Hmm no that might be OK too

[Peter Scholze]

As long as the rescaling is mentioned explicitly

[Peter Scholze]

Well, whatever you think works to formalize cleanly the BD resolutions in the appendix to lecture 9

[Johan Commelin]

The suitable predicate worked quite well there.

[Johan Commelin]

I'll take another careful look at that appendix, to see what we need.

[Johan Commelin]

My guess is that we'll have another predicate very_suitable that will assert that a sequence of constants is not only suitable, but also works for the homotopies from that appendix.

[Johan Commelin]

But I agree that we should keep track of the constants. It just seems that it's better to pack them closer to the homs than to the objects

[Peter Scholze]

OK, sounds good. I think I misunderstood the proposal. I was thinking about the analogue of any bounded homomorphism of Banach spaces, where that notion does not keep track of the bound. Such a notion would definitely be too weak

[Johan Commelin]

Another design question: we want $x \in M_c \implies T^{-1}x \in M_{c/r}$. This is a condition on the action of $T^{-1}$ that will be bundled into the objects. But do we want to vary r with the objects? Or is r fixed for the entire category?

[Johan Commelin]

Since homs need to commute with $T^{-1}$, I'm guessing that r is fixed for the entire category. On the other hand, there are natural inclusions (that don't commute with $T^{-1}$) from $\overline{\mathcal M}_{r'}(S) \to \overline{\mathcal M}_{r}(S)$ for $r' \le r$.

[Peter Scholze]

For now, you should think of $r$ as fixed forever

[Johan Commelin]

Ok, thanks. That's what I was hoping :sweat_smile:

[Peter Scholze]

Although I guess, in the notation of the lecture notes, it is $r'$ that is relevant here

[Johan Commelin]

But if (when?!) we get to $\mathcal{M}_{<r}(S)$, we can start worrying about how to move $r$...

[Peter Scholze]

But both are completely fixed throughout lecture 9

[Peter Scholze]

hmm yes for $\mathcal M_{<r}(S)$, but there you don't have to worry about $\overline{\mathcal M}$ for example

[Johan Commelin]

@Peter Scholze For the time being, we don't need functoriality in the normed group $V$ either, right?

[Peter Scholze]

No, we don't! $V$ is fixed throughout lecture 9.

[Johan Commelin]

The second stage of the rocket is done. The third stage is coming along nicely.

[Johan Commelin]

If anybody is looking for something to work on, you can show that (weak) exactness is isomorphism invariant for isos of systems of complexes.

[Johan Commelin]

Another option is to turn Mbar into an object of ProFiltPseuNormGrpWithTinv, although that isn't as follow your nose as the other thing.

[Riccardo Brasca]

I can do something next week... too much teaching this week!

[Kevin Buzzard]

I will have several hours tomorrow. I was just tidying up the stuff I did last weekend.

[Kevin Buzzard]

I could try either thing -- do you have a preference?

[Johan Commelin]

I don't really care

[Riccardo Brasca]

The iso invariance should be easy... or there is something subtle I am missing?

[Johan Commelin]

No, it should be easy. But it has to be done.

[Johan Commelin]

I think the Mbar thing should be done by somebody who wants to learn all about the API for Mbar and ProFiltBazQuuxs

[Johan Commelin]

I'll probably do it tomorrow, if nobody beats me.

[Johan Commelin]

Once those things are done, and I finish the functoriality of the systems of complexes, then the only thing stopping us from stating 9.5 is the defn of polyhedral lattices, and turning $\mathrm{Hom}(\Lambda, \overline{\mathcal M}_{r'}(S))$ into a ProFiltBazQuux.

[Johan Commelin]

I haven't thought hard about that last thingy, but it shouldn't cause any surprises.

[Kevin Buzzard]

I was going to start on Laurent series until I saw this thread. I'm flexible.

[Scott Morrison]

"(weak) exactness is isomorphism invariant for isos of systems of complexes" is https://github.com/leanprover-community/lean-liquid/blob/master/src/system_of_complexes.lean#L197

[Riccardo Brasca]

We will probably also need the weak version, using is_weak_bdd_exact_for_bdd_degree_above_idx (with identical proof I think)

[Scott Morrison]

ah, okay

[Scott Morrison]

I'm having a go at this now

[Scott Morrison]

I've only just started reading these definitions, so I'm probably missing something, but I don't see why this iso-invariance lemma is true. I see that C₁.is_bdd_exact_for_bdd_degree_above_idx k m c₀ and f : C₁ ≅ C₂ implies that C₁.is_bdd_exact_for_bdd_degree_above_idx k' m c₀ for some potentially _larger_ k', but not that you can use the same k. Perhaps I am just misunderstanding something basic about the definitions.

[Scott Morrison]

f doesn't preserve norms, does it?

[Adam Topaz]

@Scott Morrison That's right, a moprhism of normed abeliaan groups is only assumed to be bounded (with respect to some constant C). Maybe k' = C * k?

[Scott Morrison]

Something like that. There will be appearances of f on both sides of the inequality, so potentially two appearances of that constant C.

[Adam Topaz]

But there are many morphisms involved one of these systems of complexes, so it's unclear whether a single k' would work.

[Adam Topaz]

I've also been too busy to follow the discussion here the last few weeks, so maybe someone else can clarify.

[Scott Morrison]

Hmm, yes. The different components of f : C₁ ≅ C₂ could all have different bounds...

[Riccardo Brasca]

Ah, I thought f preserved the norm... if this is not the case I agree it's not true

[Scott Morrison]

maybe we've just set up the category structure on system_of_complexes incorrectly, and it is meant to only have norm-nonincreasing morphisms?

[Scott Morrison]

in which case an isomorphism would be norm-preserving?

[Adam Topaz]

If you think of just the case of normed abelian grouups, and you have an isomorphism f with inverse g, then f has an associated constant C aand same with g, say D, so you would end uup with
|x| \le C * D * |x|
for all x. Of course, this doesn't mean that C = 1

[Scott Morrison]

I haven't discovered yet where we want to use this isomorphism-invariance result, so I don't know what statement we really want.

[Riccardo Brasca]

Yes, we should wait for someone who has a better understanding of the big picture

[Riccardo Brasca]

There was a discussion about optimizing the constants, so the existence of some k is definitely weaker than what we want

[Floris van Doorn]

I'm interested in joining this project. I just finished a paper I was writing on the formalization of Haar measure, so I have time now.
I looked a bit at the library, and I tried this lemma, and am stuck at exactly the same place (also not having any high-level idea of what I'm doing :) )

[Johan Commelin]

@Scott Morrison A system is admissible if all the maps are norm-nonincreasing. So we can have two versions of "iso-preserving", I guess.

[Johan Commelin]

But in practice, we will apply this to admissible examples only, so it's fine to add that as assumption.

[Scott Morrison]

but admissible is about the maps within a system, not the morphisms between them?

[Johan Commelin]

Oooh, you are right.

[Johan Commelin]

Sorry, let me think for a sec about how I want to apply the iso invariance

[Johan Commelin]

In NormedGroup we need norm-increasing morphisms, because we'll have automorphisms T that rescale the norm by some r.

[Johan Commelin]

But for the iso-invariance, we can assume that the maps between the systems are norm-noninc.

[Scott Morrison]

is it just that for system_of_complexes the morphisms should be norm nonincreasing?

[Scott Morrison]

or do we even want norm-increasing morphisms there?

[Johan Commelin]

I don't know yet

[Johan Commelin]

For the implication 9.5 => 9.4 we only need norm-noninc. But I don't know about the proof of 9.5.

[Johan Commelin]

I think it should be fine to make everything norm-noninc. Because the main tool is the normed spectral sequence 9.6. And that one is assumed to be admissible.

[Peter Scholze]

Isomorphism invariance is definitely one of the things I might use without noticing. But I'm actually confused where we want to use it. Currently, I can only think of situations where the two are literally the same to my eyes, so in particular everything is compatible with norms.

[Peter Scholze]

I agree that for an isomorphism that has a weird behaviour with respect to norms, the translation may not be so obvious, but I don't think such a situation appears.

[Johan Commelin]

@Peter Scholze In the proof of 9.5 => 9.4 you use that Hom(Z, Mbar) is the same as Mbar.

[Johan Commelin]

But Lean doesn't agree that they are the same-same-same.

[Johan Commelin]

/-- The system of complexes
`V-hat(M_{≤c})^{T⁻¹} ⟶ V-hat(M_{≤c_1c}^2)^{T⁻¹} ⟶ ...`
as a functor in `M`.

See also `system`. -/
@[simps]
def System (r : ℝ≥0) (V : NormedGroup) [normed_with_aut r V] [fact (0 < r)]
  (r' : ℝ≥0) [fact (0 < r')] [fact (r' ≤ 1)] :
  (ProFiltPseuNormGrpWithTinv r')ᵒᵖ ⥤ system_of_complexes :=
{ obj := λ M, BD.system c' r V r' (unop M),
  map := λ M₁ M₂ f, system.map BD c' r V r' f.unop,
  map_id' := λ M, by apply system.map_id,
  map_comp' := λ M₁ M₂ M₃ f g, by apply system.map_comp }

[Johan Commelin]

So now we need to turn Mbar into an object of the source category, and then we can restate 9.4.
Much ado about nothing...

[Johan Commelin]

But the upshot is that we are now also quite a bit closer to the statement of 9.5

[Johan Commelin]

Once Mbar is a ProFiltDingsBums we can also delete several hundreds of lines of dead code :sweat_smile:

[Peter Scholze]

OK, great! But then the norms are literally the same.

[Johan Commelin]

Sure, this is one of those hyper-canonical identifications that Lean will stumble over, but of course it's utterly trivial.

[Peter Scholze]

Sure, that's OK. I was just trying to answer the question that came up in the chat above, about which version of isomorphism invariance is required

[Johan Commelin]

Ok, yes. That's helpful. You're saying that in the proof of 9.5 we will not need a more advanced version. That's useful info.

[Riccardo Brasca]

So in practice we can add the assumption that the isomorphism preserves the norm?

[Riccardo Brasca]

If this is the case I can try to prove it now

[Johan Commelin]

Maybe we should do as Scott suggested, and bake this into the definition of morphism of system_of_complexes.

[Riccardo Brasca]

But this means changing the category, right? Morphisms of system of complexes are never explicitly defined, they are just natural transformations. And if we do so we can never consider norm increasing morphism

[Johan Commelin]

True. So my inclination is to just add it as unbundled assumptions on top of morphisms-as-nat-trans when we need it.

[Riccardo Brasca]

So something like

lemma of_iso (h : C₁.is_bdd_exact_for_bdd_degree_above_idx k m c₀) (f : C₁ ≅ C₂)
  (hnorm : ∀ c i (x : C₁.X c i), ∥(f.apply c i).1 x∥ ≤ ∥x∥ ) :
  C₂.is_bdd_exact_for_bdd_degree_above_idx k m c₀ :=

[Peter Scholze]

I think I strive to only ever consider norm-nonincreasing maps. If you formalize 9.6, you will find that it's best to have this assumption baked into the foundations, probably...

[Peter Scholze]

On the other hand, in the proof of 9.5, there is a point where I have to artificially divide by some factorials to make this assumption true. But I think it's still best to do the work there. In general, it's best to have norm-nonincreasing as the standard and make additional arguments when that's violated, because bounds are so important in this argument

[Scott Morrison]

It shouldn't be hard to do this. We can't just use a @[derive] statement to summon the category structure of system_of_complexes, but it will only be a few lemmas to define the subcategory of norm nonincreasing maps. (And I guess some straightforward helpful lemmas, e.g. that isomorphisms thus preserve norms.)

[Scott Morrison]

We already have a special apply function to apply a morphism to an element, so it will be no harder to use, whether the morphisms are collections of natural transformations or collections of natural transformations satisfying a condition.

[Johan Commelin]

@Peter Scholze $T^{-1}$ acts as automorphism on $V$. But do you ever consider the action of $T$? Or should we turn it into an norm-noninc endomorphism?

[Peter Scholze]

I think I only ever use the action of $T^{-1}$ in Lecture 9. I'm sorry that this is bad notation... but $\mathbb Z((T^{-1}))$ didn't feel much better to me.

[Peter Scholze]

Also note that $T$ doesn't act on $\overline{\mathcal M}$!

[Johan Commelin]

Right, only $T^{-1}$ does...

[Riccardo Brasca]

I have no idea how to modify the definition, so I will let someone else doing it :stuck_out_tongue:

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/Mbar/Mbar_le.lean#L583
two sorrys here that shouldn't be too hard...

Other than that, Mbar is now a profinitely_filtered_pseudo_normed_group_with_Tinv, and so we can use the general machinery to get a system of complexes (instead of the "ad hoc" approach that we first used to get the statement of 9.4).

[Kevin Buzzard]

Is someone working on these? I can try them now

[Johan Commelin]

I'm not

[Johan Commelin]

I need to have lunch, and after that there is a seminar talk in Freiburg by a certain Heather Macbeth :smiley: :laughing:

[Kevin Buzzard]

OK I'm unsorrying Mbar_le

[Johan Commelin]

Thanks!

[Kevin Buzzard]

I've done neg so all that's left is embedding_cast_le, although I'm wrestling with excessive memory consumption errors :-/

[Riccardo Brasca]

I had the same problem of excessive memory consumption. I run leanproject build and now it seems to be gone

[Kevin Buzzard]

Yeah, although that's a bit weird (I did the same).

[Riccardo Brasca]

Yes, there is something wrong...

[Kevin Buzzard]

We might have to ask the computer scientists, the code is nowhere near big or complicated enough to be causing problems, there might be some loop somewhere.

[Kevin Buzzard]

Going back to mathematics, it seems that I'm supposed to be proving that if $c_1\leq c_2$ then the injection Mbar_le r S c_1 \to Mbar_le r S c_2 is an embedding (i.e. the topology on the source is induced by the topology on the target under the injection). Is this done or am I expected to prove it?

[Kevin Buzzard]

(Mbar_le r' S c is the set of power series F_s = ∑ a_{n,s}T^n ∈ Tℤ[[T]] such that ∑_{n,s} |a_{n,s}|r'^n ≤ c, and S is finite)

[Kevin Buzzard]

OK I think I have a maths proof, I'll just type that in.

[Peter Scholze]

Any injective map of compact Hausdorff spaces acquires the subspace topology

[Peter Scholze]

not sure whether you already have that in mathlib, but it might be useful

[Kevin Buzzard]

oh that's a better approach than mine.

[Kevin Buzzard]

@Riccardo Brasca I had a problem with a proof timing out in Mbar_le and I've written a much simpler one, so maybe if you pull that memory error will go away.

[Kevin Buzzard]

I'm kind of annoyed I didn't spot that proof, I thought I had some counterexample but now I realise the source wasn't Hausdorff.

[Riccardo Brasca]

I don't see any timeout anymore :grinning:

[Sebastien Gouezel]

We have docs#closed_embedding_of_continuous_injective_closed. Is this what you need here?

[Peter Scholze]

I think not: There's something more specific to compact Hausdorff spaces, where merely being injective on underlying sets already implies it's closed immersion, with the subspace topology

[Sebastien Gouezel]

I think it's exactly this lemma, plus the trivial fact that a continuous map on a compact space is closed, no?

[Peter Scholze]

Well, I find the other half more trivial, I believe?

[Peter Scholze]

(After all, that half works for any topological space, so I regard it as "abstract nonsense")

[Sebastien Gouezel]

The other half is the fact that the image of a closed set is in fact the image of a compact set, hence it is compact, hence it is closed. We have all these facts in mathlib, but probably not glued together exactly in the form you need.

[Kevin Buzzard]

import topology.separation

lemma foo (X Y : Type*) [topological_space X] [topological_space Y]
  [compact_space X] [t2_space X] [compact_space Y] [t2_space Y]
  (f : X → Y) (hf1 : continuous f) (hf2 : function.injective f) :
  embedding f := sorry

is what we seem to need.

[Peter Scholze]

If I remember right, you can omit t2_space X

[Sebastien Gouezel]

Let me do this now.

[Kevin Buzzard]

Many thanks -- it is the last sorry in the file I'm working on.

[Kevin Buzzard]

lemma embedding_of_injective {X Y : Type*} [topological_space X] [topological_space Y]
  [compact_space X] [t2_space X] [compact_space Y] [t2_space Y] {f : X → Y}
    (hf1 : continuous f) (hf2 : function.injective f) :
  embedding f := sorry

is a tidier version

[Sebastien Gouezel]

#6057

[Sebastien Gouezel]

If you want to put it in your file, this is just

lemma continuous.is_closed_map [compact_space α] [t2_space β] {f : α → β} (h : continuous f) :
  is_closed_map f :=
λ s hs, (hs.compact.image h).is_closed

lemma continuous.closed_embedding [compact_space α] [t2_space β] {f : α → β} (h : continuous f)
  (hf : function.injective f) : closed_embedding f :=
closed_embedding_of_continuous_injective_closed h hf h.is_closed_map

(with topological space assumptions)

[Adam Topaz]

Did we decide what to do about (non)invariance under isomorphisms of systems of complexes?

Here's a possible suggestion, which I think we discussed at some point before (possible in a different context):

1. Redefine normed_group_hom to be norm nonincreasing.
2. Introduce an endofunctor on NormedGroup which on objects just scales the norm by a positive constant C.

[Johan Commelin]

I think such an endofunctor will lead to annoying DTT hell, unfortunately.

[Johan Commelin]

I would rather work with two separate categories.

[Adam Topaz]

Will it be more annoying than not having invariance under isomorphisms?

[Johan Commelin]

I think we don't need invariance under isos that much.

[Adam Topaz]

Oh ok.

[Johan Commelin]

But we could tweak the category structure on system_of_complexes instead, to ask that those maps are all norm-noninc

[Johan Commelin]

that seems like the best of both worlds

[Johan Commelin]

Should we explicitly make a norm_nonincreasing predicate? That might by more economical and ergonomical then explicitly writing out the condition every time.

[Adam Topaz]

Yes, I think making such a predicate would be a good option.

[Adam Topaz]

We can rewrite things like admissible using this

[Adam Topaz]

Should it be a class?

[Adam Topaz]

(or we can use facts again...)

[Johan Commelin]

No, I think just a regular predicate.

[Adam Topaz]

I'm thinking it might be nice to have it automatically for things like quotient maps

[Johan Commelin]

If we start using it a lot, we can upgrade.

[Adam Topaz]

Sounds good

[Johan Commelin]

And with regular predicates, we can have dot notation, which is also a powerful tool.

[Johan Commelin]

@Adam Topaz do you want to do this (minor) refactor?

[Adam Topaz]

I can. But I won't be able to today. I'll have much more time starting next week

[Johan Commelin]

ok, then let's see if it's still waiting for you next week :wink:

[Kevin Buzzard]

@Johan Commelin OK Mbar_le is now sorry-free.

[Johan Commelin]

Great, thanks!

[Johan Commelin]

I did the refactor, and pushed a proof that strong exactness is isom invariant (assuming strictness).

[Johan Commelin]

the condition embedding_cast_le is now replaced by continuous_cast_le (and embedding_cast_le is a lemma).

[Kevin Buzzard]

Nice!