torsion free

Stream: condensed mathematics

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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.

[Johan Commelin]

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.

[Johan Commelin]

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.

[Adam Topaz]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Adam Topaz]

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)

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Damiano Testa]

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!

[Adam Topaz]

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

[Damiano Testa]

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

[Adam Topaz]

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

[Adam Topaz]

Oh, but domain extends ring in mathlib.

[Damiano Testa]

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

[Damiano Testa]

Actually, this works:

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

[Yakov Pechersky]

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

[Damiano Testa]

Thanks for the characters' saving tip!

[Damiano Testa]

Maybe a better name for is_regular_of_cancel_monoid_with_zero would be is_regular_of_ne_zero?

[Johan Commelin]

@Damiano Testa I like that name! Sounds good

[Damiano Testa]

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

[Damiano Testa]

PR #6408

[Damiano Testa]

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' _ _ _ }

[Adam Topaz]

Sounds good to me!

[Adam Topaz]

How generally are natural-number powers defined in mathlib?

[Adam Topaz]

We can go as general as that...

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Damiano Testa]

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 }

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Johan Commelin]

Is there a strong need for pnat powers?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Kevin Buzzard]

I think Sort needs to be replaced by Sort*

[Kevin Buzzard]

I think Sort = Prop

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

But your eliminator problems might just be the Sort issue

[Kevin Buzzard]

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

[Kevin Buzzard]

Your lemma should be a def

[Damiano Testa]

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

[Kevin Buzzard]

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

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

[Damiano Testa]

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

[Damiano Testa]

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)

[Kevin Buzzard]

This could be fixed by redefining pnat to be nat.

[Damiano Testa]

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 _"!

[Damiano Testa]

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!

[Damiano Testa]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

Very nice, Mario! Thank you!

[Mario Carneiro]

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

[Mario Carneiro]

Unfortunately as you can see they aren't both refl

[Mario Carneiro]

because pnat isn't actually an inductive type

[Kevin Buzzard]

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

[Damiano Testa]

PR #6410 : Mario's induction for pnat!

[Kevin Buzzard]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Damiano Testa]

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.

[Mario Carneiro]

unlikely, that shouldn't make much difference

[Mario Carneiro]

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

[Damiano Testa]

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!

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Eric Wieser]

The equation compiler almost proves them for you

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Filippo A. E. Nuccio]

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.

[Eric Wieser]

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

[Filippo A. E. Nuccio]

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.

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

So far, the definition looked good to me

[Damiano Testa]

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,

[Filippo A. E. Nuccio]

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

[Damiano Testa]

No, I have not looked into the import issue.

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Filippo A. E. Nuccio]

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:

[Johan Commelin]

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

[Eric Wieser]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

No, we have to do this ourselves

[Johan Commelin]

Damiano is building the machine to prove it

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I get an error on some rw

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Damiano Testa]

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.

[Filippo A. E. Nuccio]

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.

[Filippo A. E. Nuccio]

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

[Damiano Testa]

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

[Riccardo Brasca]

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

[Filippo A. E. Nuccio]

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.

[Riccardo Brasca]

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.

[Riccardo Brasca]

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