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

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 pnatand 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_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 (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 sorrys 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 importing 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