# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: torsion free

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

#### Adam Topaz (Feb 24 2021 at 15:28):

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

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

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

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

#### Adam Topaz (Feb 24 2021 at 15:34):

Oh, I just noticed that `is_regular`

is defined for anything with `has_mul`

:rofl:

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

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

#### 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)
```

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

#### Johan Commelin (Feb 24 2021 at 18:37):

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

#### Adam Topaz (Feb 24 2021 at 19:00):

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

#### 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!

#### Adam Topaz (Feb 24 2021 at 19:00):

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

#### Damiano Testa (Feb 24 2021 at 19:01):

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

#### Adam Topaz (Feb 24 2021 at 19:01):

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

#### Adam Topaz (Feb 24 2021 at 19:03):

Oh, but `domain`

extends `ring`

in mathlib.

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

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

#### Yakov Pechersky (Feb 24 2021 at 20:25):

I learned recently that `lt.ne'`

is the same as `lt.ne.symm`

.

#### Damiano Testa (Feb 24 2021 at 20:32):

Thanks for the characters' saving tip!

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

?

#### Johan Commelin (Feb 24 2021 at 20:41):

@Damiano Testa I like that name! Sounds good

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

#### Damiano Testa (Feb 25 2021 at 03:27):

PR #6408

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

#### Adam Topaz (Feb 25 2021 at 04:17):

Sounds good to me!

#### Adam Topaz (Feb 25 2021 at 04:17):

How generally are natural-number powers defined in mathlib?

#### Adam Topaz (Feb 25 2021 at 04:17):

We can go as general as that...

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

#### Adam Topaz (Feb 25 2021 at 04:18):

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

#### Johan Commelin (Feb 25 2021 at 04:22):

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

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

#### Damiano Testa (Feb 25 2021 at 05:32):

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

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

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

#### Johan Commelin (Feb 25 2021 at 08:35):

Is there a strong need for `pnat`

powers?

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

#### Kevin Buzzard (Feb 25 2021 at 08:37):

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

#### Kevin Buzzard (Feb 25 2021 at 08:37):

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

#### 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 `pnat`

and I am glad that Kevin confirms that it is missing some functionality!

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

#### Kevin Buzzard (Feb 25 2021 at 08:59):

I think `Sort`

needs to be replaced by `Sort*`

#### Kevin Buzzard (Feb 25 2021 at 09:00):

I think `Sort = Prop`

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

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

#### Kevin Buzzard (Feb 25 2021 at 09:05):

But your eliminator problems might just be the Sort issue

#### Kevin Buzzard (Feb 25 2021 at 09:49):

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

#### Kevin Buzzard (Feb 25 2021 at 09:52):

Your `lemma`

should be a `def`

#### Damiano Testa (Feb 25 2021 at 10:06):

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

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

#### Damiano Testa (Feb 25 2021 at 10:24):

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

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

#### Kevin Buzzard (Feb 25 2021 at 10:26):

This could be fixed by redefining `pnat`

to be `nat`

.

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

#### 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!

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

.

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

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

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

#### Mario Carneiro (Feb 25 2021 at 10:52):

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

#### Damiano Testa (Feb 25 2021 at 10:56):

Very nice, Mario! Thank you!

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

#### Mario Carneiro (Feb 25 2021 at 10:57):

Unfortunately as you can see they aren't both refl

#### Mario Carneiro (Feb 25 2021 at 10:57):

because `pnat`

isn't actually an inductive type

#### 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!

#### Damiano Testa (Feb 25 2021 at 11:24):

PR #6410 : Mario's induction for `pnat`

!

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

.

#### 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!

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

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

.

#### Mario Carneiro (Feb 25 2021 at 12:07):

unlikely, that shouldn't make much difference

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

#### 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!

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

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

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

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

#### Mario Carneiro (Feb 25 2021 at 13:23):

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

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

.

#### Eric Wieser (Feb 25 2021 at 20:54):

The equation compiler almost proves them for you

#### Eric Wieser (Feb 25 2021 at 20:57):

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

#### Eric Wieser (Feb 25 2021 at 20:58):

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

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

#### Filippo A. E. Nuccio (Mar 09 2021 at 22:23):

I have just pushed a loooong proof that the direct sum of `polyhedral_lattice`

s is torsion free, to remove one `sorry`

from the `instance : polyhedral_lattice (⨁ i, Λ i)`

of `polyhedral_lattice.basic`

. But something strange happens : when adding`import 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 (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

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

#### Filippo A. E. Nuccio (Mar 10 2021 at 08:35):

On the other hand, the `sorry`

s on lines 156, 158, 164 were already there.

#### Johan Commelin (Mar 10 2021 at 08:37):

@Filippo A. E. Nuccio what do you think, is `torsion_free`

working well?

#### 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)
```

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

#### Johan Commelin (Mar 10 2021 at 08:38):

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

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

#### 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 $\mathbb{Z}$

#### 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?

#### 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"

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

#### Filippo A. E. Nuccio (Mar 10 2021 at 08:42):

So far, the definition looked good to me

#### 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,
```

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

Ok, thanks. I'll improve it. But do you understand the problem with `import`

ing `direct_sum_module`

?

#### Damiano Testa (Mar 10 2021 at 08:56):

No, I have not looked into the `import`

issue.

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

'?

#### Johan Commelin (Mar 10 2021 at 09:29):

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

#### 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?

#### 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:

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

#### Eric Wieser (Mar 10 2021 at 09:33):

To bisect the problem; does importing `linear_algebra.dfinsupp`

instead break it too?

#### 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?

#### Johan Commelin (Mar 10 2021 at 09:33):

No, we have to do this ourselves

#### Johan Commelin (Mar 10 2021 at 09:33):

Damiano is building the machine to prove it

#### Johan Commelin (Mar 10 2021 at 09:34):

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

#### Johan Commelin (Mar 10 2021 at 09:34):

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

#### Johan Commelin (Mar 10 2021 at 09:34):

I get an error on some `rw`

#### Damiano Testa (Mar 10 2021 at 10:32):

I also get an error on a `rw`

further down the line.

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

#### 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!

#### 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?

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

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

#### 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?

#### 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:

#### 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)?

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

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

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