## Stream: condensed mathematics

### Topic: lemma 9.7

#### Johan Commelin (Jan 20 2021 at 20:47):

I pushed a statement of lemma 9.7. I characterise "finite free abelian group" as "fin.gen. and torsion free". As far as I can see, that should work for the proof.

#### Johan Commelin (Jan 20 2021 at 20:47):

If someone want to take a shot at this sorry, go ahead.

#### Filippo A. E. Nuccio (Jan 22 2021 at 11:23):

I have begun looking at Lemma 9.7 and it really seems feasable. I will try to work on this from next week, but I feel that (at least if one follows the proof in the paper), we need a structure theorem for finite abelian groups to characterize $\Lambda$. I think this is OK as part of our project on Dedekind domains where I think we have the structure theorem for f.g. modules over PID.

#### Filippo A. E. Nuccio (Jan 22 2021 at 11:24):

I also think that there is a small typo on line 3 of the proof in the manuscript, $\Lambda^{\vee}_+$ should be a submodule of $\Lambda^{\vee}$, not of $\Lambda$.

#### Peter Scholze (Jan 22 2021 at 11:55):

Thanks for catching the typo! By the way, as suggested by Johan Commelin, there is now a git repository with the source code https://github.com/PeterScholze/Analytic , so you can make pull requests for typos. It should also help with version control, as I often update the version on my webpage. (I will now make sure it is synced with the version on github.)

#### Johan Commelin (Jan 22 2021 at 12:12):

@Filippo A. E. Nuccio I haven't thought hard about the ingredients yet. But if you already have the structure theorem, that's great!

#### Filippo A. E. Nuccio (Jan 22 2021 at 15:09):

Unfortunately I have to take it back! I thought that it had been implemented, but it turns out it is not the case... Never mind, I will try to figure out if it is really needed and will keep you posted.

#### Johan Commelin (Jan 22 2021 at 16:06):

My guess is that it would be fine to assume that all $\Lambda$'s are of the form $\mathbb{Z}^n$. But we can't explicitly write it like that, because we'll run into defeq-issues.

#### Johan Commelin (Jan 22 2021 at 16:06):

So we need to describe free abelian groups in such a way that a product of two free abelian groups is again free abelian, etc...

#### Kevin Buzzard (Jan 22 2021 at 18:53):

@Amelia Livingston has some partial progress on this

#### Filippo A. E. Nuccio (Jan 25 2021 at 12:59):

Is it in mathlib or is she working on her own?

#### Kevin Buzzard (Jan 25 2021 at 13:06):

I'm meeting her this afternoon, I can ask her the status of things. I don't think she's actively working on it right now

#### Kevin Buzzard (Jan 25 2021 at 22:03):

The answer was https://github.com/101damnations/fg_over_pid , which is unfinished, and currently she's more worried about her finals than finishing it (which is fair enough -- she's also working on Koszul complexes in Lean as part of her project)

#### Filippo A. E. Nuccio (Jan 26 2021 at 07:48):

Oh sure! Thanks, I'll have a look at the repository and see if I can extract useful pieces of code.

#### Damiano Testa (Jan 26 2021 at 08:13):

Filippo, I have been thinking about how to formalize this result and I suspect that it might be a good idea to break the problem in two.

First, show that we can fit the "inequalities", working over a Q (or R). This should be easy, since the inequalities are open and homogeneous, so we should get cones that are non-empty, since we start with x that lies in these cones.

Second, we show that if we have open cones, then we can fit the congruence condition. This should be a "density" argument: an open cone and a lattice should meet.

How does that sound? I have not yet written down the statements, nor the frame of the proof of Lemma 9.7, so some details might change.

#### Damiano Testa (Jan 26 2021 at 08:20):

I think that cones are not in mathlib. We could introduce them as submodules for ℝ≥0 in an add_comm_semigroup with an ℝ≥0 action. We could probably get rid of ℝ and work with a linearly ordered group_with_zero. I am less sure about this.

#### Johan Commelin (Jan 26 2021 at 08:24):

you'll need a semiring, if you want to use mathlibs submodules, right?

#### Damiano Testa (Jan 26 2021 at 08:26):

Ah, you are right. It would be the comm_semiring of the non-negative reals.

#### Damiano Testa (Jan 26 2021 at 08:27):

Still, I think that breaking off the "inequalities" from the "congruences" will make the arguments easier to write and prove.

sounds good

#### Damiano Testa (Jan 26 2021 at 08:28):

I am teaching in half an hour, so I am not sure that I can have a skeleton ready before that, but I will try!

#### Damiano Testa (Jan 26 2021 at 08:37):

Since I am not too familiar with structures, does this seem reasonable?

structure cone (V : Type*) [normed_group V] [normed_space ℝ V] :=
(carrier : set V)
(add_mem : ∀ {a b : V}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier)
(nonneg_smul_mem : ∀ {r : ℝ}, ∀ {a : V}, 0 ≤ r → a ∈ carrier → r • a ∈ carrier)


Updated version with nonneg instead of pos.

#### Johan Commelin (Jan 26 2021 at 08:41):

@Damiano Testa from a lean side, yes. From a maths side: can cones be empty? Or do you want zero_mem?

#### Johan Commelin (Jan 26 2021 at 08:41):

if yes, then I would change pos_smul_mem to nonneg_smul_mem

#### Damiano Testa (Jan 26 2021 at 08:42):

For this specific application, I am thinking of open half-spaces, and I thought that having a strict inequality might be better. I do not know whether this is really a good idea, though.

#### Johan Commelin (Jan 26 2021 at 08:42):

you know more about the maths than I do

#### Damiano Testa (Jan 26 2021 at 08:43):

From the presence of a point, I would like to deduce the existence of an open containing it (and inside the cone). I am hoping to eliminate a few boundary cases like this, but I may simply be shuffling the problem around... I am not sure.

#### Damiano Testa (Jan 26 2021 at 08:44):

However, I do not have the time to play with either of the two possibilities before my class/meetings. I am not convinced that the positivity assumption will solve more problems than it creates.

#### Johan Commelin (Jan 26 2021 at 08:45):

My intuition says that you should prove this for nontrivial cones (-;

#### Damiano Testa (Jan 26 2021 at 08:46):

In any case, the first few lemmas will be about the fact that a (open/closed) half-space is a cone, that an intersection of cones is a cone... these will require small tweaks, if we change the inequality, right?

#### Damiano Testa (Jan 26 2021 at 08:46):

Ah, ok, I like the non-triviality!

#### Damiano Testa (Jan 26 2021 at 08:46):

Ok, I will make it non-negative multiplication. It may also be useful to have a zero element.

#### Damiano Testa (Jan 26 2021 at 08:48):

I changed the definition above: our conversation appears meaningless now, but the code is correct!

#### Johan Commelin (Jan 26 2021 at 08:50):

Ooh, but you still don't have a 0 (-;

#### Damiano Testa (Jan 26 2021 at 08:50):

With this definition the open first quadrant in R^2 union the origin is a cone. While I am not opposed to this, it will be something to keep in mind when proving stuff about cones.

#### Damiano Testa (Jan 26 2021 at 08:51):

Well, empty is easy to split off, no?

#### Damiano Testa (Jan 26 2021 at 08:51):

or should I assume zero_mem?

#### Johan Commelin (Jan 26 2021 at 08:52):

If you do, then it's literally submodule nnreal V, right?

#### Johan Commelin (Jan 26 2021 at 08:52):

(You might need an is_scalar_tower nnreal real V instance for real vector spaces, if that doesn't yet exist.)

#### Damiano Testa (Jan 26 2021 at 08:52):

I have not worked with nnreal, but given the name, I suspect that it is!

#### Damiano Testa (Jan 26 2021 at 08:53):

So, maybe I can work with submodule nnreal V and then try to make statements about the submodules with non-empty interior.

#### Peter Scholze (Jan 26 2021 at 08:53):

Just a quick comment that the proof of 9.7 really makes critical use of the fact that the cones are defined by inequalities with rational coefficients. And the argument is also only really working with closed cones.

#### Johan Commelin (Jan 26 2021 at 08:53):

It is \R\ge0 for people with unicode keyboards...

Ooh well, I guess I can type $\mathbb{R}_{\ge0}$

#### Damiano Testa (Jan 26 2021 at 08:55):

Peter, thank you for your comment: I will keep it in mind!

In any case, Lean will not allow me to prove something that is not true! :wink:

#### Peter Scholze (Jan 26 2021 at 08:56):

sure :-)! I think the central part of the argument even has an official name (blahblah's lemma or so), let me try to find it again...

#### Peter Scholze (Jan 26 2021 at 08:57):

Gordan's lemma it is: https://en.wikipedia.org/wiki/Gordan%27s_lemma

#### Damiano Testa (Jan 26 2021 at 08:57):

At the moment, I am trying to get to a stage where proving that a non-empty open cone contains a basis. Once there will be enough lemmas to get there, I think that we can focus on the actual proof of the lemma and the tools that are needed specifically for that.

#### Damiano Testa (Jan 26 2021 at 08:58):

Thanks for the reference!

#### Peter Scholze (Jan 26 2021 at 08:58):

What do you mean by basis here?

#### Damiano Testa (Jan 26 2021 at 08:59):

I mean a basis of the rational vector space (In my mind, this is a statement about lattices and I constantly change between the integers and the rationals.)

#### Damiano Testa (Jan 26 2021 at 08:59):

The reals might be useful, since there are a lot of results about real stuff already in Lean, which is why I am starting with R.

#### Damiano Testa (Jan 26 2021 at 08:59):

I now have to "go" to my virtual class!

#### Peter Scholze (Jan 26 2021 at 08:59):

ah, just a basis for the vector space, not for the cone

#### Peter Scholze (Jan 26 2021 at 09:00):

OK, nice chatting with you!

Yes, indeed!

#### Damiano Testa (Jan 26 2021 at 09:00):

more on this later!

#### Sebastien Gouezel (Jan 26 2021 at 09:23):

There are already cones in mathlib, in analysis/convex/cone.

docs#convex_cone

#### Johan Commelin (Jan 26 2021 at 09:33):

@Sebastien Gouezel ooh, thanks for the pointer. Not sure why I forgot about that :face_palm:

#### Sebastien Gouezel (Jan 26 2021 at 09:35):

The problem when you grep for cone is that you have too much of it in category theory. I grepped for convex_cone instead :-)

#### Filippo A. E. Nuccio (Jan 26 2021 at 10:36):

@Damiano Testa I am teaching the whole day today and I am finishing another project, so I have been only thinking superficially at the problem. I also agree that one can split things up. I though about making a separate lemma for the case where all $x(\lambda_i)$ are positive, and then to take the union, which is the strategy in the paper, basically. I was also thinking about removing the freeness assumption, since at any rate any hom from a torsion group to $\mathbb{Z}$ would be trivial (of course, I did not want to remove the f.g. one...). So I was trying to go in a different direction, but yours seems reasonable, and I'll look at it asap.

#### Damiano Testa (Jan 26 2021 at 14:00):

I am looking at convex_cone in mathlib and I am tempted to simply use this notion. It uses pos_mul, rather than nonneg_mul. In any case, I do not think that it would be a great deal to switch from one to the other.

I will import it, start playing with it and see how it pans out!

#### Adam Topaz (Jan 26 2021 at 15:33):

Hey, I'm just catching up on this discussion now. Why isn't a convex cone defined as a nnreal submodule of a real vectorspace?

#### Adam Topaz (Jan 26 2021 at 15:34):

Or I guess I should say "subsemimodule" or whatever.

#### Johan Commelin (Jan 26 2021 at 15:34):

might be historical reasons...

#### Damiano Testa (Jan 26 2021 at 15:35):

I think that the role of 0 is special in cones, and it may be better sometimes, to not automatically assume that 0 is in all cones.

#### Damiano Testa (Jan 26 2021 at 15:35):

However, I agree that whether you always add 0, or only sometimes, will not create any huge difference in the theory!

#### Adam Topaz (Jan 26 2021 at 15:54):

Is the definition of polyhedral lattice in the repo actually correct? I'm trying to fill in the sorry in polyhedral_lattice.lean and I get to the following:

instance int : polyhedral_lattice ℤ :=
{ tf := λ m hm n h,
begin
rw [← nsmul_eq_smul, nsmul_eq_mul, mul_eq_zero] at h,
simpa only [hm, int.coe_nat_eq_zero, or_false, int.nat_cast_eq_coe_nat] using h
end,
polyhedral' :=
begin
use {1},
split,
{ simp [finset.coe_singleton],
rw eq_top_iff,
rintro n -,
rw submodule.mem_span_singleton,
use n,
rw [← gsmul_eq_smul, gsmul_one, int.cast_id] },
{ intros x,
let b : {a : ℤ // a ∈ ({1} : finset ℤ)} := ⟨1,by simp⟩,
have : (finset.univ : finset {a // a ∈ ({1} : finset ℤ)}) = {b}, by tauto,
erw this,
simp,
-- ∥ x b • 1 ∥ = x b • 1
},
end }


#### Adam Topaz (Jan 26 2021 at 15:55):

Full context:

x : {a // a ∈ {1}} → ℤ,
b : {a // a ∈ {1}} := ⟨1, _⟩,
this : finset.univ = {b}
⊢ ∥x b • 1∥ = x b • 1


#### Johan Commelin (Jan 26 2021 at 16:00):

@Adam Topaz I might have messed up! I just tried to get the ball rolling.

#### Adam Topaz (Jan 26 2021 at 16:01):

The following seems more reasonable, no?

class polyhedral_lattice (A : Type*) [normed_group A] :=
(tf : torsion_free A)
(polyhedral' [] : ∃ s : finset A, submodule.span ℤ (s : set A) = ⊤ ∧
∀ n : {a // a ∈ s} → ℤ, ∥∑ a, n a • a.1∥ = ∑ a, ∥ n a ∥ • ∥a.1∥)


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

Yes, a lot more (-;

#### Johan Commelin (Jan 26 2021 at 16:07):

Maybe we want abs around the integer, I don't know. That's a design decision. But at least your version is maths-correct, and mine wasn't.

#### Adam Topaz (Jan 26 2021 at 16:07):

Is it obvious that this matches the definition in analytic.pdf on page 59?

#### Adam Topaz (Jan 26 2021 at 16:08):

(In any case, I made the change and killed the sorry, and pushed)

#### Johan Commelin (Jan 26 2021 at 16:09):

Is it obvious that this matches the definition in analytic.pdf on page 59?

Not obvious-obvious to me. It would be good to get something closer to p59. But that definition looks complicated to work with in Lean.

#### Filippo A. E. Nuccio (Jan 26 2021 at 17:40):

@Damiano Testa @Adam Topaz I have just git pulled and it seems to me that the statement of Lemma 9.7 is still the same. Are you working on paper (I'm also trying to...) or have I missed something?

#### Adam Topaz (Jan 26 2021 at 17:40):

Oh, I changed the definition of polyherdral_lattice.

#### Adam Topaz (Jan 26 2021 at 17:43):

Which file has the statement of Lemma 9.7?

#### Filippo A. E. Nuccio (Jan 26 2021 at 17:43):

combinatorial_lemma.lean

(deleted)

(deleted)

#### Damiano Testa (Jan 26 2021 at 19:44):

I did not push anything yet: I was trying to get somewhere more stable before doing so.

#### Filippo A. E. Nuccio (Jan 27 2021 at 10:37):

@Damiano Testa I have seen you're now actively working on polyhedral lattices. Do you think the "new" formulation you're heading to will make Lemma 9.7 useless or are you still also working on it? I am trying to come up with a " purely algebraic" strategy for it, using duals of free f.g. abelian groups, but I wonder if this is useless/obsolete.

#### Damiano Testa (Jan 27 2021 at 10:40):

I am not sure which strategy will work best in Lean, so at the moment, I think that we should all try to make it work and we will find out later which approach is more successful. I am still trying to get the proof of 9.7 in place, though!

#### Peter Scholze (Jan 27 2021 at 10:52):

I'm excited to watch this progress! But I'm curious: In which sense would Lemma 9.7 become useless?

#### Filippo A. E. Nuccio (Jan 27 2021 at 10:55):

No, no, I was wondering if Damiano and others were finding another path. I don't think it will (and really: it was simply a question before starting formalizing it, not any kind of "hint")

#### Damiano Testa (Jan 27 2021 at 10:55):

I am not sure that it will become useless, but I would interpret this as "the proof will fall out from a formalization of the polyhedral stuff".

#### Peter Scholze (Jan 27 2021 at 11:05):

OK, that sounds good :-). So you are actually saying that you will formalize Lemma 9.7, but just as part of a much larger effort on polyhedral lattices?

#### Damiano Testa (Jan 27 2021 at 14:00):

My impression is that a lot of the tools that will go into polyhedral lattices will also be useful to prove lemma 9.7. When formalizing something, you start by proving lots of very trivial results and it makes sense to make sure to only require lots of trivial results only once! So, I think that trying to get polyhedral stuff into Lean might yield useful tools to prove lemma 9.7.

At the same time, working on the concrete goal of proving lemma 9.7 is also useful to see which results will be needed and which ones will not. So, maybe the two streams will go parallel, but closeby!

#### Filippo A. E. Nuccio (Jan 27 2021 at 14:37):

Indeed, I believe that if we have a good understanding of free modules, proving Lemma 9.7 it should be "easy". But I don't know if Lean contains the statement that if you have $n$ linearly independent elements $\mu_1,...\mu_n$ in $\mathbb{Z}^k$ then you can produce a linear map $f\colon\mathbb{Z}^k\to\mathbb{Z}$ taking any chosen values $\alpha_i$ on each $\mu_i$.

#### Johan Commelin (Jan 27 2021 at 14:39):

Lean's biggest problem is that you can't call the elements $\lambda_i$...

Corrected :wink:

#### Kevin Buzzard (Jan 27 2021 at 15:02):

This isn't true for my understanding of linearly indepedent -- you can't send 2 to 1 without introducing denominators. But I should think that this sort of thing is either there already or would be easily doable

#### Johan Commelin (Jan 27 2021 at 15:03):

I think we can just use basis from linear algebra

#### Damiano Testa (Jan 27 2021 at 15:11):

It may also be the case that simply using the submodule spanned by the images is all we need...

#### Filippo A. E. Nuccio (Jan 27 2021 at 15:12):

Kevin Buzzard said:

This isn't true for my understanding of linearly indepedent -- you can't send 2 to 1 without introducing denominators. But I should think that this sort of thing is either there already or would be easily doable

Oh sure! I meant to say that they were part of a basis.

#### Adam Topaz (Jan 27 2021 at 15:13):

The words free_module don't even show up in the mathlib API search :sad:

#### Filippo A. E. Nuccio (Jan 27 2021 at 15:14):

The words free_module don't even show up in the mathlib API search :sad:

Yes, that is what I had realized. But I hoped to dig a bit better in the linear_algebra file.

#### Riccardo Brasca (Jan 27 2021 at 15:14):

But free_abelian_group does!

#### Adam Topaz (Jan 27 2021 at 15:15):

Is there a docs#free_abelian_group.lift ?

#### Adam Topaz (Jan 27 2021 at 15:17):

So this lift is what @Filippo A. E. Nuccio was looking for, right?

#### Filippo A. E. Nuccio (Jan 27 2021 at 15:18):

Oh wow, it can very well be! I am teaching now and will have a deep look at this tonight. Thanks!

#### Adam Topaz (Jan 27 2021 at 15:18):

Or do you want to lift with respect to some other basis which need not be the "standard" basis?

#### Filippo A. E. Nuccio (Jan 27 2021 at 15:18):

I don't know yet, honestly. But will try to find out soon and post here what I end up with.

#### Johan Commelin (Jan 27 2021 at 15:46):

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

#### Johan Commelin (Jan 27 2021 at 15:47):

Because once we start taking powers and quotients, you still want your API to work

#### Johan Commelin (Jan 27 2021 at 15:48):

The other option is that we completely rewrite the proof of 9.5 to only use lattices of the form $\mathbb{Z}^k$. But that doesn't seem natural.

#### Adam Topaz (Jan 27 2021 at 15:55):

Johan Commelin said:

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

Since we're ignoring universes for the most part, perhaps it makes sense to write down the usual universal property of the free module as the characteristic predicate?

#### Johan Commelin (Jan 27 2021 at 15:59):

can't we just define it as "have a finite basis", and then prove the universal property?

Sure.

#### Adam Topaz (Jan 27 2021 at 16:00):

Don't we have this somewhere in the repo already?

#### Johan Commelin (Jan 27 2021 at 16:06):

nope, I don't think so

#### Filippo A. E. Nuccio (Jan 27 2021 at 17:29):

Johan Commelin said:

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

@Johan Commelin Can you speculate a bit about this notion of "characteristic predicates", or point to a reference? In particular, what would the issue with quotients/powers be? Concerning rewriting 9.5 entirely, I want to insist that I haven't finished my proof on paper yet, so if the rewriting has to do with Lemma 9.7 in light of using free abelian groups, please wait! May be Damiano's approach will be more efficient and his work on polyhedral lattices will be the right path.

#### Adam Topaz (Jan 27 2021 at 17:31):

@Filippo A. E. Nuccio for example we would want the fact that the product of two free modules is free, so you want to characterize free modules in some way that makes it easy to obtain such facts.

#### Filippo A. E. Nuccio (Jan 27 2021 at 17:32):

Makes sense, sure. But why is

def free_abelian_group : Type u :=
additive $abelianization$ free_group α


"bad" in this perspecitve? Do we like something like a is_free_abelian_group : (Type *) ---> Prop more?

#### Adam Topaz (Jan 27 2021 at 17:32):

because the definitions dont matter :rofl:

#### Adam Topaz (Jan 27 2021 at 17:33):

It's not bad per se. Rather it's just a construction that says "hey, look, the free abelian group on a type \alpha actually exists."

#### Adam Topaz (Jan 27 2021 at 17:34):

But this is somehow separate from the characterization of free modules that Johan was referring to.

#### Johan Commelin (Jan 27 2021 at 17:35):

@Filippo A. E. Nuccio if you write a lot of lemmas about free_abelian_group X, then you cannot apply those lemmas to (free_abelian_group X) \times (free_abelian_group Y). If instead, you prove the lemmas about torsion free groups with a finite basis, then everything is fine.

#### Johan Commelin (Jan 27 2021 at 17:36):

Same thing with (fin n) -> \Z and finsupp (fin n) \Z and 37 other ways that we can build free abelian groups.

#### Johan Commelin (Jan 27 2021 at 17:37):

You want lemmas that work for all of those. So you need to find a characterisation that takes an arbitrary group as input, and asserts that it behaves like a free_abelian_group X.

#### Filippo A. E. Nuccio (Jan 27 2021 at 17:37):

Ok, so something like is_free_abelian_group : (Type *) ---> Prop?

#### Johan Commelin (Jan 27 2021 at 17:38):

Or maybe is_free (R) (M) that characterizes free modules

#### Mario Carneiro (Jan 27 2021 at 17:38):

More like is_free_abelian_group A X : Prop

#### Adam Topaz (Jan 27 2021 at 17:38):

import linear_algebra.basis

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

class fg_free_module :=
(S : set M)
(finite : S.finite)
(is_basis : is_basis A (coe : S → M))


#### Mario Carneiro (Jan 27 2021 at 17:38):

which says A ~= free_abelian_group X

#### Adam Topaz (Jan 27 2021 at 17:38):

that's not quite right....

#### Johan Commelin (Jan 27 2021 at 17:38):

I don't know if we want to fix the basis in the predicate, or only assert the existence.

#### Filippo A. E. Nuccio (Jan 27 2021 at 17:39):

Yes, it seems dangerous to fix the basis, I believe, no?

#### Johan Commelin (Jan 27 2021 at 17:39):

@Adam Topaz your class is not a Prop

#### Filippo A. E. Nuccio (Jan 27 2021 at 17:39):

These would be "framed free groups", no?

#### Mario Carneiro (Jan 27 2021 at 17:39):

for fg you probably want to quantify over it

#### Adam Topaz (Jan 27 2021 at 17:39):

Better:

import linear_algebra.basis

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop := ∃ (S : set M), S.finite ∧ (is_basis A (coe : S → M))


#### Mario Carneiro (Jan 27 2021 at 17:40):

Why is S a subset of M instead of just an arbitrary finite type or fin n?

#### Johan Commelin (Jan 27 2021 at 17:40):

I think we can then continue to prove theorems about arbitrary fintypes with basis-maps to M.

#### Adam Topaz (Jan 27 2021 at 17:41):

import category_theory.Fintype
import linear_algebra.basis

open category_theory

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop := ∃ (S : Fintype) (ι : S → M), (is_basis A ι)


:smile:

#### Johan Commelin (Jan 27 2021 at 17:41):

which universe does S live in?

Does it matter?

#### Mario Carneiro (Jan 27 2021 at 17:41):

I would suggest quantifying only over fin n and proving the fintype version

#### Mario Carneiro (Jan 27 2021 at 17:42):

because there is a universe issue as johan points out

#### Adam Topaz (Jan 27 2021 at 17:42):

docs#category_theory.Fintype.skeleton

#### Johan Commelin (Jan 27 2021 at 17:42):

but why not just use the finset in the defn?

#### Mario Carneiro (Jan 27 2021 at 17:42):

I think the finset adds an unnecessary injectivity restriction

#### Adam Topaz (Jan 27 2021 at 17:43):

If you use fin n, then you would need to go back and forth with the equuivalence between fin n \sum fin mand fin (n+m) which isn't much fun.

#### Johan Commelin (Jan 27 2021 at 17:43):

is_basis makes it injective, right?

#### Mario Carneiro (Jan 27 2021 at 17:43):

yes it's a basis so injectivity is almost always redundant, but it's an extra thing that has to be dealt with in proofs

#### Adam Topaz (Jan 27 2021 at 17:44):

import category_theory.Fintype
import linear_algebra.basis

open category_theory

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop := ∃ (S : Fintype.{0}) (ι : S → M), (is_basis A ι)


#### Johan Commelin (Jan 27 2021 at 17:44):

I don't really care. We want a defn and 37 constructors (-;

#### Mario Carneiro (Jan 27 2021 at 17:45):

To clarify, with the fin n version you have a constructor

def fg_free_module.mk (A) [fintype A] (f : A -> M) : is_basis A f -> fg_free_module A M


#### Mario Carneiro (Jan 27 2021 at 17:45):

and note that A can come from any universe

#### Damiano Testa (Jan 27 2021 at 18:30):

How hard would it be to work with the property that any surjective map to a free abelian group admits a section?

#### Johan Commelin (Jan 27 2021 at 18:34):

that should be a theorem, not a def

#### Johan Commelin (Jan 27 2021 at 18:35):

because it quantifies over types, which is better avoided

Ah, I see

#### Damiano Testa (Jan 27 2021 at 18:42):

And a finsupp from a (finite if wanted) Type to Z?

#### Johan Commelin (Jan 27 2021 at 18:44):

that shouldn't be a defn either, but an example of free abelian groups

#### Damiano Testa (Jan 27 2021 at 18:45):

Ok, I will keep quiet!

#### Johan Commelin (Jan 27 2021 at 18:45):

because the product of two finsupp _ _s is not of the form finsupp _ _

#### Johan Commelin (Jan 27 2021 at 18:46):

So you want a definition that works for all free abelian groups... not just for some constructions.
This is a concept that is somewhat strange for mathematicians. Because $\mathbb{Z}^m \times \mathbb{Z}^n = \mathbb{Z}^{m+n}$, right?

#### Johan Commelin (Jan 27 2021 at 18:46):

But lean will not agree about that =

#### Peter Scholze (Jan 27 2021 at 19:12):

I think algebraic topologists wouldnt agree either. Ask them about signs (or, in fact, all higher homotopy groups of spheres) arising from swapping factors ;-)

#### Kevin Buzzard (Jan 27 2021 at 19:23):

Here's a question I ran into the other day. Say we have a short exact sequence of short exact sequences, i.e. a 3x3 grid of modules (say for a group G) with all rows and columns exact. Say the top left hand module is $A_1$ and the bottom right is $C_3$. Using boundary maps we can construct two maps $H^n(G,C_3)\to H^{n+2}(G,A_1)$ (one going around two sides of the square, the other around the other two sides). Are these maps (a) the same, (b) different by a sign, (c) depends on conventions? Not a serious question, but it does remind you how scary this stuff is.

#### Adam Topaz (Jan 27 2021 at 19:39):

@Kevin Buzzard You just gave me something to give my students on their next homework assignment. Thanks.

#### Kevin Buzzard (Jan 27 2021 at 19:42):

I wanted to compute explicitly for n=0 but managed to get confused about what the explicit boundary map was from 1-cocycles to 2-cocycles. What do you tell your students is the map from 0-cocycles to 1-cocycles? Given $c\in C$ pull back to $b\in B$, and now the difference of $b$ and $gb$ is in $A$, and that's where you send $g$. But is it $b-gb$ or $gb-b$?

#### Adam Topaz (Jan 27 2021 at 19:43):

My go-to convention is $gb-b$.

#### Adam Topaz (Jan 27 2021 at 19:43):

.... I think.... I can't even remember...

#### Adam Topaz (Jan 27 2021 at 19:45):

Okay, my go-to convention is indeed $gb-b$ because [NSW] says so on page 15
https://www.mathi.uni-heidelberg.de/~schmidt/NSW2e/NSW2.1.pdf

#### Kevin Buzzard (Jan 27 2021 at 19:46):

So you agree that this is just a convention?

absolutely.

#### Kevin Buzzard (Jan 27 2021 at 19:49):

Is your convention for the map from C-valued 1-cocycles to A-valued 2-cocycles a second independent convention, or is it somehow tied down by your convention for 0-cocycles to 1-cocycles?

#### Adam Topaz (Jan 27 2021 at 19:52):

It's a priori independent, but I would generally follow the "consistent" formula from page 14 of [NSW] :smile:

#### Johan Commelin (Jan 27 2021 at 19:52):

Kevin Buzzard said:

Are these maps (a) the same, (b) different by a sign, (c) depends on conventions? Not a serious question, but it does remind you how scary this stuff is.

It depends on whether the first map goes clockwise and the second counter-clockwise around the diagram, or the other way round...

#### Adam Topaz (Jan 27 2021 at 19:57):

Maybe it is pinned down with the formula for the boundary of the cup-product.

#### Kevin Buzzard (Jan 27 2021 at 19:57):

p14 of NSW doesn't give conventions for signs for boundary maps, it seems to me, only for the definitions of the cohomology groups themselves. p15 of the version I'm looking at writes down an explicit map $H^0(C)\to H^1(A)$ which seems to come out of the blue, and of course there is the claim that it is "canonical".

#### Adam Topaz (Jan 27 2021 at 19:58):

Oh, I'm thinking of the usual thing where you choose a lift to the middle term of the exact sequence and apply the differential in the complex to obtain the bounday map on cohomology.

#### Riccardo Brasca (Jan 27 2021 at 19:59):

This is just because derived functors are defined via a universal property, so they are unique up to isomorphism, right?

#### Kevin Buzzard (Jan 27 2021 at 19:59):

but derived functors are not just a choice of cohomology groups, they are also a compatible choice of boundary maps for every short exact sequence.

#### Riccardo Brasca (Jan 27 2021 at 20:00):

Sure, they are unique up to isomorphism of $\delta$-functors, or whatever the terminology is

#### Kevin Buzzard (Jan 27 2021 at 20:00):

So in particular here is an isomorphism between group cohomology and itself -- it's the identity on $H^n$ for all $n\not=37$, and $-1$ for $n=37$. This changes some boundary maps.

#### Kevin Buzzard (Jan 27 2021 at 20:01):

In particular it does not even really make sense to ask what "the" boundary map $H^{36}(C)\to H^{37}(A)$ is. You have to tell me, when you're defining cohomology.

#### Kevin Buzzard (Jan 27 2021 at 20:02):

And there is certainly no guarantee that it is the same one that is being used in the references you're using.

#### Patrick Massot (Jan 27 2021 at 20:05):

Isn't there a famous paper by Deligne about all this fun?

#### Kevin Buzzard (Jan 27 2021 at 20:05):

Fortunately, the choices $H^n(C)\to H^{n+1}(A)$ all have to be compatible, so you can only change them all at once. This means that my question about $H^n(C_3)\to H^{n+2}(A_1)$ is at least well-defined, in the sense that it is independent of convention. It is either always the same for each route round the square, or always off by a sign.

#### Kevin Buzzard (Jan 27 2021 at 20:05):

Yes, I took a look at this paper only last week in an attempt to resolve this issue, but he doesn't go explicitly into this point.

#### Kevin Buzzard (Jan 27 2021 at 20:06):

I am still really confused about the cup product issue which Adam raised. Any diagram at all which has only one occurrence of a boundary map $H^n\to H^{n+1}$ -- it seems to me that it does not even make sense to ask whether it commutes until more information is given about the definitions of the boundary maps.

#### Peter Scholze (Jan 27 2021 at 20:09):

Well, it probably also uses maps from some concrete things into $H^n$'s, and then you have to look how those are defined in turn. If they make use of explicit cochain representatives, then yeah.

For the question, my guess is that it's $-1$; you seem to be swapping to degree $1$ maps, which should introduce a sign. Although you can surely find many papers of mine where I pretend it's the identity.

#### Kevin Buzzard (Jan 27 2021 at 20:17):

According to Neukirch it is indeed -1.

#### Kevin Buzzard (Jan 27 2021 at 20:26):

Oh Adam -- the 3x3 question is 1.3.4 in NSW, I just ran into it whilst looking through the book hoping for some more enlightenment about cup products. Amelia has been collapsing double complexes $C_{i,j}:=A_i\otimes B_j$ into single complexes and defining explicit boundary maps in Lean. Her collapsed $C_n:=\oplus_{i+j=n}C_{i,j}$ are fine, but when she defined the differential between them she simply had to choose between $(-1)^i$ and $(-1)^j$ at some point, and it really felt to me that it was just a coin-toss.

#### Kevin Buzzard (Jan 27 2021 at 20:32):

Got one: NSW 1.4.3 is a claim about a diagram commuting which has precisely one boundary map from degree $p+q$ to $p+q+1$. I don't even see how it makes sense to claim that this diagram commutes unless you announce your conventions and make it clear that anyone who uses that result needs to be using the same conventions for boundary maps. This is just like the nightmare I faced when writing some parts of Buzzard-Diamond-Jarvis and I had to try to figure out everyone's convention on Shimura varieties. Some people explicitly said they were using Deligne's convention for class field theory (typically the people working in large generality); some said explicitly they were using Artin's (typically the people doing Heegner point computations for Shimura curves over totally real fields, for whom the inverse is just an unnecessary bother for the equations they deal with) and some people simply did not say at all. Those folk of course had the best of both worlds, because in their ignorance they could borrow computations from all the literature instead of just half of it.

#### Adam Topaz (Jan 27 2021 at 20:32):

Sorry -- I have "zoom office hours" right now, so I can't really follow all the discussion...

#### Adam Topaz (Jan 27 2021 at 20:33):

But good to know that [NSW] has the details :)

#### Kevin Buzzard (Jan 27 2021 at 20:59):

I think I understand now. Let's say a pinning of a cohomology theory is a choice of signs for all boundary maps. Once it is pinned, then there is a choice of cup products $H^p(A)\times H^q(B)\to H^{p+q}(A\otimes B)$ whose sign depends on the pinning (i.e. if I change my boundary map $H^{37}(C)\to H^{38}(A)$ then some of these cup product maps change sign too) and which satisfies all the theorems in the book.

#### Adam Topaz (Jan 27 2021 at 21:11):

Yeah, that sounds reasonable. And as for the boundary map, in NSW they actually prove the snake lemma, and part of the proof is the "construction" of the boundary map, so that's what they take as their definition throughout.

#### Kevin Buzzard (Jan 27 2021 at 21:21):

I am still a bit confused by this because the boundary map in the snake lemma really _does_ feel like it's "more canonical than the other choice" -- like the obvious map from a vector space to its double-dual really is better than the one where you randomly introduce a minus sign.

#### Adam Topaz (Jan 27 2021 at 21:25):

What happens if we want to define group cohomology for semimodules :expressionless: ?

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:27):

But there is something I don't understand: Grothendieck writes in his Tohokou :

Soit $T = (T^i), 0 \leq i\leq a$ un $\delta$-foncteur
covariant de $C$ dans $C'$, où $a > 0$. $T$ est dit un $\delta$-foncteur universel si pour tout $\delta$-foncteur $T '= (T'^i)$ fonctoriel défini pour les mêmes degrés, et tout morphisme fonctoriel $f^{i_0}$ de $T^{i_0}$ dans $T'^{i_0}$, il existe un seul morphisme et un seul $f$ de $T$ dans $T'$ qui pour le degré $i_0$ se réduise à $f^{i_0}$.

In particular, all our functors (say, group cohomology) are not universal $\delta$ functors, because the functorial isomorphism in question is not unique?

#### Adam Topaz (Jan 27 2021 at 21:28):

It is unique, but if you change the $\delta$ in one of these functors by $-\delta$ then you need to change the corresponding morphism comparing them as well.

#### Adam Topaz (Jan 27 2021 at 21:28):

At least I think that's the idea...

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:29):

Well, but if I can change the 37-th, I have infinitely many choices.

#### Adam Topaz (Jan 27 2021 at 21:29):

The boundary maps are part of the "data" of a $\delta$-functor.

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:29):

This I understand. But what is a universal one, then?

#### Adam Topaz (Jan 27 2021 at 21:31):

It's one satisfying the universal property, which says that for all blah blah blah there exists a unique morphism such that blah blah. So if I multiply the boundary map by $-1$ in such a universal delta functor, it's still universal, but the "unique morphism" will be different...

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:31):

Ah, I see. If I take two cohomology theories, one with a certain $\delta_{37}$ and the other with all the $\delta_i$'s equal to those of the first, but the 37-th, then the map comparing them is unique.

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:35):

Kevin Buzzard said:

I am still a bit confused by this because the boundary map in the snake lemma really _does_ feel like it's "more canonical than the other choice" -- like the obvious map from a vector space to its double-dual really is better than the one where you randomly introduce a minus sign.

If you're looking at the snake lemma on page 25 of NSW leading to Theorem 1.3.2, I agree that it is somehow "more canonical that the other choice", but the $\partial_\ast$ are not.

#### Filippo A. E. Nuccio (Jan 27 2021 at 21:36):

They are defined explicitly through the alternating sum on page 15, I guess, and there is clearly a choice of sign there (you can index from 0 to n or from 1 to n+1, affecting the $(-1)^n$).

#### Patrick Massot (Jan 27 2021 at 22:10):

This is all nice and fun, but we drifted quite a bit. I think we should try to stay closer to the main topic in this stream, otherwise Peter may miss messages that actually need his input.

#### Filippo A. E. Nuccio (Jan 27 2021 at 22:17):

Yes, I agree. Apologies to Peter, we might continue this discussion with @Kevin Buzzard and @Adam Topaz elsewhere.

#### Peter Scholze (Jan 27 2021 at 22:22):

I enjoy random conversations, don't bother about me :-)

#### Peter Scholze (Jan 27 2021 at 22:23):

By the way, for more fun regarding signs, this project actually also needs simplicial stuff, in the proof of 8.19 (used later when there is also some simplicial stuff in the main proof 9.5)

#### Filippo A. E. Nuccio (Jan 27 2021 at 22:26):

In the first part of its proof, when you split the hypercover?

#### Peter Scholze (Jan 27 2021 at 22:26):

well, the statement itself is simplicial!

#### Peter Scholze (Jan 27 2021 at 22:27):

or do you mean the signs? I just mean that in Dold-Kan etc you can surely have fun fixing all the signs

#### Filippo A. E. Nuccio (Jan 27 2021 at 22:27):

Yes, I meant the signs.

#### Filippo A. E. Nuccio (Jan 27 2021 at 22:28):

(And we might debate if "fun" is the most appropriate word... :smile: )

#### Peter Scholze (Jan 27 2021 at 22:28):

Sorry, this is my sense of humour ;-)

#### Peter Scholze (Jan 27 2021 at 22:29):

well, anyways I'm off for tonight. See you around!

See you, bye!

#### Filippo A. E. Nuccio (Jan 29 2021 at 19:19):

I am a bit confused about the sign requirement of Lemma 9.7: now it reads

the numbers $x'(\lambda_i)$ and $(x-x')(\lambda_i)$ have the same sign

but I wonder if it should not be

the numbers $x(\lambda_i)$ and $(x-x')(\lambda_i)$ have the same sign

Or am I misunderstanding the idea of the lemma?

#### Peter Scholze (Jan 29 2021 at 20:41):

The first implies the second, and I really want the first

#### Filippo A. E. Nuccio (Jan 29 2021 at 21:05):

Ah, ok. I agree that the first implies the second, but I thought the second was enough

#### Filippo A. E. Nuccio (Jan 29 2021 at 21:07):

@Johan Commelin I think you have coded the second, weaker version of the inequality in the file. No?

#### Johan Commelin (Jan 29 2021 at 21:51):

Ooh, my bad. That must have been a typo. Please fix it.

#### Filippo A. E. Nuccio (Jan 30 2021 at 13:55):

Ok, fixed and pushed.

#### Peter Scholze (Feb 02 2021 at 19:45):

Let's continue this conversation in the proper thread. Are you OK with the proof as given? I assume Gordan's lemma is the nontrivial part in the formalization?

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:52):

Yes, indeed. I agree with the proof, although it took me a while to figure out the $x(\lambda_i)\geq 0$ vs $x'(\lambda_i)\geq 0$ business. But as you explained the other day, it is the second that you need.

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:54):

Indeed, formalizing Gordan's lemma seems a bit painful: I am more and more going to convince myself that the prove isn't that hard: basically, a compact intersected with a discrete is finite, more or less. And this is certainly in mathlib. But I need that the dual of a free module is free, and to extract the positive cone from it. This I still do not know how to do.

#### Peter Scholze (Feb 02 2021 at 19:54):

The first proof here https://en.wikipedia.org/wiki/Gordan's_lemma seems like it shouldn't be too hard

I see

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:55):

The final part with the congruences should really be painless.

#### Peter Scholze (Feb 02 2021 at 19:55):

But actually, you don't need a basis -- these cones may need more generators than the vector space

Right

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:56):

Still I need that it is f.g., and for this I ended up thinking if it wasn't possible to have a more constructive proof.

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:58):

Assuming always that $x$ is in the "positive dual cone", I wanted to somehow produce the $x'$ by looking at successive minima : fix $\lambda_1$ and look for a $x_0$ which takes on $\lambda_1$ the minimum, on all $x\in\Lambda_+^\vee$ of $x(\lambda_1)$.

#### Peter Scholze (Feb 02 2021 at 19:58):

Aha. That seems tricky.

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:59):

Then do the same for $\lambda_2$, etc... Of course, this will hugely depend on the choice of the ordering, but there are $m!$ choices.

#### Filippo A. E. Nuccio (Feb 02 2021 at 19:59):

(was $m$ the number of $\lambda$'s?)

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:00):

I was thinking about that tonight and had been teaching the whole day, so I haven't checked whether this makes sense.

#### Peter Scholze (Feb 02 2021 at 20:00):

For the proof on wikipedia, you effectively need that if in a finite-dimensional $\mathbb Q$-vector space $V$, if you intersect finitely many half-spaces $f(v)\geq 0$ where $f$ is a linear function on $V$, then this $\mathbb Q_{\geq 0}$-module is finitely generated. (Once you have that, the rest of the proof on wikipedia should be easy to get.)

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:00):

If you see an evident obstruction, I might give up, otherwise, I'll think a little bit in this direction for a while.

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:01):

Peter Scholze said:

For the proof on wikipedia, you effectively need that if in a finite-dimensional $\mathbb Q$-vector space $V$, if you intersect finitely many half-spaces $f(v)\geq 0$ where $f$ is a linear function on $V$, then this $\mathbb Q_{\geq 0}$-module is finitely generated. (Once you have that, the rest of the proof on wikipedia should be easy to get.)

I agree.

#### Peter Scholze (Feb 02 2021 at 20:01):

Well, I really think it would be cleanest to prove Gordan's lemma

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:01):

Surely cleanest, you're right.

#### Peter Scholze (Feb 02 2021 at 20:02):

OK, so how does one get at that result on $\mathbb Q$-vector spaces...

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:03):

This should be what @Damiano Testa has been thinking about for a while, I haven't started yet.

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:03):

In particular, I haven't done a good analysis of what is in mathlib yet to know what is missing.

I see

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:05):

Already the dual cone scares me a bit (I mean: to show it is a cone), but I really need to think more before talking nonsense.

#### Peter Scholze (Feb 02 2021 at 20:07):

yeah, that's why I wrote that statement about $\mathbb Q_{\geq 0}$-modules above -- I think it gets more directly to the point than defining cones

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:11):

I'll be thinking about the statement and will put here any advance. Now I really have to run for dinner, but as soon as I get somewhere I'll post here what I have.

#### Filippo A. E. Nuccio (Feb 02 2021 at 20:11):

Thanks for the clues! :wave:

#### Damiano Testa (Feb 03 2021 at 14:49):

Sorry for going quiet a bit. I will have more time on Friday, and only a few scattered moments before that.

Anyway, I had also converged on the fact that the main statement that we should formalize is that intersecting finitely many half-spaces in $\mathbb{Q}_{\geq 0}$ is finitely generated. I will try to at least formulate a statement that asserts this fact and will report back once I have it!

#### Johan Commelin (Mar 10 2021 at 07:12):

I think we are now at a point where we can state a version of Gordan's lemma (https://en.wikipedia.org/wiki/Gordan%27s_lemma) that we think will be nice to work with. @Damiano Testa is working hard on all the machinery needed to prove Gordan's lemma. But at the same time, we can start trying to prove lemma 9.7 assuming Gordan's lemma.

#### Filippo A. E. Nuccio (Mar 15 2021 at 15:54):

I made some advances for lemma 9.7. Assuming @Damiano Testa 's proof of Gordan's lemma, I have set-up the reduction step. What needs to be proved is only the "positive case", so the claim for all $x$ which pair positively with all $\lambda_i$'s, which should be quite easy (am I writing this? :thinking: ) using Gordan's lemma.

#### Filippo A. E. Nuccio (Mar 15 2021 at 15:55):

The file still has a lot of "easy" sorry's, so I don't know how to proceed. Is it better to pull it to master or to wait to have it sorry-free?

#### Johan Commelin (Mar 15 2021 at 15:55):

No, just push to master

#### Johan Commelin (Mar 15 2021 at 15:56):

sorry s are fine, but there shouldn't be errors

#### Filippo A. E. Nuccio (Mar 15 2021 at 15:56):

No, no, there are no errors (but I will double-check before pushing).

#### Filippo A. E. Nuccio (Mar 15 2021 at 15:57):

I will at any rate keep on working on this on the coming days (not so much for today, I fear, but who knows). If you find that the strategy is bad/needs a fundamental revision, please warn me.

#### Johan Commelin (Mar 15 2021 at 16:03):

@Filippo A. E. Nuccio I think I've pushed errors to master several times :see_no_evil: but I always try to fix them asap...

#### Filippo A. E. Nuccio (Mar 15 2021 at 16:14):

Ok, I've pushed my changes. I have to prepare my lesson for tomorrow, but I'll probably be around on Zulip and hope to resume the work later on in the evening.

#### Filippo A. E. Nuccio (Mar 19 2021 at 17:53):

I have just pushed a proof of the "reduction step" from the positive version of lemma 9.7 to the full one. There are still some very minor sorry's here and there concerning sign vectors, and I hope to get rid of them tonight.

#### Johan Commelin (Mar 19 2021 at 18:00):

Sounds great, thanks!

#### Johan Commelin (Mar 19 2021 at 20:11):

@Filippo A. E. Nuccio It seems that you renamed lem97' to lem97''. I adapted combinatorial_lemma.lean.

#### Filippo A. E. Nuccio (Mar 19 2021 at 22:55):

Oh yes, you're right. I ended up with three versions of the lemma before deciding which one to throw away, and modified yours since I did not know it was already quoted somewhere. Of course, it makes more sense to go back to the previous numbering, as having a lem97'' without lem97' seems odd...

#### Filippo A. E. Nuccio (Mar 19 2021 at 23:14):

@Johan Commelin I have renamed it back to lem97' and modified combinatorial_lemma.lean accordingly, so that it compiles. I have also started the proof of lem97' building on lem97. I arrived at the point where the three lemmas you put in the "preamble" are needed, and wanted to know if you confirm they're in mathlib (and where).

Thanks!

#### Filippo A. E. Nuccio (Mar 20 2021 at 12:19):

I'm running into some coercion issues that I don't really know how to solve. The current statement of lem97' contains something like N * (y (l i)).nat_abs + (x' (l i)).nat_abs and I would like to apply some of the lemmas pointed out at by @Riccardo Brasca . For this, I need to convert nat_abs  to abs, which I could do using int.abs_eq_nat_abs, but here the problem shows up. Since abs : ℤ → ℤ takes values in ℤ and nat_abs takes values in ℕ, the true equality is abs m = ↑ nat_abs m. Hence, I would need to change the statement to N * ↑(y (l i)).nat_abs + ↑(x' (l i)).nat_abs. But if I do so, then combinatorial_lemma.lean does not compile any longer (it is unhappy with the terms being integers rather than natural numbers, and I can't but sympathize with it).

#### Kevin Buzzard (Mar 20 2021 at 12:21):

You first want to zify and then use the fact that the coercion of nat_abs back to int is abs

#### Filippo A. E. Nuccio (Mar 20 2021 at 12:21):

zify?

#### Johan Commelin (Mar 20 2021 at 12:22):

A tactic that turns statements about nat into statements about int

#### Filippo A. E. Nuccio (Mar 20 2021 at 12:23):

Wonderful! :grinning:

And dreadful at the same time: I could have spent two days looking for it without ever finding it... :sad:

#### Johan Commelin (Mar 22 2021 at 15:21):

I saw that Filippo made some more progress here! Thanks

#### Filippo A. E. Nuccio (Mar 30 2021 at 18:54):

In the proof of Lemma 9.7 I am using that N \neq 0. I can either do a case distinction at the beginning, getting rid of the case N=0 or, what seems more reasonable to me (since we're going to divide by N at any rate) to assume throughout that N \neq 0. But this requires a bit of refactoring, to add the assumption everywhere. What is best?

#### Johan Commelin (Mar 30 2021 at 19:16):

@Filippo A. E. Nuccio I think [fact (0 < N)] is fine, and shouldn't require much refactoring (hopefully)

#### Patrick Massot (Mar 30 2021 at 19:30):

The standard procedure is to do a case distinction at the beginning, especially if this assumption helps only with this lemma.

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:20):

Great, in this case I will add this and do a bit of refactoring when/where needed. But do you think it would overall be a good idea to leave N explicit or to make it implicit at the beginning of the section/file?

#### Johan Commelin (Mar 31 2021 at 06:22):

I think N should be explicit almost everywhere

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:23):

OK, I will simply add then (hN: 0 < N) in the statement of all results in lem 97 and all those that depend on them...

#### Johan Commelin (Mar 31 2021 at 06:24):

Right, but if you use fact, then it might be automatic

#### Johan Commelin (Mar 31 2021 at 06:24):

Typeclass inference will just find the [fact (0 < N)] if you add it to variables at the top of the file

#### Johan Commelin (Mar 31 2021 at 06:25):

But is your lemma provable for N = 0?

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:25):

Yes, I do think it is (I haven't though about it and am teaching now, but a brief thought yesterday evening convinced me it is trivial in that case).

#### Johan Commelin (Mar 31 2021 at 06:26):

hmm... it looks like you can't get the finiteness in that case

#### Johan Commelin (Mar 31 2021 at 06:26):

anyway, I need to run now

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:26):

OK, can you point at a file using fact where I can see how to use it?

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:26):

(if not, I'll figure out)

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:37):

And no, you were right: N needs to be positive (and it is also required to be positive in the .pdf). So there is no choice.

#### Johan Commelin (Mar 31 2021 at 06:48):

@Filippo A. E. Nuccio If you add [hN : fact (0 < N)] as assumption, then hN.out (or hN.1) is a proof of 0 < N.

#### Johan Commelin (Mar 31 2021 at 06:49):

And afterwards you just add [fact (0 < N)] to all lemmas that need it.

#### Johan Commelin (Mar 31 2021 at 06:49):

Or you add it to a variables line, and then you need to change almost nothing, hopefully

#### Johan Commelin (Mar 31 2021 at 06:53):

Otherwise, it behaves the same way as [group G] etc

Thanks

#### Filippo A. E. Nuccio (Mar 31 2021 at 07:06):

Johan Commelin said:

Or you add it to a variables line, and then you need to change almost nothing, hopefully

Well, but for this I thought it needed to be implicit. What is the difference between

variables (T : Type*) [add_monoid T]
lemma foo : (T : Type*) [add_monoid T] T = 0 :=


and simply

lemma foo : (T : Type*) [add_monoid T] T = 0 :=


Also, what is the difference between hN : 0 < N  and [hN : fact (0 < N)] (i.e. : what's the magic in the word "fact")?

#### Johan Commelin (Mar 31 2021 at 07:09):

fact is a class, so you can use typeclass inference to automatically figure out those arguments.

#### Johan Commelin (Mar 31 2021 at 07:10):

With implicit, I thought you were talking about (N : nat) vs {N : nat}.

#### Filippo A. E. Nuccio (Mar 31 2021 at 07:14):

Yes, I agree it was misleading (and, given the role played in the paper, I agree it needs to be explicit). Thank for the explanation of the fact as an instance. Is it the same for declaring variables at the beginning of sections/files? I thought this was only useful if wanting to leave things implicit, but if they're explicit in the statement, is there a point in setting up variables at the beginning?

#### Filippo A. E. Nuccio (Mar 31 2021 at 09:04):

I am sorry but I'm unable to make this work. What I have now is

lem97_pos (N : nat) : blabla


and no variables. I can transform it in

lem97_pos (N : nat) (hN : 0 < N) : blabla


and then modify all calls to lem97_pos from apply lem_97pos \Lambda N to apply lem97_pos \Lambda N hN by adding hN : 0 < N to all statements relying on lem97_pos. But I guess you had a more clever solution...

#### Filippo A. E. Nuccio (Mar 31 2021 at 09:11):

Forget: it worked! :octopus:

#### Filippo A. E. Nuccio (Mar 31 2021 at 09:38):

Lemma 9.7 is now sorry-free.

#### Filippo A. E. Nuccio (Mar 31 2021 at 09:39):

I have pushed to master the final proof and have moved the file into the toric folder. Two things left:
1) Add a couple of things to mathlib from the move section: I am going to create the PR straight away, when they'll be in mathlib I'll remove from them from the file.
2) Prove Gordan...

#### Johan Commelin (Mar 31 2021 at 09:43):

Filippo A. E. Nuccio said:

Lemma 9.7 is now sorry-free.

That's great!

#### Filippo A. E. Nuccio (Mar 31 2021 at 09:52):

Well, actually there is a problem on line 250 of combinatorial_lemma, but this has nothing to do with lemma 9.7 (I realized this because I modified the final part of the file, where it calls lemma_97)

#### Filippo A. E. Nuccio (Mar 31 2021 at 10:15):

(It occurs in the proof of lemma lem98_int)

#### Johan Commelin (Mar 31 2021 at 10:16):

Is this on your branch? master seems to compile just fine

#### Filippo A. E. Nuccio (Mar 31 2021 at 11:00):

...hmm, let me update and build.

#### Filippo A. E. Nuccio (Mar 31 2021 at 11:27):

Yes, everything is fine now!

#### Filippo A. E. Nuccio (Mar 31 2021 at 11:28):

I'll now PR a couple of things to mathlib, and then I will need to slow a bit to concentrate also on another project. But in the spare time I'd like to work on the fact that quotients of polyhedral lattices are still polyhedral lattices. Where is it?

#### Johan Commelin (Mar 31 2021 at 11:35):

It's not true in general. Only some specific quotients are...

#### Johan Commelin (Mar 31 2021 at 11:37):

polyhedral_lattice/cech.lean, there are 4 sorrys.

• nr 1 will vanish when we have semi_normed_group quotients
• nr 2 and 3 are the ones you are looking for
• nr 4 is also a todo, shouldn't be too hard

#### Johan Commelin (Mar 31 2021 at 15:48):

I pushed \leanok to the blueprint! Green is taking over the graph (-;

#### Johan Commelin (Mar 31 2021 at 15:48):

Thanks again @Filippo A. E. Nuccio

#### Filippo A. E. Nuccio (Apr 01 2021 at 08:22):

I have just pushed a slightly improved version of lemma 9.7 avoiding PR anything to mathlib, as the results were too specific and could be golfed to two rw` (thanks @Eric Wieser ).

Last updated: May 09 2021 at 16:20 UTC