Zulip Chat Archive

Stream: condensed mathematics

Topic: profinitely filtered pseudo normed topological groups


view this post on Zulip Johan Commelin (Jan 29 2021 at 09:25):

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 MM with an increasing filtration (Mc)cR0(M_c)_{c \in \mathbb R_{\ge 0}} such that
  • McM_c is a profinite set
  • MM is pseudo normed, so 0Mc0 \in M_c, Mc=Mc-M_c = M_c, and Mc1+Mc2Mc1+c2M_{c_1} + M_{c_2} \subset M_{c_1+c_2}

Morphisms of these gadgets should be continuous and bounded homs.

view this post on Zulip Johan Commelin (Jan 29 2021 at 09:25):

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

view this post on Zulip Johan Commelin (Jan 29 2021 at 09:26):

Reason for the generalisation:

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

view this post on Zulip Adam Topaz (Jan 29 2021 at 14:22):

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?

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:23):

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

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:24):

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

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:24):

But we should definitely experiment a bit with different approaches.

view this post on Zulip Adam Topaz (Jan 29 2021 at 14:24):

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

view this post on Zulip Adam Topaz (Jan 29 2021 at 14:25):

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.

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:26):

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

view this post on Zulip Adam Topaz (Jan 29 2021 at 14:27):

Ah, I see.

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:51):

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?

view this post on Zulip Peter Scholze (Feb 01 2021 at 09:58):

definitely not!

view this post on Zulip Peter Scholze (Feb 01 2021 at 09:58):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:59):

Oooh right.

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:00):

So we'll need some special work to make Hom(Λ,Mr(S))\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.

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:01):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:01):

Right

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:01):

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 }

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:04):

I'm currently playing around with formal definitions of the objects. Lean automatically puts a (subspace) topology on the filtration sets McM_c, if we put a topology on MM. But if the topology on MM is defined in terms of topologies on McM_c to start with, this means we now have two topologies on McM_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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:05):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:05):

Definitely!

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:06):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:06):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:07):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:08):

But it's not a metric topology!

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:08):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:15):

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×YX \times Y or the product topology (of the metric topologies on XX and YY). To make this usable, we need to use a "trick". We put a separate topology on XX, together with a proof that it is equal to the metric topology. And then on X×YX \times Y the proof that it's a metric space includes the lemma that the two aforementioned topologies agree.

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:24):

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

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:27):

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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:29):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:30):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:30):

I thought the homomorphisms should be strict, i.e. map McM_{\leq c} into NcN_{\leq c}

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:31):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:31):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:33):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:33):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:35):

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

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:36):

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.

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:36):

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...

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:38):

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.

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:48):

One thing I find mildly confusing about type theory is that its advocates claim that when you form say 1/x1/x it automatically checks for you that xx 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 xx 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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:50):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:51):

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".

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:55):

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).

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:55):

But currently such automation is typically slow or brittle.

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:56):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:57):

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?

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:59):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 10:59):

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

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:59):

OK, I see

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:00):

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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:02):

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."

view this post on Zulip Peter Scholze (Feb 01 2021 at 11:02):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:03):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:04):

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...)

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:05):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:06):

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 x0x \ne 0. And I think I'm not the only one who "cheats" like this.

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 11:07):

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.

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 11:10):

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.

view this post on Zulip Peter Scholze (Feb 01 2021 at 11:22):

Johan Commelin said:

Similarly, if C : system_of_complexes and xCcix \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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:25):

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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 11:26):

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...

view this post on Zulip Patrick Massot (Feb 01 2021 at 12:13):

The question of 1/01/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 kk, we define division as a function from k×kk \times k to kk, without any precondition, and it satisfies 1/0=01/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×1/x=1x \times 1/x = 1 without asking for a proof that xx is non-zero. The lemma simplifying this expressions asks for a proof, the definition of 1/x1/x doesn't. Note that apologizing is not always needed. For instance (a+b)/c=a/c+b/c(a+b)/c = a/c + b/c is true without any condition on cc. That's because we've clearly chosen the "junk value" a/0=0a/0 = 0. This is simply convenient in practice.

view this post on Zulip Johan Commelin (Feb 01 2021 at 12:16):

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

view this post on Zulip Patrick Massot (Feb 01 2021 at 12:25):

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 GG have a unique reasonable uniform structure. Now complete this uniform structure to get a new uniform space G^\hat G and extend the group operations to G^\hat G. The new group operations are continuous. So G^\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 G^\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 GG are compatible then the group structure and the uniform structure on G^\hat G are compatible.

view this post on Zulip Peter Scholze (Feb 01 2021 at 12:50):

I can totally relate to that second trick, but remain minimally perplexed by this 1/0=01/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=01/0=0 is a very discontinuous extension of 1/x1/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...!

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:58):

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.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:59):

(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.)

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:05):

I pushed a definition of the category.

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:24):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:27):

We used to go from Mr(S)cmMr(S)cn\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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:28):

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

view this post on Zulip David Michael Roberts (Feb 01 2021 at 23:43):

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=01/0=0 is a very discontinuous extension of 1/x1/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.

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 06:58):

The reason it doesn't work in constructive settings is that given a random term representing a real number, such as π2/6n11/n2\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=0x=0 then..."

view this post on Zulip Peter Scholze (Feb 02 2021 at 09:52):

@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 22 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.)

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:04):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:04):

He frequently says "types are an editor feature".

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:10):

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.

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:12):

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).

view this post on Zulip Peter Scholze (Feb 02 2021 at 10:12):

Aha, that's great!

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:16):

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 XYX \to Y uses the same machinery as an implication of propositions P    QP \implies Q.

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:16):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 10:22):

yes and no. There's this whole hierarchy of nn-truncated homotopy types: For n=2n=-2, just the one-point set, for n=1n=-1, the empty set and the one-point set, for n=0n=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=0n=0 (why not n=1n=1 and allow groupoids as well? Why not n=2n=2? etc.)

view this post on Zulip Johan Commelin (Feb 02 2021 at 10:24):

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.

view this post on Zulip Johan Commelin (Feb 02 2021 at 16:30):

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.

view this post on Zulip Johan Commelin (Feb 03 2021 at 07:17):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 07:18):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 07:18):

profinitely_filtered_pseudo_normed_group_with_Tinv is a bit... long

view this post on Zulip Kevin Buzzard (Feb 03 2021 at 07:28):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 07:32):

But that doesn't mention the T

view this post on Zulip Johan Commelin (Feb 03 2021 at 07:33):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:37):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:39):

Yes, that might be the best approach

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:39):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:40):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:40):

Sure

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:40):

But that ought to be automatic in what I said above

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:41):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:42):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:42):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:43):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:43):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:43):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:43):

Hmm, I disagree

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:44):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:44):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:45):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:46):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:46):

I guess that would work

view this post on Zulip Peter Scholze (Feb 03 2021 at 08:46):

Yes

view this post on Zulip Johan Commelin (Feb 03 2021 at 08:47):

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

view this post on Zulip Patrick Massot (Feb 03 2021 at 09:11):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:34):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:35):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 09:35):

Σ\Sigma = :rainbow:

view this post on Zulip Peter Scholze (Feb 03 2021 at 09:37):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:37):

That's another option

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:38):

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.

view this post on Zulip Peter Scholze (Feb 03 2021 at 09:39):

Hmm no that might be OK too

view this post on Zulip Peter Scholze (Feb 03 2021 at 09:39):

As long as the rescaling is mentioned explicitly

view this post on Zulip Peter Scholze (Feb 03 2021 at 09:40):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:40):

The suitable predicate worked quite well there.

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:41):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:42):

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.

view this post on Zulip Johan Commelin (Feb 03 2021 at 09:43):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 09:51):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 12:35):

Another design question: we want xMc    T1xMc/rx \in M_c \implies T^{-1}x \in M_{c/r}. This is a condition on the action of T1T^{-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?

view this post on Zulip Johan Commelin (Feb 03 2021 at 12:38):

Since homs need to commute with T1T^{-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 T1T^{-1}) from Mr(S)Mr(S)\overline{\mathcal M}_{r'}(S) \to \overline{\mathcal M}_{r}(S) for rrr' \le r.

view this post on Zulip Peter Scholze (Feb 03 2021 at 13:27):

For now, you should think of rr as fixed forever

view this post on Zulip Johan Commelin (Feb 03 2021 at 13:27):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 13:28):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 13:28):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 13:28):

But both are completely fixed throughout lecture 9

view this post on Zulip Peter Scholze (Feb 03 2021 at 13:29):

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

view this post on Zulip Johan Commelin (Feb 03 2021 at 19:50):

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

view this post on Zulip Peter Scholze (Feb 03 2021 at 22:07):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:05):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:50):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:51):

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

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 21:52):

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

view this post on Zulip Kevin Buzzard (Feb 04 2021 at 21:53):

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

view this post on Zulip Kevin Buzzard (Feb 04 2021 at 21:54):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:55):

I don't really care

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 21:55):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:55):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:56):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:56):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:57):

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 Hom(Λ,Mr(S))\mathrm{Hom}(\Lambda, \overline{\mathcal M}_{r'}(S)) into a ProFiltBazQuux.

view this post on Zulip Johan Commelin (Feb 04 2021 at 21:58):

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

view this post on Zulip Kevin Buzzard (Feb 04 2021 at 22:01):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 22:27):

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

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 22:31):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 22:40):

ah, okay

view this post on Zulip Scott Morrison (Feb 04 2021 at 22:40):

I'm having a go at this now

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:01):

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.

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:02):

f doesn't preserve norms, does it?

view this post on Zulip Adam Topaz (Feb 04 2021 at 23:12):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:12):

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

view this post on Zulip Adam Topaz (Feb 04 2021 at 23:13):

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

view this post on Zulip Adam Topaz (Feb 04 2021 at 23:13):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:15):

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

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 23:17):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:18):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:18):

in which case an isomorphism would be norm-preserving?

view this post on Zulip Adam Topaz (Feb 04 2021 at 23:18):

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

view this post on Zulip Scott Morrison (Feb 04 2021 at 23:20):

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

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 23:20):

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

view this post on Zulip Riccardo Brasca (Feb 04 2021 at 23:21):

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

view this post on Zulip Floris van Doorn (Feb 05 2021 at 00:16):

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 :) )

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:45):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:46):

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

view this post on Zulip Scott Morrison (Feb 05 2021 at 05:46):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:46):

Oooh, you are right.

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:47):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:48):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:49):

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

view this post on Zulip Scott Morrison (Feb 05 2021 at 05:50):

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

view this post on Zulip Scott Morrison (Feb 05 2021 at 05:50):

or do we even want norm-increasing morphisms there?

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:51):

I don't know yet

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:52):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 05:53):

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.

view this post on Zulip Peter Scholze (Feb 05 2021 at 08:45):

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.

view this post on Zulip Peter Scholze (Feb 05 2021 at 08:47):

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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:00):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:00):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:05):

/-- 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 }

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:06):

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...

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:06):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:07):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:11):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:12):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:13):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:13):

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.

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 09:16):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 09:16):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:17):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 09:19):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:21):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 09:35):

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₀ :=

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:37):

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...

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:38):

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

view this post on Zulip Scott Morrison (Feb 05 2021 at 09:40):

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.)

view this post on Zulip Scott Morrison (Feb 05 2021 at 09:41):

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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:42):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:47):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:47):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:48):

Right, only T1T^{-1} does...

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 09:50):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 11:07):

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).

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 11:46):

Is someone working on these? I can try them now

view this post on Zulip Johan Commelin (Feb 05 2021 at 11:46):

I'm not

view this post on Zulip Johan Commelin (Feb 05 2021 at 11:47):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 12:07):

OK I'm unsorrying Mbar_le

view this post on Zulip Johan Commelin (Feb 05 2021 at 12:07):

Thanks!

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:12):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 13:17):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:17):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 13:17):

Yes, there is something wrong...

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:19):

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.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:20):

Going back to mathematics, it seems that I'm supposed to be proving that if c1c2c_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?

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:23):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:25):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 13:48):

Any injective map of compact Hausdorff spaces acquires the subspace topology

view this post on Zulip Peter Scholze (Feb 05 2021 at 13:48):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:49):

oh that's a better approach than mine.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:50):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 13:51):

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.

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 13:51):

I don't see any timeout anymore :grinning:

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 13:58):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 14:09):

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

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 14:19):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 14:22):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 14:23):

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

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 14:24):

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.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 14:26):

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.

view this post on Zulip Peter Scholze (Feb 05 2021 at 14:26):

If I remember right, you can omit t2_space X

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 14:27):

Let me do this now.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 14:27):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 14:29):

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

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 14:42):

#6057

view this post on Zulip Sebastien Gouezel (Feb 05 2021 at 14:50):

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)

view this post on Zulip Adam Topaz (Feb 05 2021 at 14:54):

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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:08):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:08):

I would rather work with two separate categories.

view this post on Zulip Adam Topaz (Feb 05 2021 at 15:09):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:10):

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

view this post on Zulip Adam Topaz (Feb 05 2021 at 15:11):

Oh ok.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:11):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:11):

that seems like the best of both worlds

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:17):

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

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:19):

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

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:19):

We can rewrite things like admissible using this

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:19):

Should it be a class?

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:20):

(or we can use facts again...)

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:20):

No, I think just a regular predicate.

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:21):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:21):

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

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:21):

Sounds good

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:22):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:23):

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

view this post on Zulip Adam Topaz (Feb 05 2021 at 17:23):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:24):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 17:44):

@Johan Commelin OK Mbar_le is now sorry-free.

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:44):

Great, thanks!

view this post on Zulip Johan Commelin (Feb 05 2021 at 19:26):

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

view this post on Zulip Johan Commelin (Feb 06 2021 at 06:05):

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

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 08:55):

Nice!


Last updated: May 09 2021 at 16:20 UTC