lemma 9.7

Stream: condensed mathematics

[Johan Commelin]

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]

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

[Filippo A. E. Nuccio]

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]

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]

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]

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

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]

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]

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]

@Amelia Livingston has some partial progress on this

[Filippo A. E. Nuccio]

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

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

Sorry to read your message so late, but I'm eager to read anything she's been doing, in case you ended up asking.

[Kevin Buzzard]

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]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

sounds good

[Damiano Testa]

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]

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]

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

[Johan Commelin]

if yes, then I would change pos_smul_mem to nonneg_smul_mem

[Damiano Testa]

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]

you know more about the maths than I do

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

Ah, ok, I like the non-triviality!

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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]

Well, empty is easy to split off, no?

[Damiano Testa]

or should I assume zero_mem?

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Peter Scholze]

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]

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

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

Thanks for the reference!

[Peter Scholze]

What do you mean by basis here?

[Damiano Testa]

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]

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]

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

[Peter Scholze]

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

[Peter Scholze]

OK, nice chatting with you!

[Damiano Testa]

Yes, indeed!

[Damiano Testa]

more on this later!

[Sebastien Gouezel]

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

[Sebastien Gouezel]

docs#convex_cone

[Johan Commelin]

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

[Sebastien Gouezel]

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]

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

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]

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]

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

[Johan Commelin]

might be historical reasons...

[Damiano Testa]

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]

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

[Adam Topaz]

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]

Full context:

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

[Johan Commelin]

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

[Johan Commelin]

Please fix my blunders (-;

[Adam Topaz]

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]

Yes, a lot more (-;

[Johan Commelin]

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]

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

[Adam Topaz]

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

[Johan Commelin]

Adam Topaz said:

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]

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

Oh, I changed the definition of polyherdral_lattice.

[Adam Topaz]

Which file has the statement of Lemma 9.7?

[Filippo A. E. Nuccio]

combinatorial_lemma.lean

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

(deleted)

[Damiano Testa]

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

[Filippo A. E. Nuccio]

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

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]

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

[Filippo A. E. Nuccio]

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]

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]

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]

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]

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]

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

[Filippo A. E. Nuccio]

Corrected :wink:

[Kevin Buzzard]

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]

I think we can just use basis from linear algebra

[Damiano Testa]

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

[Filippo A. E. Nuccio]

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]

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

[Filippo A. E. Nuccio]

Adam Topaz said:

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]

But free_abelian_group does!

[Adam Topaz]

Is there a docs#free_abelian_group.lift ?

[Adam Topaz]

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

[Filippo A. E. Nuccio]

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

[Adam Topaz]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Adam Topaz]

Sure.

[Adam Topaz]

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

[Johan Commelin]

nope, I don't think so

[Filippo A. E. Nuccio]

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]

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

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]

because the definitions dont matter :rofl:

[Adam Topaz]

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]

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

[Johan Commelin]

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

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

More like is_free_abelian_group A X : Prop

[Adam Topaz]

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]

which says A ~= free_abelian_group X

[Adam Topaz]

that's not quite right....

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Mario Carneiro]

For free groups I think you want to fix the basis

[Johan Commelin]

@Adam Topaz your class is not a Prop

[Filippo A. E. Nuccio]

These would be "framed free groups", no?

[Mario Carneiro]

for fg you probably want to quantify over it

[Adam Topaz]

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]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

:smile:

[Johan Commelin]

which universe does S live in?

[Adam Topaz]

Does it matter?

[Mario Carneiro]

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

[Mario Carneiro]

because there is a universe issue as johan points out

[Adam Topaz]

docs#category_theory.Fintype.skeleton

[Johan Commelin]

but why not just use the finset in the defn?

[Mario Carneiro]

I think the finset adds an unnecessary injectivity restriction

[Adam Topaz]

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]

is_basis makes it injective, right?

[Mario Carneiro]

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]

Okay, how about this:

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]

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

[Mario Carneiro]

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]

and note that A can come from any universe

[Damiano Testa]

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

[Johan Commelin]

that should be a theorem, not a def

[Johan Commelin]

because it quantifies over types, which is better avoided

[Damiano Testa]

Ah, I see

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

Ok, I will keep quiet!

[Johan Commelin]

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

[Johan Commelin]

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]

But lean will not agree about that =

[Peter Scholze]

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]

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]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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]

So you agree that this is just a convention?

[Adam Topaz]

absolutely.

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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]

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]

According to Neukirch it is indeed -1.

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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]

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

[Filippo A. E. Nuccio]

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]

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]

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

[Filippo A. E. Nuccio]

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

[Adam Topaz]

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

[Filippo A. E. Nuccio]

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

[Adam Topaz]

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]

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]

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]

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]

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]

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

[Peter Scholze]

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

[Peter Scholze]

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]

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

[Peter Scholze]

well, the statement itself is simplicial!

[Peter Scholze]

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]

Yes, I meant the signs.

[Filippo A. E. Nuccio]

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

[Peter Scholze]

Sorry, this is my sense of humour ;-)

[Peter Scholze]

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

[Filippo A. E. Nuccio]

See you, bye!

[Filippo A. E. Nuccio]

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]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

Ok, fixed and pushed.

[Peter Scholze]

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]

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]

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]

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

[Peter Scholze]

I see

[Filippo A. E. Nuccio]

The final part with the congruences should really be painless.

[Peter Scholze]

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

[Filippo A. E. Nuccio]

Right

[Filippo A. E. Nuccio]

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]

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]

Aha. That seems tricky.

[Filippo A. E. Nuccio]

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]

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

[Filippo A. E. Nuccio]

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

[Peter Scholze]

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]

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]

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]

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

[Filippo A. E. Nuccio]

Surely cleanest, you're right.

[Peter Scholze]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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

[Peter Scholze]

I see

[Filippo A. E. Nuccio]

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]

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]

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]

Thanks for the clues! :wave:

[Damiano Testa]

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]

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]

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]

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]

No, just push to master

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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]

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

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]

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]

Sounds great, thanks!

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

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

[Riccardo Brasca]

Yes, they are now in mathlib... docs#abs_add_eq_add_abs_iff

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

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]

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]

zify?

[Johan Commelin]

A tactic that turns statements about nat into statements about int

[Filippo A. E. Nuccio]

Wonderful! :grinning:

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

[Johan Commelin]

I saw that Filippo made some more progress here! Thanks

[Filippo A. E. Nuccio]

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]

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

[Patrick Massot]

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]

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]

I think N should be explicit almost everywhere

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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

[Johan Commelin]

But is your lemma provable for N = 0?

[Johan Commelin]

I didn't think about it

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

anyway, I need to run now

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

(if not, I'll figure out)

[Filippo A. E. Nuccio]

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]

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

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

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

Thanks

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

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]

Forget: it worked! :octopus:

[Filippo A. E. Nuccio]

Lemma 9.7 is now sorry-free.

[Filippo A. E. Nuccio]

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]

Filippo A. E. Nuccio said:

Lemma 9.7 is now sorry-free.

That's great!

[Filippo A. E. Nuccio]

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]

(It occurs in the proof of lemma lem98_int)

[Johan Commelin]

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

[Filippo A. E. Nuccio]

...hmm, let me update and build.

[Filippo A. E. Nuccio]

Yes, everything is fine now!

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Thanks again @Filippo A. E. Nuccio

[Filippo A. E. Nuccio]

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