Zulip Chat Archive

Stream: condensed mathematics

Topic: torsion free


view this post on Zulip Johan Commelin (Feb 24 2021 at 15:27):

A little project: develop some API for torsion_free.
If we want to do this mathlib style, then we probably need:

Definitions:

  • torsion free modules module.torsion_free?
  • torsion free (additive) groups torsion_free/add_torsion_free?
  • (do we care about the noncommutative case?)

Glue:

  • glue between the two additive notions

API:

  • finite direct_sum of add_groups / modules
  • subgroups/submodules

view this post on Zulip Adam Topaz (Feb 24 2021 at 15:28):

What's the definition of torsion-free over rings with zero divisors?

view this post on Zulip Adam Topaz (Feb 24 2021 at 15:29):

I guess now that we have regular elements in mathlib (right?) we can say that the module has no torsion with respect to every regular element.

view this post on Zulip Johan Commelin (Feb 24 2021 at 15:31):

I think we can also choose to only develop the notion for modules. But when someone shows up and wants to apply it to a multiplicative group, we'll need to duplicate the API at that point.

view this post on Zulip Johan Commelin (Feb 24 2021 at 15:32):

Maybe that's even better, because then we can crystallize the API just in the module case, and afterwards the copy-pasta should be straightforward when we want to adapt it to groups.

view this post on Zulip Adam Topaz (Feb 24 2021 at 15:34):

Oh, I just noticed that is_regular is defined for anything with has_mul :rofl:

view this post on Zulip Damiano Testa (Feb 24 2021 at 16:04):

I am not sure whether the definition of is_regular already applies to modules, but if it does not apply "as is", it should really be defined by saying that a scalar r is regular for a module M should mean that smultiplication by r is injective.

view this post on Zulip Damiano Testa (Feb 24 2021 at 16:06):

For instance, I would say that 1 : \Z is regular on zmod 2, but 2 is not. I have not thought too much about the case in which the module is not faithful, though, so I am not sure whether down the line, you would like to avoid these cases...

view this post on Zulip Adam Topaz (Feb 24 2021 at 18:17):

So here's a definition that works in general:

import algebra.regular

variables (M X : Type*) [monoid M] [mul_action M X]

def torsion_free : Prop :=
   (m : M), is_regular m  function.injective (λ x : X, m  x)

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

But to get torsion-free groups out of this, we have to do some gymnastics:

-- is this somewhere?
instance foo (G : Type*) [group G] : mul_action  G :=
{ smul := λ x y, y^x,
  one_smul := λ b, by simp,
  mul_smul := λ a b c, pow_mul' _ _ _ }

lemma nat.pos_regular (m : ) : 0 < m  is_regular m :=
begin
  intro h,
  split,
  { intros a b hh,
    rwa nat.mul_right_inj h at hh },
  { intros a b hh,
    rwa nat.mul_left_inj h at hh }
end

lemma nat.succ_regular (m : ) : is_regular (m+1) := nat.pos_regular (m+1) $ nat.succ_pos _

example (G : Type*) [group G] (cond : torsion_free  G) :
   (n : ) (x : G), 0 < n  x^n = 1  x = 1 :=
begin
  intros n x hn h,
  induction n with m hm, {finish},
  rw (show 1 = (1 : G)^(m+1), by simp) at h,
  refine cond (m+1) (nat.succ_regular _) h,
end

view this post on Zulip Johan Commelin (Feb 24 2021 at 18:37):

But for torsion-free add_groups the gymnastics should be less convoluted, right?

view this post on Zulip Adam Topaz (Feb 24 2021 at 19:00):

yeah, those should have an automatic instance of a mul-action by Z\mathbb{Z}.

view this post on Zulip Damiano Testa (Feb 24 2021 at 19:00):

In the regular file there should be a lemma about nonzero elements of integral domains being regular. I think that, with Eric's refactor, N should be an integral domain... maybe!

view this post on Zulip Adam Topaz (Feb 24 2021 at 19:00):

Or is N\mathbb{N} an integral semidomain?

view this post on Zulip Damiano Testa (Feb 24 2021 at 19:01):

Maybe: I'm not at my computer and cannot check...

view this post on Zulip Adam Topaz (Feb 24 2021 at 19:01):

(that was a joke :smile: I really hope no one defines a semidomain)

view this post on Zulip Adam Topaz (Feb 24 2021 at 19:03):

Oh, but domain extends ring in mathlib.

view this post on Zulip Damiano Testa (Feb 24 2021 at 19:03):

Certainly, an N is commutative, there is a lemma that allows you to only prove left regular.

view this post on Zulip Damiano Testa (Feb 24 2021 at 20:20):

Actually, this works:

lemma nat.pos_regular (m : ) : 0 < m  is_regular m :=
λ h, is_regular_of_cancel_monoid_with_zero h.ne.symm

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 20:25):

I learned recently that lt.ne' is the same as lt.ne.symm.

view this post on Zulip Damiano Testa (Feb 24 2021 at 20:32):

Thanks for the characters' saving tip!

view this post on Zulip Damiano Testa (Feb 24 2021 at 20:34):

Maybe a better name for is_regular_of_cancel_monoid_with_zero would be is_regular_of_ne_zero?

view this post on Zulip Johan Commelin (Feb 24 2021 at 20:41):

@Damiano Testa I like that name! Sounds good

view this post on Zulip Damiano Testa (Feb 24 2021 at 20:48):

I'll PR it tomorrow, but feel free to change it now, if you want! I'm pretty sure no one has used the lemma yet

view this post on Zulip Damiano Testa (Feb 25 2021 at 03:27):

PR #6408

view this post on Zulip Damiano Testa (Feb 25 2021 at 04:00):

Adam, the instance mul_action works, with the same proof, for a monoid. Given an earlier discussion, maybe we should also have an instance of mul_action pnat G, for any semigroup G! :smile:

-- is this somewhere?
instance foo (G : Type*) [group G] : mul_action  G :=
{ smul := λ x y, y^x,
  one_smul := λ b, by simp,
  mul_smul := λ a b c, pow_mul' _ _ _ }

view this post on Zulip Adam Topaz (Feb 25 2021 at 04:17):

Sounds good to me!

view this post on Zulip Adam Topaz (Feb 25 2021 at 04:17):

How generally are natural-number powers defined in mathlib?

view this post on Zulip Adam Topaz (Feb 25 2021 at 04:17):

We can go as general as that...

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

I don't know how easy it would be to make the to_additive machine work there...

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

(if it can be made to work at all!)

view this post on Zulip Johan Commelin (Feb 25 2021 at 04:22):

yeah, the trouble is that we are switch the sides of the action

view this post on Zulip Damiano Testa (Feb 25 2021 at 05:31):

Regardless of whether we use it or not, I decided to give a try to defining pnat powers, but I seem to be lacking good techniques to work with them: can you suggest a better proof?

instance power {G : Type*} [semigroup G] : has_pow G pnat :=
{ pow := begin
  intros g n,
  induction n with n n0,
  generalize' hn : n.pred = np,
  have n1 : n = n.pred.succ := (nat.succ_pred_eq_of_pos n0).symm,
  rw hn at n1,
  subst n1,
  induction np with np hnp,
  { exact g },
  { exact (hnp np.succ_pos np.pred_succ) * g }
end }

view this post on Zulip Damiano Testa (Feb 25 2021 at 05:32):

In particular, I could not find a suitable "pnat induction" lemma in the library.

view this post on Zulip Damiano Testa (Feb 25 2021 at 05:34):

Moreover, to then make it work, it seems that it should be proven for {n // 0 < n} as well as for pnat.

variables {G : Type*} [semigroup G] {g : G} {n : pnat} {m : } {hm : 0 < m}
#check g ^ n --works
#check (⟨m, hm : pnat) --works
#check g ^ (⟨m, hm : pnat)
-- fails: `failed to synthesize type class instance for [...] ⊢ has_pow G {n // 0 < n}`

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 08:35):

I'm not sure that going as far down as semigroups is necessary, however this might just be because everyone is always happy to stop at monoids. Damiano -- nobody uses pnat so it doesn't surprise me that you can't find induction. Just define pnat.rec_on and make a PR, and then apply it instead. Don't forget to tag it elab_as_eliminator so that lean has a better chance of figuring out the so-called "motive" C. Maybe experimenting with semigroups will be a good excuse to make pnat great again

view this post on Zulip Johan Commelin (Feb 25 2021 at 08:35):

Is there a strong need for pnat powers?

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 08:37):

You'll have problems making an API for your current definition because you've made it in tactic mode. Try #print ing it to see what kind of a monster it is

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 08:37):

Not really, I don't see any harm in sticking to monoids

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 08:37):

The issue is that with a semigroup you don't have g^0

view this post on Zulip Damiano Testa (Feb 25 2021 at 08:48):

I have no application in mind that would want an action of a semigroup instead of a monoid: in most situations that I can imagine, there is very little difficulty in extending a semigroup to a monoid by adding a "natural" identity. Thus, for the moment, I would not go further down this road. The above was mostly an experiment to work with pnatand I am glad that Kevin confirms that it is missing some functionality!

view this post on Zulip Damiano Testa (Feb 25 2021 at 08:51):

Besides, I am failing to produce an element of G by induction.

@[elab_as_eliminator]
lemma pnat.rec_on (n : pnat) {p : pnat  Sort} (p1 : p 1) (hp :  n, p n  p (n + 1)) : p n :=
begin
  cases n with n n0,
  generalize' hn : n.pred = np,
  have n1 : n = n.pred.succ := (nat.succ_pred_eq_of_pos n0).symm,
  rw hn at n1,
  subst n1,
  induction np with np hnp,
  { exact p1 },
  { exact hp _, np.succ_pos (hnp _ np.pred_succ) }
end

instance power_Np {G : Type*} [semigroup G] : has_pow G {n // 0 < n} :=
{ pow := begin
  intros g n,
  apply pnat.rec_on n _ _,
-- fails saying

invalid 'pnat.rec_on' application, elaborator has special support for this kind of application
(it is handled as an "eliminator"), but the expected type must be known
state:
G : Type ?,
_inst_1 : semigroup G,
g : G,
n : {n // 0 < n}
 G
end }

Using refine instead of apply gives:

instance power_Np {G : Type*} [semigroup G] : has_pow G {n // 0 < n} :=
{ pow := begin
  intros g n,
  refine pnat.rec_on n _ _,
-- fails saying

"eliminator" elaborator failed to compute the motive
state:
G : Type ?,
_inst_1 : semigroup G,
g : G,
n : {n // 0 < n}
 G

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 08:59):

I think Sort needs to be replaced by Sort*

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 09:00):

I think Sort = Prop

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 09:02):

And my gut feeling is that the subst command is inserting an eq.rec which might be tough to prove things about. I'm stuck away from Lean right now but I would be tempted to write this in term mode using nat.rec and trying to avoid a further eq.rec

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 09:04):

Presumably there's pnat.pred to nat and a map the other way too and it's just a case of composing these with nat.rec

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

But your eliminator problems might just be the Sort issue

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 09:49):

OK I'm at a PC, I'll give this pnat thing a go

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 09:52):

Your lemma should be a def

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:06):

I was talking to a student, so I am now reading your comments!

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 10:23):

example (n : +) : n.nat_pred.succ_pnat = n := rfl -- fails :-(

This is the problem. Maybe you need the eq.rec to get over this.

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:24):

I am also having a hard time working with this...

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:25):

the subst command was there, since I could not even rw it in the goal (which I understand I should avoid anyway, but there was already something that I found strange)

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 10:26):

This could be fixed by redefining pnat to be nat.

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:27):

I would like that. In fact, I would like to define a nat depending on a nat to stand for the "naturals at least equal to _"!

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:30):

With the Sort*, the induction applied to the definition of has_pow and it was easy:

instance power_Np {G : Type*} [semigroup G] : has_pow G {n // 0 < n} :=
{ pow := λ g n, ((pnat.rec_on n id (λ m pm1 g, (pm1 g) * g)) g) }

However, as you predicted, the lemma

lemma pow_one {G : Type*} [semigroup G] (g : G) :
  g ^ (⟨1, nat.one_pos : pnat) = g :=

went from being rfl to being not soluble by me!

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:34):

I think that I will give up: I am not sure how to make progress on this, and I am also not in need for defining induction or powers using pnat.

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 10:46):

I need to stop because I am teaching in 5 hours and I've still not started on my blog post or pushed any material. Because the proof of foo below is not rfl, one has to use eq.subst (whose proof is just eq.rec) to push through this approach:

import data.pnat.basic

open nat

-- example (n : ℕ+) : n.nat_pred.succ_pnat = n := rfl -- fails :-(

lemma foo (n : +) : n.nat_pred.succ_pnat = n := begin
  cases n with m hm,
  ext,
  cases m,
    cases hm,
  refl,
end

-- now `eq.subst (foo n) : p (n.nat_pred.succ_pnat) → p n

@[elab_as_eliminator]
def pnat.rec_on (n : pnat) {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) : p n :=
eq.subst (foo n) (@nat.rec (λ m, p (succ_pnat m)) p1
  (λ m (pm : p (succ_pnat m)), (hp (succ_pnat m) pm : p (succ_pnat (m + 1)))) n.nat_pred)

The crucial thing about nat.rec is that if you have C0 : C 0 and Csucc n : C n -> C (n + 1) and you define your function f with nat.rec, then f 0 = c0 and f (n + 1) = Csucc n (f n) are both rfl. The eq.subst will mess all this up though. I think the way to proceed is not as above but instead to use nat.rec on n.1. I'll try this later on but right now I need to focus on my class.

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 10:49):

Some smart people have looked at pnat and the fact that nobody has defined pnat.rec is telling. There's the induction principle but this has fewer problems because Prop is easier to handle than Type.

view this post on Zulip Mario Carneiro (Feb 25 2021 at 10:51):

Here's a proof using nat.rec:

@[elab_as_eliminator]
def pnat.rec_on (n : pnat) {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) : p n :=
begin
  rcases n with n, h⟩,
  induction n with n IH,
  { exact absurd h dec_trivial },
  { cases n with n,
    { exact p1 },
    { exact hp _ (IH n.succ_pos) } }
end

view this post on Zulip Mario Carneiro (Feb 25 2021 at 10:52):

(I can use tactics because I'm a professional :grinning: )

view this post on Zulip Damiano Testa (Feb 25 2021 at 10:56):

Very nice, Mario! Thank you!

view this post on Zulip Mario Carneiro (Feb 25 2021 at 10:57):

also don't forget the equation lemmas:

theorem pnat.rec_on_one (n : pnat) {p} (p1 hp) : @pnat.rec_on 1 p p1 hp = p1 := rfl
theorem pnat.rec_on_succ (n : pnat) {p : pnat  Sort*} (p1 hp) :
  @pnat.rec_on (n + 1) p p1 hp = hp n (@pnat.rec_on n p p1 hp) :=
by { cases n with n h, cases n; [exact absurd h dec_trivial, refl] }

view this post on Zulip Mario Carneiro (Feb 25 2021 at 10:57):

Unfortunately as you can see they aren't both refl

view this post on Zulip Mario Carneiro (Feb 25 2021 at 10:57):

because pnat isn't actually an inductive type

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 11:14):

@Damiano Testa it doesn't matter if the proofs aren't refl -- what matters is that the proofs exist!

view this post on Zulip Damiano Testa (Feb 25 2021 at 11:24):

PR #6410 : Mario's induction for pnat!

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 11:39):

Note that Mario's proof did indeed do induction on n : nat rather than n.nat_pred.

view this post on Zulip Damiano Testa (Feb 25 2021 at 11:41):

Yes, I thought that working with a natural number was better than working with an absurd induction step and then splitting cases, but I was wrong!

view this post on Zulip Damiano Testa (Feb 25 2021 at 11:42):

This now works:

instance power_Np {G : Type*} [semigroup G] : has_pow G {n // 0 < n} :=
{ pow := λ g n, begin
  revert g,
  refine pnat.rec_on n _ _,
  { exact id },
  { exact λ n pm1 g, (pm1 g) * g }
end
}

lemma action_one {G : Type*} [semigroup G] (g : G) :
  g ^ (⟨1, nat.one_pos : pnat) = g := rfl

lemma action_succ {G : Type*} [semigroup G] (g : G) (n : ) :
  g ^ (⟨n + 2, (n + 1).succ_pos : pnat) = g ^ (⟨n + 1, n.succ_pos : pnat) * g := rfl

view this post on Zulip Damiano Testa (Feb 25 2021 at 11:46):

However, Lean almost immediately complains about excessive memory consumption. This might be a consequence of having the lemma in the liquid project and not on the separate file data/pnat/basic.

view this post on Zulip Mario Carneiro (Feb 25 2021 at 12:07):

unlikely, that shouldn't make much difference

view this post on Zulip Mario Carneiro (Feb 25 2021 at 12:08):

If you modified a basic file and then went back to the liquid project then lean might be going crazy compiling mathlib in the editor

view this post on Zulip Damiano Testa (Feb 25 2021 at 12:09):

Ok, I closed all tabs other than the one where I am working (which at the moment does not even depend on the pnat thing) and I hope that there will no longer be memory issues!

view this post on Zulip Eric Wieser (Feb 25 2021 at 12:42):

Mario Carneiro said:

(I can use tactics because I'm a professional :grinning: )

Is it a good idea to use the equation compiler instead?

@[recursor]
def pnat.rec {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) :  n, p n
| 0, h := (rfl.le.not_lt h).elim
| 1, h := p1
| n + 2, h := hp _ (pnat.rec n + 1, n.succ_pos⟩)

@[elab_as_eliminator]
def pnat.rec_on (n : pnat) {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) : p n :=
pnat.rec p1 hp n

view this post on Zulip Mario Carneiro (Feb 25 2021 at 13:18):

The term you get is a bit messier, but how much this matters depends on the context. That proof there is actually using well founded recursion, so it won't compute very well

view this post on Zulip Mario Carneiro (Feb 25 2021 at 13:19):

you can get it to at least use bounded recursion if you do the initial cases on pnat separate from the main recursion

view this post on Zulip Mario Carneiro (Feb 25 2021 at 13:22):

def pnat.rec_aux {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) :  n h, p n, h
| 0 h := (rfl.le.not_lt h).elim
| 1 h := p1
| (n + 2) h := hp _ (pnat.rec_aux (n + 1) n.succ_pos)

@[recursor]
def pnat.rec {p : pnat  Sort*} (p1 : p 1) (hp :  n, p n  p (n + 1)) :  n, p n
| n, h := pnat.rec_aux p1 hp n h

view this post on Zulip Mario Carneiro (Feb 25 2021 at 13:23):

Using tactics here makes it easier to control the exact recursion structure

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 20:53):

@Eric Wieser I should think the proof of the pudding will be whether you can prove rec_on_one and rec_on_succ.

view this post on Zulip Eric Wieser (Feb 25 2021 at 20:54):

The equation compiler almost proves them for you

view this post on Zulip Eric Wieser (Feb 25 2021 at 20:57):

At least, it emits proofs of type defeq to the ones we care about

view this post on Zulip Eric Wieser (Feb 25 2021 at 20:58):

But Mario's right about it producing an undesirably long term

view this post on Zulip Damiano Testa (Feb 27 2021 at 16:27):

I want to revive the torsion free part of this thread.

While experimenting with the toric branch, it seems that assuming is_basis is a very good substitute for torsion free.

While this may not be a very robust or general approach, working with modules admitting a basis is actually not such a mathematically weird idea. Of course, you would not be able to apply these statements about the rationals viewed as a module of the integers (or the naturals!), but maybe this is not what we need...

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 22:23):

I have just pushed a loooong proof that the direct sum of polyhedral_lattices is torsion free, to remove one sorry from the instance : polyhedral_lattice (⨁ i, Λ i) of polyhedral_lattice.basic. But something strange happens : when addingimport linear_algebra.direct_sum_module at the beginning of the file, the code breaks on line 167 (this has nothing to do with my proof). I can't understand where this comes from, so I left my proof commented (and replaced it with a sorry), hoping that someone can fix the problem.

view this post on Zulip Eric Wieser (Mar 10 2021 at 01:49):

It fails on the end of the namespace? https://github.com/leanprover-community/lean-liquid/blob/6de12c8fa1eefa02db4ada2babd5bbf06785de44/src/polyhedral_lattice/basic.lean#L167

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:26):

Yes, the rw [hl, finset.smul_sum, ← finset.univ_sigma_univ, finset.sum_sigma], on line 159 compiles well if import linear_algebra.direct_sum_module is not called, but when adding import linear_algebra.direct_sum_module, it suddenly fails.

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:35):

On the other hand, the sorrys on lines 156, 158, 164 were already there.

view this post on Zulip Johan Commelin (Mar 10 2021 at 08:37):

@Filippo A. E. Nuccio what do you think, is torsion_free working well?

view this post on Zulip Johan Commelin (Mar 10 2021 at 08:38):

@Damiano Testa suggested that another way to say "finite free abelian group" is something like

\ex {\iota : Type} (v : \iota -> A) (is_basis int v)

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:38):

Well, I think it works pretty well. I was able without too much pain to prove that the direct sum of torsion-free modules is torsion-free, basically mimicking the "natural" proof

view this post on Zulip Johan Commelin (Mar 10 2021 at 08:38):

And I think @Anne Baanen was also experimenting with making this the definition of free

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:38):

Well, I have just worked with it yesterday, but I found the API pretty good.

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:39):

In particular, it seems perfectly well-suited for saying what being torsion (or not) is over very general basis other than Z\mathbb{Z}

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:40):

Johan Commelin said:

And I think Anne Baanen was also experimenting with making this the definition of free

But free and torsion_free are quite far apart, as notions, no?

view this post on Zulip Johan Commelin (Mar 10 2021 at 08:41):

@Filippo A. E. Nuccio Yes, but for polyhedral_lattice we want to say "finite free abelian group"

view this post on Zulip Johan Commelin (Mar 10 2021 at 08:41):

And in the end I don't care how we say it. So we should pick the version that is easiest to work with

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:42):

So far, the definition looked good to me

view this post on Zulip Damiano Testa (Mar 10 2021 at 08:52):

Filippo, I looked at your proof and I have a small streamlining of it. However, I also get the weird issues later on, so I am hesitant to push it anywhere! I leave it here, in case you find it useful.

  tf :=
  begin
    intros v hv n hnv,
    obtain i, nzv_i :  (i : ι), direct_sum.component  ι Λ i v  0,
    { rw  not_forall,
      rwa [ne.def, direct_sum.ext_iff ] at hv },
    have tf_i : torsion_free (Λ i),
    { suffices pl_i : polyhedral_lattice (Λ i),
      exact pl_i.tf,
      apply_assumption },
    refine tf_i (direct_sum.component  ι Λ i v) nzv_i n _,
    rw  linear_map.map_smul_of_tower,
    convert (direct_sum.ext_iff ).mp hnv i,
  end,

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 08:54):

Ok, thanks. I'll improve it. But do you understand the problem with importing direct_sum_module?

view this post on Zulip Damiano Testa (Mar 10 2021 at 08:56):

No, I have not looked into the import issue.

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 09:28):

@Johan Commelin May be you have an idea of this import issue? Also, what is your plan for this file polyhedral_lattice.basis, is it reasonable to continue working on this trying to "kill" some sorry'?

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:29):

@Filippo A. E. Nuccio I will take a look at the import issue now

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:30):

At some point you were thinking about 9.7, right? If we pin down some statement of Gordan's lemma, would you like to try proving Gordan => 9.7?

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 09:30):

Johan Commelin said:

At some point you were thinking about 9.7, right? If we pin down some statement of Gordan's lemma, would you like to try proving Gordan => 9.7?

I had just opened the file to look into this! :time:

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:31):

For polyhedral_lattice.basis, we first have to decide what is the best way for us to say "finite free abelian group". And I think the point where we want to use this most is in the proof of Gordan. So Damiano will have to tell us what he likes best (-;

view this post on Zulip Eric Wieser (Mar 10 2021 at 09:33):

To bisect the problem; does importing linear_algebra.dfinsupp instead break it too?

view this post on Zulip Filippo A. E. Nuccio (Mar 10 2021 at 09:33):

BTW: Is there already a formulation of Gordan's lemma in the library? Or is it coming with Damiano's work?

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:33):

No, we have to do this ourselves

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:33):

Damiano is building the machine to prove it

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:34):

@Filippo A. E. Nuccio shall we do a quick video call, to work out a sketch?

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:34):

Also, the import issue doesn't show up for me

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:34):

I get an error on some rw

view this post on Zulip Damiano Testa (Mar 10 2021 at 10:32):

I also get an error on a rw further down the line.

view this post on Zulip Damiano Testa (Mar 10 2021 at 10:32):

(my day today is littered with commitments ever once in a while, so my comments are scattered and I can only concentrate on small stuff!)

view this post on Zulip Damiano Testa (Mar 10 2021 at 15:01):

I tried looking at the import issue: I could not understand why it breaks, but was able to make it progress further, a simp step away from sorry where it stopped earlier. It is not pretty, but it seems to (partially) work and also incorporates a proof of fg. Let me know what you think!

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

What is the status here? Is this some issue with a broken proof or is the problem weirder?

view this post on Zulip Damiano Testa (Mar 11 2021 at 08:41):

I do not know what the problem is. When I looked at it, there were two relevant proofs:

  • a complete, commented out, proof, needing some import, also commented out; and
  • an incomplete proof further down that led, with no errors, to a sorry.

(If you look at the file, it might be easier to follow what I am saying.)

Adding the imports needed for the commented proof, made a rw step of the second proof no longer work. With a bad trick, I was able to push the now-broken proof a couple of steps further, just until the simp before its ending sorry.

I think that this is where the situation is right now.

view this post on Zulip Filippo A. E. Nuccio (Mar 11 2021 at 12:54):

Yes, indeed, this is the situation. It seems strange that adding an import breaks a rw proof, but may be this comes from more things having the same name? At any rate, after discussions with @Johan Commelin , it is now probably time to wait a little bit for this file as we're waiting for a PR about free modules on mathlib, which seems on its way to be merged.

view this post on Zulip Filippo A. E. Nuccio (Mar 11 2021 at 12:54):

On the other hand, @Damiano Testa I still don't find the fg proof, was it for the direct sum?

view this post on Zulip Damiano Testa (Mar 11 2021 at 15:10):

Oh, I might have said fg for tf: I simply golfed your proof, whichever one if was!! :upside_down:

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 11:41):

I didn't follow the discussion... to we have somewhere that free implies torsion free (yes, I mean the easy implication)?

view this post on Zulip Filippo A. E. Nuccio (Apr 01 2021 at 11:42):

I think we have it somewhere: I am going to look for it, but do you need for something else or for discussion we had with Damiano? Because the situation changed a bit and became slightly out of date.

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 11:45):

I am trying to prove pre_generators_finite. In any case if we want to play with lattices something like a • x = b • x → a = b (with x nonzero) seems very natural... and that is all what I need.

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 11:57):

We have docs#is_basis.no_zero_smul_divisors that is all I need.


Last updated: May 09 2021 at 16:20 UTC