spaces of measure / Z((T))_r

Stream: condensed mathematics

[Johan Commelin]

We need to formalize the definition of $\mathcal M(S, \Z((T))_r)$ and $\mathcal M(S, \Z((T))_{>r})$ (see top of page 37 of Analytic.pdf).
I think we can first define this as a functor on profinite sets, and then later turn it into a condensed abelian group. Formalizing these definitions might inform our decision about how to define condensed abelian groups.

@Peter Scholze do you have a good name for these gadgets (it doesn't matter if it is long, we can enable $\mathcal M$ notation afterwards).

[Peter Scholze]

Hmm, I don't know about a good name.

[Johan Commelin]

Does it make sense to call them something like (overconvergent) integral measures? Sounds like a weird mix...

[Filippo A. E. Nuccio]

Am I wrong or the $r$ in the right-hand side of the definition of $\overline{\mathcal{M}}_{r'}(S)_{\leq c}$ for finite $S$ on page 57 of Analytic.pdf should be an $r'$?

[Johan Commelin]

I pushed a fix

[Filippo A. E. Nuccio]

I am slowly starting to think about this, do you know if some advances have already been made?

[Johan Commelin]

Nope... not that I know of

[Adam Topaz]

@Filippo A. E. Nuccio were you thinking about $\mathcal{M}(S,\mathbb{Z}((T))_{> r})$ or $\overline{\mathcal{M}}_{r'}(S)$?

[Filippo A. E. Nuccio]

The former (well, actually $\mathcal{M}(S,\mathbb{Z}((T))_r)$ for the time being: as defined right before Theorem 6.9 on page 37 of Analytic.pdf).

[Adam Topaz]

I guess the definition could start like this:

import ring_theory.laurent_series
import topology.category.Profinite
import topology.locally_constant.algebra
import data.real.nnreal
import topology.algebra.infinite_sum
import analysis.normed_space.basic


noncomputable theory

variables (S : Profinite)

example : comm_ring (locally_constant S ℤ) := by apply_instance -- nice

-- We have this somewhere in LTE.
instance : has_nnnorm (locally_constant S ℤ) :=
⟨λ F, ⨆ (s : S), ∥ F s ∥₊⟩

example : comm_ring (laurent_series (locally_constant S ℤ)) := by apply_instance -- nice

open_locale nnreal big_operators

def filtration (r c : ℝ≥0) : set (laurent_series (locally_constant S ℤ)) :=
{ F | summable (λ n : ℤ, ∥ F.coeff n ∥₊ * r^n) ∧ -- summability
      (∑' (n : ℤ), ∥ F.coeff n ∥₊ * r^n) ≤ c } -- and bounded by c.

[Adam Topaz]

The stuff in https://github.com/leanprover-community/lean-liquid/blob/master/src/locally_constant/analysis.lean should probably move to mathlib soon...

[Filippo A. E. Nuccio]

Ah, ok: I was starting in a somewhat different direction but your approach is more valuable, I guess. I am going to have a look in half a hour or so.

[Adam Topaz]

Maybe the following is better?

import ring_theory.laurent_series
import topology.category.Profinite
import topology.locally_constant.algebra
import data.real.nnreal
import topology.algebra.infinite_sum
import analysis.normed_space.basic

noncomputable theory

variables (S : Profinite)

open_locale nnreal big_operators

def filtration (r c : ℝ≥0) : set (laurent_series (locally_constant S ℤ)) :=
{ F | ∀ (s : S), summable (λ n : ℤ, ∥ (F.coeff n) s ∥₊ * r^n) ∧ -- summability
                 (∑' (n : ℤ), ∥ (F.coeff n) s ∥₊ * r^n) ≤ c } -- and bounded by c.

[Adam Topaz]

At least that should correspond to what's defined on page 36 of analytic.pdf

[Adam Topaz]

Proving that these things are profinite sets will be a challenge... (but should go more-or-less similarly to the proof that Mbar_le are profinite)

[Filippo A. E. Nuccio]

I had

structure c_measures (r : ℝ≥0) (c : ℝ≥0) (S : Type*) (hS : fintype S) :=
(to_fun     : S → ℤ → S → ℤ)
(summable   : ∀ s s', summable (λ n, (↑(to_fun s n s').nat_abs * r ^ n)))
(bdd        : ∀ s s', tsum (λ n, (↑(to_fun s n s').nat_abs * r ^ n)) ≤ c)

structure oc_measures (r : ℝ≥0) (S : Type*) (hS : fintype S) :=
(to_fun      : S → ℤ → S → ℤ)
(summable   : ∀ s s', summable (λ n, (↑(to_fun s n s').nat_abs * r ^ n)))

and then was trying to upgrade these to functors from Fintype to pseudo-normed groups.

[Filippo A. E. Nuccio]

But as said, your approach seems better.

[Adam Topaz]

Filippo A. E. Nuccio said:

But as said, your approach seems better.

I'm not sure. Your definition gives direct access to the underlying function given by the coefficients.

[Filippo A. E. Nuccio]

Yes, it does. I was also thinking that working with finite sets and then taking inv limits (as in p 37) might be easier.

[Filippo A. E. Nuccio]

I have pushed this already to the branch fae_overconvergent_measures, if you want to have a look (I have a call now and won't be able to work on this for 30-35 mins, but will be back later).

[Adam Topaz]

I'm actually a little confused about the definition of $\mathbb{Z}((T))_r[S]_{\le c}$ that appears at the top of page 37. Are these two $S$'s really the same?

[Filippo A. E. Nuccio]

Why not? I don't see immediately where the problem lies.

[Adam Topaz]

Well, $\mathbb{Z}((T))_r$ is a condensed ring, so a priori is a functor $S \mapsto \mathbb{Z}((T))_r(S)$ as defined on page 36. The $\mathbb{Z}((T))_r[S]$ is the free module on a, say, finite set $S$.

[Filippo A. E. Nuccio]

Oh, this I agree: the two $S$'s from p. 36 and 37. I took the short path and forgot about p 36, simply thinking that the functor was defined on finite $S$ and then extended by inv. limit, without checking that the definition would give back that on p 36.

[Adam Topaz]

Using a single S probably gives the same result, but a priori there are two $S$'s in the definition of $\mathbb{Z}((T))_r[S]$ (one from the $S$ in $[S]$ and one from the condensed structure).

[Filippo A. E. Nuccio]

Actually: what do you mean by "the one from the condensed structure"? That on p. 37 the notation $\mathbb{Z}((T))_r[S]$ is the free condensed $\mathbb{Z}((T))_r$-module on $S$, and so that a priori one could evaluate $\mathbb{Z}((T))_r[S](S')$ on any profinite $S'$?

[Adam Topaz]

Ignoring the module part of the story, at the end of the day $\mathbb{Z}((T))_r[-]$ is a functor sending a profinite set $S$ to a condensed set, which is a functor sending a profinite set $S'$ to a set.

[Filippo A. E. Nuccio]

Yes, I agree; but the way I read the sentence on l. 2 of page 37 was that $\mathbb{Z}((T))_r[S]_{\leq c}$ is a functor sending a finite set $S$ to some abelian group and so $\mathbb{Z}((T))_r$ sends $S$ to the union over $c$ of the values of the previous functor. So, for me, "free-module" meant "free $\mathbb{Z}$-module" (because the explicit definition associates to $S$ a group, not a functor -- not a "true" one, i.e. a non-constant one).

[Filippo A. E. Nuccio]

At a different level: I am trying to improve a bit my code with the above definition, and I am trying to give the

def oc_functor (r : ℝ≥0) : Fintype.{u} ⥤ ProFiltPseuNormGrp.{u} :=

associating to every finite set $S$ the p-f-p-n-group oc_measures r S as defined above.

[Adam Topaz]

Maybe the equation at the top of page 37 should say the following?

$$\mathbb{Z}((T))_r[S]_{\le c} := \{ \sum_{n \in \mathbb{Z}, s \in S} a_{n,s} T^n [s] \ | \ a_{n,s} \in \mathbb{Z}, \ \sum_{n,s} | a_{n,s} | r^n \le c \}$$

[Filippo A. E. Nuccio]

But would they really be "measures"? You are right, looking at the statement of Thm 6.9 it seems all $a_n$ must be in $\mathbb{R}$

[Adam Topaz]

I'm just thinking about our definition here...
https://github.com/leanprover-community/lean-liquid/blob/8f444ae6d4113c8c550a9aa597a7511725a2658b/src/Mbar/basic.lean#L39

[Adam Topaz]

and here
https://github.com/leanprover-community/lean-liquid/blob/8f444ae6d4113c8c550a9aa597a7511725a2658b/src/Mbar/Mbar_le.lean#L34

[Filippo A. E. Nuccio]

I agree, I actually adapted mine from there (replacing $a_n$ with functions, blindly copying)

[Filippo A. E. Nuccio]

BTW: In thm 6.9, I guess the maps is as condensed groups. But how to look at an element of $\mathbb{Z}((T))_r$ as a series? Evaluating it at the singleton?

[Adam Topaz]

If I undderstand correctly, if $S$ is a profinite set, consider $\sum_n a_n T^n$ where $a_n \in C(S,\mathbb{Z})$, and send that series to the function $s \mapsto \sum_n a_n(s) r'^n$.

[Adam Topaz]

I guess that's what this map (of condensed sets) is supposed to do when you apply it to a profinite set $S$.

[Filippo A. E. Nuccio]

Ah, where the second is an element of $\mathbb{R}$ as a condensed set: right!

[Filippo A. E. Nuccio]

At any rate, as long as we put sorries everywhere, the code can very easily be adapted :grinning_face_with_smiling_eyes:

[Filippo A. E. Nuccio]

And which approach do you suggest to follow? Have you had a look to my branch?

[Adam Topaz]

@Filippo A. E. Nuccio we could discuss for a bit and do some pair programming on zoom, if you would like...

[Filippo A. E. Nuccio]

Yes, I have half an hour free now, if you want.

[Adam Topaz]

Ok, give me about 10 mins to get more coffee. I'll send you a link.

[Johan Commelin]

Adam Topaz said:

Maybe the equation at the top of page 37 should say the following?

$$\mathbb{Z}((T))_r[S]_{\le c} := \{ \sum_{n \in \mathbb{Z}, s \in S} a_{n,s} T^n [s] \ | \ a_{n,s} \in \mathbb{Z}, \ \sum_{n,s} | a_{n,s} | r^n \le c \}$$

What is the difference with what is currently there?

[Adam Topaz]

Currently it says $C(S,\mathbb{Z})$ instead of $\mathbb{Z}$

[Adam Topaz]

at least on the version on Peter's webpage (I haven't checked the version from github...)

[Johan Commelin]

git show 5765f9e35dc03ffe24563dc86cd6f4b115d004ae
commit 5765f9e35dc03ffe24563dc86cd6f4b115d004ae
Author: Johan Commelin <johan@commelin.net>
Date:   Tue Jul 13 10:51:05 2021 +0200

    fix typo in display

diff --git a/Analytic.tex b/Analytic.tex
index 6c5bc42..75c7c9a 100644
--- a/Analytic.tex
+++ b/Analytic.tex
@@ -1180,7 +1180,7 @@ each of which is a finite set.

 For any finite set $S$, we now write the free module $\mathbb Z((T))_r[S]$ as the increasing union of
 \[
-\mathbb Z((T))_r[S]_{\leq c} := \{\sum_{n\in \mathbb Z,s\in S} a_{n,s} T^n [s]\mid a_{n,s}\in C(S,\mathbb Z), \sum_{n\in \mathbb Z, s\in S} |a_{n,s}|r^n\leq c\};
+\mathbb Z((T))_r[S]_{\leq c} := \{\sum_{n\in \mathbb Z,s\in S} a_{n,s} T^n [s]\mid a_{n,s}\in \mathbb Z, \sum_{n\in \mathbb Z, s\in S} |a_{n,s}|r^n\leq c\};
 \]
 each of these is again a profinite set. The addition defines maps
 \[

[Adam Topaz]

Tue Jul 13 10:51:05 2021 +0200 ;)

[Adam Topaz]

Would you mind not gitignoring the compiled pdf in that repo, so that the most up-to-date version of analytic.pdf can be obtained from github?

[Patrick Massot]

This isn't the right solution. This repo should have CI that builds and publishes.

[Adam Topaz]

Patrick Massot said:

This isn't the right solution. This repo should have CI that builds and publishes.

Yes, of course, but that takes more effort to implement.

[Adam Topaz]

Actually, if you know of a github ci recipe that does this, that would be great to know about!

[Adam Topaz]

(I had something along these lines cobbled together for some lecture notes for one of my classes last term, but it was too clunky to be useful in general)

[Yakov Pechersky]

It does already as far as I remember engineering it. You can check the github actions

[Yakov Pechersky]

Because it needs the pdf for the web interface, iirc

[Adam Topaz]

@Yakov Pechersky this is a separate repo, not the bluepring... I'm referring to https://github.com/PeterScholze/Analytic

[Bryan Gin-ge Chen]

I've just made a PR that does something super basic: https://github.com/PeterScholze/Analytic/pull/8

cc: @Johan Commelin

[Johan Commelin]

@Bryan Gin-ge Chen @Peter Scholze Thanks! I merged the PR

[Johan Commelin]

@Bryan Gin-ge Chen The produced artifact is a .zip file: https://github.com/PeterScholze/Analytic/actions/runs/1108315466

[Johan Commelin]

Do you think this can be turned into simply the pdf?

[Johan Commelin]

Have you been pushing the Mbar variants to a branch? What is the status there?

[Adam Topaz]

Yes

[Adam Topaz]

Still WIP

[Adam Topaz]

I just pushed some stuff a few mins ago. It's on the branch fae_overconvergent_...

[Johan Commelin]

Ok, thanks for the pointer!

[Adam Topaz]

The main finiteness needed to prove that the terms in the filtration are Profinite is done, just gotta patch things together in a limit

[Johan Commelin]

Once we have those, we should build some api that takes a profinitely_filtered_pseudo_normed_foobar and turns it into a condensed_foobar.

[Adam Topaz]

@Johan Commelin shouldn't you be on vacation right now? What are you doing on zulip?

[Johan Commelin]

Ooh, and we'll need to know that $\Z((T))_r \to \R$ given by $T \mapsto \frac12$ for $r > \frac12$ is a surjective ring hom.

[Johan Commelin]

(I returned from holidays... a couple of hours ago. We'll go for another week later in August. So I'll have a week to hack on LTE :smiley: )

[Adam Topaz]

Johan Commelin said:

Ooh, and we'll need to know that $\Z((T))_r \to \R$ given by $T \mapsto \frac12$ for $r > \frac12$ is a surjective ring hom.

Does mathlib have any API for this? Something like the existence of a "decimal expansion" of a real number?

[Johan Commelin]

I'm not sure. I guess that @Mario Carneiro might know this best.

[Mario Carneiro]

Doesn't ring a bell. Maybe nat.digits or the cardinality of the reals proof?

[Adam Topaz]

Well... the rain let up so I'm going mountain biking.
I'll try to finish up the profiniteness of the filtration for oc_measures on Monday.

[Yaël Dillies]

Adam Topaz said:

Johan Commelin shouldn't you be on vacation right now? What are you doing on zulip?

Wait, are holidays when you are not doing Lean?

[Shing Tak Lam]

Adam Topaz said:

Johan Commelin said:

Ooh, and we'll need to know that $\Z((T))_r \to \R$ given by $T \mapsto \frac12$ for $r > \frac12$ is a surjective ring hom.

Does mathlib have any API for this? Something like the existence of a "decimal expansion" of a real number?

Someone on the Xena discord was working on decimal expansions of real numbers, I think it was @Deniz Aydin ? Not sure if it's public anywhere.

[Kevin Buzzard]

It's an old branch of mine. I think it was Deniz.

[Johan Commelin]

I guess the surjectivity is easy for $T \mapsto x$ for any $x \le r$. But what we actually need to use later is that the kernel is a principal ideal. And for $x \in \mathbb Q$ that is a lot easier to prove than for $x \notin \mathbb Q$.

[Johan Commelin]

In the end, we can get away with $x = 1/2$ for the final application.

[Adam Topaz]

Most of the proof that oc_measures r S is a pfpng is done in the branch fae_overco..., but there are some silly sorry's around mostly about summability of certain series. If anyone wants to fill in some of these, that would be helpful!

[Filippo A. E. Nuccio]

I think I have filled most of them, and I have merged the branch to master. I hope to finish some of the remaining ones tomorrow.

[Adam Topaz]

Great! I can try to take care of some of them this afternoon.

[Adam Topaz]

Okay, overconvergent_measures/basic.lean only has two interesting sorry's left ;)

[Adam Topaz]

These two sorry's are now squashed.

[Filippo A. E. Nuccio]

@Adam Topaz I was having a look at bounded overconvergent measures, but I can't figure out why you need them.

[Adam Topaz]

They're used to define the topology

[Filippo A. E. Nuccio]

Ah, ok.

[Adam Topaz]

Essentially it's just the collection of series $\sum_n a_n T^n$ where $a_n$ is zero outside a finite set T : finset \Z. If you also bound the norm, this is therefore a finite type, hence profinite if you give it the discrete topology. And the set of series $\sum_n a_n T^n$ with bounded norm is the limit over such collections as $T$ varies.

[Filippo A. E. Nuccio]

All this still for finite S, though, right?

[Adam Topaz]

yes

[Adam Topaz]

To replace S by a profinite set, we need functoriality of these constructions in S.

[Filippo A. E. Nuccio]

Yes, I see. There is now an error with summable_of_sum_le (which apparently does not exist) and I wanted to fix this. Then I can try to set-up this compatibility, unless you've already started.

[Adam Topaz]

That's strange... it seemed to work for me yesterday?

[Filippo A. E. Nuccio]

OK, may be I need to update mathlib? Is it a recent addition?

[Adam Topaz]

I didn't update mathlib. It should work.

[Filippo A. E. Nuccio]

I have an unknown identifier 'summable_of_sum_le'

[Adam Topaz]

the github ci on LTE was able to build successfully. So I think your setup is messed up somehow.

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/runs/3307440491

[Filippo A. E. Nuccio]

Right. Let me check.

[Filippo A. E. Nuccio]

OK, I have updated mathlib and this will take a while. In the meantime, what's your feeling about functoriality wrt S? I guess we want
1) To prove it first for bdd measures
2) To show it extends via mk_seq to compatibility between the corresponding to_fun of o.c. ones
3) Prove these transition morphisms are continuous.
What do you think?

[Adam Topaz]

I think we should follow more-or-less the same steps I did for Mbar.

[Filippo A. E. Nuccio]

RIght, I didn't think about checking that part. I am sorry, I'll have a look.

[Adam Topaz]

Here are the relevant locations:
https://github.com/leanprover-community/lean-liquid/blob/a5c5206bf3b50fb8468778e15c65b0fa056f4900/src/Mbar/basic.lean#L427
https://github.com/leanprover-community/lean-liquid/blob/a5c5206bf3b50fb8468778e15c65b0fa056f4900/src/Mbar/Mbar_le.lean#L479
https://github.com/leanprover-community/lean-liquid/blob/a5c5206bf3b50fb8468778e15c65b0fa056f4900/src/Mbar/bounded.lean#L239

[Adam Topaz]

(I'm not too happy with the Profinite.extend stuff... I need to change that at some point)

[Filippo A. E. Nuccio]

Ok, I'll study these and come back (hopefully, in the meanwhile the problem with 'summable_of_sum_le' will be gone).

[Adam Topaz]

I think a better approach is to show that ProfinitelyFilteredPseudoNormedGroups have the correct limits, and extend the corresponding functor Fintype \func ProfinitelyFiltered....instead of extending the individual components.

[Adam Topaz]

Proving that the extension commutes with cofiltered limits is also a challenge which I haven't done yet.

[Filippo A. E. Nuccio]

This is certainly more elegant. But what extension should commute with cofiltered limits? From bdd to o.c. measures?

[Adam Topaz]

Oh, I'm talking about the general construction here:
https://github.com/leanprover-community/lean-liquid/blob/a5c5206bf3b50fb8468778e15c65b0fa056f4900/src/for_mathlib/Profinite/extend.lean#L37

[Peter Scholze]

Regarding this thread: I just want to point out that to define these spaces of overconvergent measures, you should first define the spaces of convergent measures (i.e., for fixed $r$ resp. $p$) and then take a colimit (over $r$ resp. $p$). And only for (bounded) convergent measures you can reduce from profinite $S$ to finite $S$ by cofiltered limits.

I didn't quite follow what you are doing, but I was slightly afraid you take the colimit over $r$ resp. $p$ before taking the cofiltered limit over $S$'s.

[Peter Scholze]

In any case, the challenge requires only "convergent" measures

[Adam Topaz]

Oh, the name is misleading. We haven't defined anything overconvergent yet

[Filippo A. E. Nuccio]

@Peter Scholze But when you speak about the space of conv. measure, do you mean it as a condensed group?

[Peter Scholze]

Sure

[Peter Scholze]

As Johan was discussing, this should come from its structure as a profinitely filtered blah

[Adam Topaz]

@Filippo A. E. Nuccio we should probably change the name oc_measures (these are the convergent ones)

[Filippo A. E. Nuccio]

I see, so you mean that we should not define an "overconvergent functor on finite sets" (whatever it is) hoping to extend it to profinite ones, but rather first extend it to profinite, and then "overconverge"

[Filippo A. E. Nuccio]

@Adam Topaz It's dinner time here now; I can take up some of this tomorrow, but have to go now,

[Adam Topaz]

Ok. I'll try to change the name.

[Adam Topaz]

By the way, if we try to prove that ProfinFiltPseudoNormedGroup has cofiltered limits, we'll probably run into issues similar to limits in seminormed groups, since the morphisms in this category need not be strictly compatible with the filtration.

[Adam Topaz]

So the idea above about extending the functor into ProfinFiltPseudoNormedGroup probably won't work

[Adam Topaz]

Okay, I think I'll replace oc_measures with laurent_measures. Any objections?

[Adam Topaz]

Okay, that's done. I also started on the functoriality

[Adam Topaz]

Just pushed:

@[simps]
def functor (r : ℝ≥0) [fact (0 < r)] : Fintype.{u} ⥤ ProFiltPseuNormGrp.{u} :=
{ obj := λ S, ProFiltPseuNormGrp.of $ laurent_measures r S,
  map := λ S T f, map_hom f,
...

[Adam Topaz]

I think in this case it may be worthwhile to introduce ProFiltPseuNormGrp₀ (with maps strictly compatible with the filtration, analogous to SemiNormedGroup₀). The functor above really lands there, and we would be able to actually show that this category has enough limits so that the profinite variant of the above could be obtained by extension along cofiltered limits.

[Johan Commelin]

I guess that would work. But things like multiplication by $T^{-1}$ are not compatible with the filtration, right? So we might need to deal with those separately.

[Adam Topaz]

True. one solution (that came up before as well) could be to introduce functors F C from ProFiltPseuNormGrp₀ to itself which rescale the filtration by C, and have T\inv be a morphism from Mto (F C).obj M.

[Johan Commelin]

but extending bounded_laurent_measures to profinite S is easy, right?

[Johan Commelin]

and showing that we can "inclusion" maps between those extensions is also not so hard.

[Johan Commelin]

similar for addition and negation maps

[Johan Commelin]

and then we can take a colimit in condensed sets (which exists by generic stuff done by Bhavik), and then we can build a condensed abelian group

[Johan Commelin]

that would bypass the whole ProFiltPseuNormGrp(₀) stuff. I don't know if that is good or bad.

[Adam Topaz]

I would prefer to define functor ProFiltPseuNormGrp to Cond (Ab), and compose that with a functor to ProFiltPseuNormGrp.

[Johan Commelin]

But I guess it might be best to use CompHausFiltPseuNormGrp

[Adam Topaz]

As for defining the extension to Profinite, sure it's easy, but it's incredibly annoying. For example, think about what it takes to define addition -- you need to use the fact that binary products commute with limits, and that category_theory.limits.binary_product agrees with the usual type-theoretic product.

[Johan Commelin]

That's a good point.

[Johan Commelin]

Ok, I'm now somewhat convinced that it will probably pay of to build CompHausFiltPseuNormGrp₀ and construct a functor to that category.

[Adam Topaz]

Of course working with CompHausFiltPseuNormGrp\0 isn't going to save us from doing the annoying work showing that it has enough limits, but at least we would have to only do it once!

[Filippo A. E. Nuccio]

@Adam Topaz Have you begun working on this CompHausFiltPseuNormGrp\0 category already?

[Adam Topaz]

No

[Filippo A. E. Nuccio]

Ok; and would you suggest me starting with that or are there things which you believe to be more useful/urgent ?

[Johan Commelin]

If/when you start, I suggest that you slightly refactor profinitely_filtered_pseudo_normed_group so that it extends comphaus_filtered_pseudo_normed_group (which is defined as the former, but without tot.disconnectedness).

[Adam Topaz]

Do we want a ProfinFiltPseuNormGrp\_0 as well? @Johan Commelin ?

[Johan Commelin]

No, I don't think we need it.

[Johan Commelin]

As far as I can see now

[Adam Topaz]

Yeah, same here.

[Adam Topaz]

Well, morphisms in CompHausFiltPseuNormGroup and ProfinFiltPseuNormGroup are the same, and similarly with the \_0, so we if have to add it in the future it will be easy once we have CompHaus...\_0.

[Adam Topaz]

I haven't checked the details, but if we want to have limits, I think we may need to add an assumption on these objects that the fiultration is exhaustive.

[Johan Commelin]

Which it is in all the examples that we care about.

[Adam Topaz]

Sure.

[Johan Commelin]

But I don't think we proved this for Mbar.

[Adam Topaz]

In all our cases the filtration comes from some norm anyway, so it should be easy to obtain

[Johan Commelin]

If we add that to the existing definition, then we might have to prove this in quite a bunch of places.

[Adam Topaz]

Maybe we should just add in for CompHausFilt.... for now?

[Johan Commelin]

So maybe we drop my idea of having profinitely_filtered_bla extend comphaus_filtered_bla.

[Filippo A. E. Nuccio]

Can't we just add exhaustiveness (?) when proving that limits exist as an extra hyp?

[Adam Topaz]

We could have [exhaustive A] as a mixin.

[Filippo A. E. Nuccio]

You mean to add a typeclass?

[Adam Topaz]

But [has_limits C]is a propoerty of a category C, so then we would need to make a new thing called CompHausExhausFiltPseuNormGroup and that's just way too long to type

[Filippo A. E. Nuccio]

Ah right

[Filippo A. E. Nuccio]

So I'm a bit lost. Do we go for these CompHausFilt_blaor not? At any rate, what I don't understand if how this would really help. Sure constructing limits there is probably easier since there is no issue with non-uniqueness of the norm, but then we need to show that the functor to ProfFinitely_bla preserves limits, no?

[Adam Topaz]

@Filippo A. E. Nuccio you can start to try proving that ProfinFiltPseuNormGroup (without \_0) has limits and see that you will get stuck pretty quickly because the morphisms in this category involve inflating the filtration index by some constant (analogous to the way morphisms are defined for semi_normed_group, where there is a similar issue). That's why we would want a \_0. Next, we want one context where both $\mathcal{M}(S,\mathbb{Z}((t))_r)$ and $\mathcal{M}_p(S)$ would fit in. The first one is profinitely filtered, but the second has a filtration by compact hausdorff spaces which are not totally disconnected. That's why we want Comphaus_filt_blah. Finally, the reason we want limits is because we first define the things above for finite S then take a limit. The idea is to take a limit in Comhaus_filt_blah\_0, and compose with a functor from there to condensed abelian groups.

[Filippo A. E. Nuccio]

Oh thanks! Very nice summary.

[Filippo A. E. Nuccio]

Before going further, I immediately have the question as whether we really need that the category ``has limits''. For instance, I remember that in @Johan Commelin and @Rob Lewis ' paper on Witt vectors, they show that Witt vecs are a limit without proving it "categorically".

[Filippo A. E. Nuccio]

I agree this is certainly a nicer approach, but I wonder if it is needed (or if we can't just force the definition on a profinite set, although of course the problem is to show that the result is indep. of the way we write a profinite set as a limit).

[Adam Topaz]

You don't have to, but then you can't use the stuff from for_mathlib/Profinite/extend because https://github.com/leanprover-community/lean-liquid/blob/23e4854a4b1390672b8962018bff47af5f650ddd/src/for_mathlib/Profinite/extend.lean#L33

[Adam Topaz]

The alternative is to ignore all this nonsense and take all limits/colimits in Cond Type*, then manually promote to an object of Cond Ab.

[Adam Topaz]

Adam Topaz said:

The alternative is to ignore all this nonsense and take all limits/colimits in Cond Type*, then manually promote to an object of Cond Ab.

Maybe this is an argument for defining Cond Ab as the category of abelian group objects in Cond Type*?

[Filippo A. E. Nuccio]

By "manually" you mean to prove the axioms add, has_neg, etc... by hand?

[Filippo A. E. Nuccio]

Adam Topaz said:

Adam Topaz said:

The alternative is to ignore all this nonsense and take all limits/colimits in Cond Type*, then manually promote to an object of Cond Ab.

Maybe this is an argument for defining Cond Ab as the category of abelian group objects in Cond Type*?

Or is this an argument to construct a general formalism that takes categories $\mathcal{C},\mathcal{D}$ and defines $\mathcal{C}$-objects valued in $\mathcal{D}$ so that we also have condensed rings in one shot?

[Adam Topaz]

There is no such general formalism... See e.g. docs#Mon_

[Filippo A. E. Nuccio]

Ok, I was pushing it too far without solid knowledge, sorry.

[Adam Topaz]

(Well, you could cook up a general formalism like that for concrete categories $\mathcal{C}$, using representable presheaves for example, but I don't know how useful that is.)

[Filippo A. E. Nuccio]

OK. I have to go soon now. I'll see where things are tomorrow to see if I can be of any help, as I haven't fully understood if we ultimately want to follow @Johan Commelin ' suggestion of having profinitely_filtered_blah extending comphaus_filtered_blah.

[Filippo A. E. Nuccio]

As an aside: reading on p. 38 of Analytic.pdf I see the object $\mathcal M(S, \mathbb{Z}((T))_{>r})$ (so, in particular, the condended ring $\mathbb{Z}((T))_{>r}$. Is it by definition the colimit of all $\mathbb{Z}((T))_r$? I can't find a definition of it before p. 38 :thinking:

[Johan Commelin]

Yes, it is the "overconvergent version, which takes the union over all $r' > r$. But we don't need that ring for the time being.

[Adam Topaz]

I've started this refactor in the branch comphaus_filt_refactor. So far I just made the class comphaus_filt_... and made profinitely_filt_... extend it, while ensuring everything compiles, and I also added the definition of the category CompHausFiltPSeuNormGroup (without \_0). I still haven't generalized everything that should be generalized (such as the stuff in rescale/pseudo_normed_group)

[Filippo A. E. Nuccio]

Johan Commelin said:

Yes, it is the "overconvergent version, which takes the union over all $r' > r$. But we don't need that ring for the time being.

I guessed so, but is it me or its definition only shows up after p. 38?

[Filippo A. E. Nuccio]

@Adam Topaz I can try to define the instance : comphaus_filtered_pseudo_normed_group (rescale r M) for a comphaus_filtered_pseudo_normed_group M and let type-class inference deduce the old one? Done.

[Johan Commelin]

@Filippo A. E. Nuccio Almost at the end of p37 there is

On the other hand, this again indicates that for a fixed r, the theory will not work, so we pass to a colimit again.

This explains how to define $\mathcal M(S, \Z((T))_{>r})$ as colimit of $\mathcal M(S, \Z((T))_{r'})$ s. The ring $\Z((T))_{>r}$ only shows up in S7 and this is also where it is properly defined. There are some forward refs from S6 to S7.

[Filippo A. E. Nuccio]

Ah, I see, thanks. I was reading too linearly, I guess... :ruler:

[Adam Topaz]

Filippo A. E. Nuccio said:

Adam Topaz I can try to define the instance : comphaus_filtered_pseudo_normed_group (rescale r M) for a comphaus_filtered_pseudo_normed_group M and let type-class inference deduce the old one? Done.

Thanks! I just pushed a minor change.

[Adam Topaz]

instance [profinitely_filtered_pseudo_normed_group M] :
  profinitely_filtered_pseudo_normed_group (rescale r M) := {}

:smile:

[Filippo A. E. Nuccio]

And do we also want the notion of a comphaus_filt... with an action of $T^{-1}$? Because it seems a bit strange to me now that for a [profinitely_filtered_pseudo_normed_group_with_Tinv r' M] we have an instance of comphaus_filtered_pseudo_normed_group_hom (rescale r M) (rescale r M): I agree that this makes sense, but I wonder if we don't want it under slightly more general hyp on M

[Adam Topaz]

I think the $T^{-1}$ instance is only really used for $\mathcal{M}(S,\mathbb{Z}((T))_r)$, so leaving it for the profinite case should be okay.

[Adam Topaz]

If we want to eventually generalize, we should just do things properly and work with condensed modules over condensed rings (the $T^{-1}$ case is for modules over $\mathbb{Z}[T^{-1}]$)

[Filippo A. E. Nuccio]

OK. I was just observing that it is strange to say that the morphism between the rescale is as comphaus_filt.. as everything in sight is already a profinitely_filt....

[Filippo A. E. Nuccio]

But it is certainly a minor point.

[Filippo A. E. Nuccio]

@Adam Topaz as you're probably working on this right now and have a clear picture: do you want me to work on something in particular?

[Adam Topaz]

I actually don't have much time today unfortunately... One concrete thing that you could go for is defining CompHausFiltPseuNormGroup\_0 using https://github.com/leanprover-community/lean-liquid/blob/7060d641407fef3a0282aa05386f593d654e438d/src/pseudo_normed_group/profinitely_filtered.lean#L92

[Adam Topaz]

And define the functor to CompHaus... without the 0.

[Filippo A. E. Nuccio]

Ok, I will go for the first, either today or tomorrow morning (CET), and if I can I will define the functor.

[Filippo A. E. Nuccio]

In the meanwhile I have added a couple of lines of doc for comphaus... and adapted that of profinitely... accordingly.

[Adam Topaz]

Oh yeah I've been very lazy about docs :expressionless: sorry!

[Adam Topaz]

@Filippo A. E. Nuccio when defining the category, please take a look at how CompHausFilt... is defined using docs#category_theory.bundled and docs#category_theory.bundled_hom and try to mimic that.

[Filippo A. E. Nuccio]

OK! Thanks.

[Adam Topaz]

Using this bundled formalism, the [derive ...] tag will give a lot of the structure we need for free.

[Filippo A. E. Nuccio]

While I was looking at your link above: I thought you wanted me to define CompHausFilt... with 0 (generalising groups with 0) but the link points to strict morphisms. Do I miss something?

[Filippo A. E. Nuccio]

Ah no, I see.

[Filippo A. E. Nuccio]

You want two categories, one with strict morphisms, the other with usual ones.

[Filippo A. E. Nuccio]

(The first you call with a 0) and a functor between the two.

[Filippo A. E. Nuccio]

Right? For the usual business of uniqueness of limits, I guess.

[Adam Topaz]

Yes, the one with nonstrict morphisms is defined here: https://github.com/leanprover-community/lean-liquid/blob/60ab75bfbd20ad2323c4922a48d1664d6a8efd92/src/pseudo_normed_group/category.lean#L25

[Johan Commelin]

Should we use \_1 as subscript?

[Filippo A. E. Nuccio]

Ok, I got the point.

[Johan Commelin]

That's what we do with (semi)normed groups

[Adam Topaz]

Isn't it 0 for SemiNormedgroup?

[Johan Commelin]

I thought it was \_1 (because norm le one)

[Adam Topaz]

You're right. Yes, 1 is better ;)

[Filippo A. E. Nuccio]

OK, I'll call it with 1. :one:

[Filippo A. E. Nuccio]

On line 40 of pseudo_normed_group/category.lean, shouldn't the doc say

/-- The category of profinitely filtered pseudo-normed groups. -/

rather than

/--CompHaus-ly-/

?

[Filippo A. E. Nuccio]

OK, I'll modify it.

[Filippo A. E. Nuccio]

I have modified the name of the field continuous' to continuous₁' in the definition of strict morphism to differentiate it from the field with the same name in the definition of a "usual" morphism between comphaus_fil....

[Adam Topaz]

You're really supposed to use f.continuous for comphaus_..._hom and f.continuous_level (or f.level_continuous, I don't remember) for strict_..._hom.

[Filippo A. E. Nuccio]

Well, but for the time being they were both called continuous'. Do you mean I should rename both as you suggest?

[Adam Topaz]

What I mean is that both having the same name shouldn't matter.

[Filippo A. E. Nuccio]

I simply find it confusing, not that it creates issues. But I suspect you wanted to say something deeper.

[Filippo A. E. Nuccio]

(I guess I see what you meant: I am currently proving axiom continuous' for the hom obtained from a strict_hom and I have just encountered the def level you're probably speaking about)

[Adam Topaz]

Oh, take a look at https://github.com/leanprover-community/lean-liquid/blob/ddfed397901ac19bf274e547c28e8e9ca376dc7e/src/pseudo_normed_group/profinitely_filtered.lean#L375

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

I have defined the category CompHausFiltPseuNormGrp₁ (I hope correctly) and I am defining the "forgetful" functor towards CompHausFiltPseuNormGrp. I need to go now, but I can (and will!) continue tomorrow. I was not able to immediately adapt @Adam Topaz ' suggestion, but, unless this is super-urgent, I am happy to continue with what I am doing since I am learning a lot about category theory in Lean (and will also be happy to delete everything for the usual one-line proof I won't have been able to find).

[Filippo A. E. Nuccio]

All this in the file category.lean of pseudo_normed_group in the branch comphaus_filt_refactor.

[Adam Topaz]

@Filippo A. E. Nuccio sorry, I should have been more clear. The functor can be defined as follows:

def enlarging_functor : CompHausFiltPseuNormGrp₁ ⥤ CompHausFiltPseuNormGrp :=
{ obj := λ M, M,
  map := λ M₁ M₂ f, f.to_chfpsng_hom }

once you add

instance (M : CompHausFiltPseuNormGrp₁) : comphaus_filtered_pseudo_normed_group M := M.str

I pushed the change just now.

[Adam Topaz]

(the fields map_id' and map_comp' are filled in automatically by the auto param, since we set up the correct ext and simp lemmas)

[Filippo A. E. Nuccio]

@Adam Topaz I have modified a bit functor because there was an error in the map field. It now takes values in CompHausFiltPseuNormGrp rather than in ProFiltPseuNormGrp, but this should not be a problem. As an aside, I have re-read most of the profinitely_filtered file and it seems to me that it still speaks about profinitely filtered pseudo-normed group hom although they don't exist anymore.

[Filippo A. E. Nuccio]

Should I modify all the doc accordingly? Also, I don't understand how can Lean know what the category ProFiltPseuNormGrp is, given that the morphisms are not explicitly defined.

[Adam Topaz]

@Filippo A. E. Nuccio The morphisms in ProFiltPseuNormGrp and CompHausFiltPseuNormGrp are both defined as comphaus_filtered_pseudo_normed_group_hom, so functor should really land in ProFiltPseuNormGrp. There is a functor from ProFiltPseuNormGrp to CompHausFiltPseuNormGrp, and the version of functor you just defined is the composition of functor as it originally was with this functor from ProFiltPseuNormGrp to CompHausFiltPseuNormGrp.

[Adam Topaz]

The category structure on ProFiltPseuNormGrp is defined using the bundled hom's trick here:
https://github.com/leanprover-community/lean-liquid/blob/4cf07bae405b23d50b6353a969dc937dd403fb07/src/pseudo_normed_group/category.lean#L78

[Adam Topaz]

Oh, I found the issue. When CompHausFiltPseuNormGrp₁ was defined using bundled_hom, the typeclass system decided to choose that instance when defining the category structure on ProFiltPseuNormGrp. That's not good. I'll try to fix it now.

[Adam Topaz]

Okay, it should be fixed now.

[Adam Topaz]

I reverted functor back to ProFilt... as well.

[Filippo A. E. Nuccio]

Good!

[Johan Commelin]

What's the status here? Can someone bring me up to speed again?

[Adam Topaz]

We probably want to finish off and merge the refactor of profinitely_filtererd_... which was started in the branch comphaus_filt_refactor.

[Filippo A. E. Nuccio]

Both structures of ProFiltPseu... and CompHausFiltPseu... are now defined (as categories), the first also with its variants using strict, rather than continuous, homs.

[Filippo A. E. Nuccio]

Oh yes, I agree.

[Adam Topaz]

$\mathcal{M}(S,\mathbb{Z}((T))_r)$ for finite $S$ has also been defined as a profinitely filtered pseudo normed group, and as a functor in (again finite) $S$, in the branch fae_overconvergent_measures.

I'm in the process of finish off some of the API for Profinite.extend (which is essentially showing that Profinite is equivalent to Pro(Finite)) and that should help us with the extensions from finite sets to profinite sets.

[Adam Topaz]

For these extensions, we will probably want to show that CompHausFiltPseuNormGroup\_1 has limits, and extend a functor from Fintype to this. We can then define a functor from CompHausFiltPseuNormGroup (without the \_1) to Cond(Ab).

(Now that I'm thinking about this again, we may need to add a condition that the filtration is exhaustive for CompHausFiltPseuNormGroup\_1.)

[Adam Topaz]

And before doing anything with Cond(Ab), we need to fix the universe issues in the definition of Cond Foo.

[Johan Commelin]

Thanks! So if I understand correctly, both comphaus_filt_refactor and fae_overconvergent_measures contain unmerged mergable material?

[Johan Commelin]

Are there parts that shouldn't be merged?

[Adam Topaz]

I don't think so. @Filippo A. E. Nuccio what do you think?

[Johan Commelin]

If not, please go ahead and merge :octopus:

[Filippo A. E. Nuccio]

I think that basic of fae_over... contains a lot of useless stuff.

[Filippo A. E. Nuccio]

OK, I can try to polish it a bit and merge in master the fae... branch.

[Adam Topaz]

Wait... looks like laurent_measures is already in master.

[Adam Topaz]

I guess we merged it at some point ;)

[Adam Topaz]

So please ignore the fae_overco... branch.

[Filippo A. E. Nuccio]

I have a general question: why don't we use the API developed for formal power series/laurent series (which is already in mathlib)? Just because it is useless in our setting?

[Johan Commelin]

I think that in principle we could certainly use it. But we still need the filtration, and the fact that it is a filtration by profinite/comphaus gadgets.

[Adam Topaz]

I think it would be a good idea to use the existing Laurent series API if we need the ring structure, but do we actually need the ring structure?

[Johan Commelin]

Afaik, for the bare minimum challenge, we don't need it.

[Adam Topaz]

I proved this lemma:
https://github.com/leanprover-community/lean-liquid/blob/b7c0ec4cd13dc012041cc46d50042758d1ef2dcb/src/laurent_measures/basic.lean#L287
which should let us relate the current def of laurent_measures to Laurent series as they appear in mathlib.

[Filippo A. E. Nuccio]

OK, I see.

[Adam Topaz]

(note that a priori laurent_measures makes no restrictions on vanishing of coefficients)

[Filippo A. E. Nuccio]

The reason I was asking is that I was thinking about defining the map $\mathbb{Z}((T))_r\to\mathbb{R}$. I guess we'll need it pretty soon, right?

[Filippo A. E. Nuccio]

I was thinking of defining it at the level of groups, but as ring-hom is probably better (surjectivity will be harder, of course). Hence the question about giving the lhs a ring structure.

[Johan Commelin]

For surjectivity, given some $x \in \R$, we should define a stream of coefficients $(a_n)_n$ such that $\sum_n a_n (\tfrac12)^n = x$.

[Johan Commelin]

I think that's a project that can be done independent of any other choices.

[Filippo A. E. Nuccio]

But it won't be unique.

[Johan Commelin]

Sure, I don't care (-;

[Filippo A. E. Nuccio]

OK, I am happy to give it a go.

[Johan Commelin]

But you can take $a_n \in \{-1,0,1\}$ if you want.

[Filippo A. E. Nuccio]

On the other hand, I was also thinking that a priori it should be a map of condensed ab. groups. Given the fact that all topologies here are nice, I guess that full faithfulness will tell us that it makes no difference, but do we intend to prove this faithfulness or is it better to define it as map of condensed ab groups?

[Adam Topaz]

As long as it's a map of comphaus_filt_... things, it will be fine on the condensed level as well.

[Adam Topaz]

So it comes down to the compatibility of this map with the norms, which should be more-or-less clear from the definitions.

[Filippo A. E. Nuccio]

Ah ok, so I will need not to define it as map of ab. groups but as comphaus_filt_.. things, right?

[Filippo A. E. Nuccio]

Do we already have a proof that \mathbb{R} is comph_filt..?

[Johan Commelin]

Where "more-or-less-clear" means Prop 7.2

[Filippo A. E. Nuccio]

OK, I'll go for it in the fae_overconvergent.. branch, in a new file.

[Adam Topaz]

Filippo A. E. Nuccio said:

OK, I'll go for it in the fae_overconvergent.. branch, in a new file.

make sure to merge master -> fae_over...

[Filippo A. E. Nuccio]

Already done!

[Adam Topaz]

Johan Commelin said:

Where "more-or-less-clear" means Prop 7.2

Yeah, but look at how Prop 7.2(3) is proved (with $C_3 = 1$)

[Filippo A. E. Nuccio]

@
Adam Topaz said:

Filippo A. E. Nuccio said:

OK, I'll go for it in the fae_overconvergent.. branch, in a new file.

make sure to merge master -> fae_over...

On the other hand, since the comphaus_filt... branch is not in master, I don't have the comphaus business in mine yet. It is not super-urgent, but if you can merge comphaus... -> master may be tomorrow this would help.

[Adam Topaz]

I'll try to merge it at some point today.

[Johan Commelin]

@Filippo A. E. Nuccio Did you by chance start working on 7.2 or something related?

[Filippo A. E. Nuccio]

Yes, I have begun working on the definition of $\theta$. I am actually almost done with the proof of its surjectivity as set-theoretic map, but I need to upgrade it to a comphaus_bla map, which will rely on 7.2. This I planned to do in what follows.

[Johan Commelin]

Great! Is this also on a branch, if so which one?

[Filippo A. E. Nuccio]

Do you need them now? I wanted to polish a bit my file before pushing to master.

[Filippo A. E. Nuccio]

Ah, the branch is fae_overconnvergent...

[Johan Commelin]

Ok

[Johan Commelin]

I just wanted to get a sense of what's going on.

[Johan Commelin]

The downside of these branches is that master is not always an accurate depiction of where we are standing

[Filippo A. E. Nuccio]

Yes, you're right.

[Filippo A. E. Nuccio]

On the other hand, I wrote a lot (lot!) of nonsense and played with many things to get used to summability, and it would have been insane to push all this to master, no?

[Johan Commelin]

fair enough

[Filippo A. E. Nuccio]

At any rate, speaking about 6.9, will we need Harbater's theorem describing $\ker\theta$?

[Filippo A. E. Nuccio]

(In particular, given we're not putting a ring structure on $\mathbb{Z}((T))_r$)?

[Johan Commelin]

no, we only apply it to $x = 1/2$, so we will be effectively modding out $(2T - 1)$

[Johan Commelin]

The proof in S7 is a lot more general, and shows that evaluating at non-rational numbers still has a principal ideal as kernel

[Filippo A. E. Nuccio]

But in (2) of 6.9 there are both $r$ and $r'$ (I guess you meant $r=1/2$), and $r'$ changes with $p$.

[Filippo A. E. Nuccio]

And soon becomes very non-rational.

[Johan Commelin]

No, we can keep $r'$ fixed in our applications.

[Filippo A. E. Nuccio]

OK, this I can't understand by now: but I'll study more and see how this works, I don't want to waste your time. Just going back to $\theta$: is it OK that I finish its surjectivity as set-theoretic map and then move on to the one as comp_haus_blah... (i.e. I prove it is a comp_haus_blah morphism)?

[Johan Commelin]

The strategy is as follows: we want to prove LTE for some $p$ (i.e. a statement about Ext groups and $\mathcal M_p$). So now we set $r' = 1/2$ and $r = (r')^p$. And then we reduce everything to theorem 9.4 for $r < r'$.

[Filippo A. E. Nuccio]

AH OK, this makes sense.

[Filippo A. E. Nuccio]

I somehow thought that to prove the full statement about Ext groups we needed to let $p$ vary.

[Johan Commelin]

No, I think that only happens when you start to worry about $\mathcal M_{<p}$. That's part of the statement that $\R$ is an analytic ring, but it's not part of the LTE challenge.

[Filippo A. E. Nuccio]

OK, I guess I see but as said I prefer to study more before saying nonsense. I'll let you know as soon as I push to master some advances on 6.9.

[Filippo A. E. Nuccio]

Going back to the discussion we had yesterday, I suppose that what we want is that r' does not appear in the definition of $\theta$ and that r≥0 and hr : r < 1 do appear. I guess they better be explicit variables, right?

[Johan Commelin]

Hmm, the definition of $\theta$ very much depends on r', right? It's evaluating Laurent series at r'.

[Filippo A. E. Nuccio]

Sure, but you told me you wanted to fix r' = 1/2.

[Johan Commelin]

I guess you need $0 < r' \le r$, but I don't think you need $r < 1$ for most of this story.

[Johan Commelin]

Filippo A. E. Nuccio said:

Sure, but you told me you wanted to fix r' = 1/2.

Aaah, if you want you can specialize there directly. I think that for defining the hom it doesn't make things easier. But for the surjectivity, and for describing the kernel, it will certainly help.

[Filippo A. E. Nuccio]

Yes, this was my point.

[Filippo A. E. Nuccio]

Of course, for the def is basically equivalent. But I was thinking at the best API. First, having r' in the proof makes things (slightly) less nice, but most importantly we have to carry it over forever, and if we only use r'=1/2 it is better to have it fixed, no? This I meant by " r' does not appear".

[Filippo A. E. Nuccio]

On the other hand, I guess we want to have r (as the radius of the laurent measure mapping to a certain $x$ through $\theta$) variable; but then my question is whether implicit or explicit.

[Johan Commelin]

Actually, fixing things early can sometimes make life harder. For example simp might start doing things to the / in 1/2. Keeping it packaged in an atomic r' can help in those cases.

[Johan Commelin]

So I would keep around the r' until specializing to 1/2 really helps.

[Filippo A. E. Nuccio]

Ah, ok. I will modify accordingly. And what about implicit/explicit ones? r' certainly needs to be explicit if we want to specialize to 1/2 but r (and r < 1, should this be needed)? I can't come up with a nice picture in my head of how we will need to apply this. Of course, it won't be very hard to change later, but if you have a suggestion I'd be happy to follow it.

[Johan Commelin]

I would make r and r' explicit and use [fact (0 < r')] etc for the conditions.

[Filippo A. E. Nuccio]

OK, I was going in that direction, good. Thanks! I will push something later today and let you know when it's done.

[Filippo A. E. Nuccio]

I have pushed the file laurent_measures/thm69.lean with the basics concerning $\theta$ and its surjectivity. I might have some time later today but at any rate I plan to finish both the surjectivity and attack some of thm 7.2 to show it is a comp_haus_blah morphism. This will need to wait until Tuesday but I will have time next week to advance.

[Adam Topaz]

Adam Topaz said:

I'll try to merge it at some point today.

Sorry it's a few (maybe more than a few ;)) days late... but this is now merged to master

[Filippo A. E. Nuccio]

Thanks!