# Zulip Chat Archive

## Stream: new members

### Topic: Modules with no 6-torsion

#### Christopher Hoskin (Jan 01 2021 at 21:40):

Hello,

I'm trying to define a class of objects with a number of properties, one of which is that they are modules with no 6-torsion (i.e 6•a=0 implies a=0). This is the definition I'm using:

```
import algebra.module
universes u v
variables (R : Type u) [comm_ring R]
class nosixtorsion (A : Type v) [add_comm_group A] extends semimodule R A :=
(no_6_torsion : ∀ (a : A), 6•a=0 → a=0)
```

(I've removed the other properties for clarity)

I'd like to be able to show that subobjects of this class also have the no 6-torsion property. Using the mathlib code for Lie sub-algebras as a guide, I've tried this:

```
namespace nosixtorsion
set_option old_structure_cmd true
variables (A : Type v) [add_comm_group A] [nosixtorsion R A]
structure subnosixtorsion extends submodule R A
attribute [nolint doc_blame] subnosixtorsion.to_submodule
instance : has_coe (subnosixtorsion R A) (set A) := ⟨subnosixtorsion.carrier⟩
instance : has_mem A (subnosixtorsion R A) := ⟨λ a A', a ∈ (A' : set A)⟩
instance subnosixtorsion_coe_submodule : has_coe (subnosixtorsion R A) (submodule R A) :=
⟨subnosixtorsion.to_submodule⟩
instance submodule_nosixtorsion (A' : subnosixtorsion R A) : nosixtorsion R A' :=
{
no_6_torsion :=
begin
introv h,
apply set_coe.ext,
no_6_torsion a h
end
}
end nosixtorsion
```

(again, the other properties have been removed for clarity). However, Lean describes `a`

and `h`

as unknown identifiers.

Despite staring at this all evening, I can't see how to complete the proof. Perhaps there is a better way of implementing the property of not having torsion?

Thanks,

Christopher

#### Mario Carneiro (Jan 01 2021 at 21:49):

You are calling `no_6_torsion`

as a tactic, which will give bad error messages. You need something like `exact no_6_torsion ...`

or `have := no_6_torsion ...`

#### Mario Carneiro (Jan 01 2021 at 21:50):

This gets closer, although there is an issue with your coercions that makes `h`

not directly suitable for the final `_`

:

```
begin
introv h,
apply set_coe.ext,
simpa using @no_6_torsion R _ A _ _ a _,
sorry
end
```

#### Eric Wieser (Jan 01 2021 at 22:00):

Is there a reason you need `subnosixtorsion`

, even though it has no members that are different from submodule?

#### Christopher Hoskin (Jan 01 2021 at 22:05):

@Eric Wieser - It's not needed for the purposes of this example. The following would illustrate my problem just as well:

```
instance submodule_nosixtorsion (A' : submodule R A) : nosixtorsion R A' :=
{
no_6_torsion :=
begin
introv h,
apply set_coe.ext,
simpa using @no_6_torsion R _ A _ _ a h,
end
}
```

#### Christopher Hoskin (Jan 01 2021 at 22:07):

@Mario Carneiro Thanks for your help - it seems that the elements of the carrier are subtypes - a structure with a value and a proposition.

#### Mario Carneiro (Jan 01 2021 at 22:09):

I noticed that. Perhaps you meant to use `\forall a \in A`

in `no_6_torsion`

instead of `\forall a : A`

?

#### Christopher Hoskin (Jan 01 2021 at 22:15):

Lean seems to assume `a`

is a natural number if I do that.

#### Mario Carneiro (Jan 01 2021 at 22:16):

you need a type ascription on `6`

#### Eric Wieser (Jan 01 2021 at 22:17):

`(6 : R)`

I assume?

#### Christopher Hoskin (Jan 01 2021 at 22:18):

Trying

```
class nosixtorsion (A : Type v) [add_comm_group A] extends semimodule R A :=
(no_6_torsion : ∀ a ∈ A, (6 :R)•a=0 → a=0)
```

`a`

is red underlined as `?m_1`

#### Mario Carneiro (Jan 01 2021 at 22:19):

Oh I see, this proof is about showing that a submodule is a nosixtorsion, so the coe is unavoidable. You should do something like what's done to prove that a submodule is a semimodule:

```
instance : semimodule R p :=
by refine {smul := (•), ..p.to_sub_mul_action.mul_action, ..};
{ intros, apply set_coe.ext, simp [smul_add, add_smul, mul_smul] }
```

The key step being `set_coe.ext`

#### Mario Carneiro (Jan 01 2021 at 22:23):

Oh, there is a missing simp lemma here

#### Christopher Hoskin (Jan 01 2021 at 22:23):

I'm wondering if I need to apply `set_coe.ext`

to `h`

somehow?

#### Mario Carneiro (Jan 01 2021 at 22:24):

yes, like this:

```
begin
introv h,
rw ← set_coe.ext_iff at h ⊢,
rw submodule.smul_coe at h,
end
```

#### Mario Carneiro (Jan 01 2021 at 22:24):

the problem is that the latter theorem doesn't exist

#### Mario Carneiro (Jan 01 2021 at 22:25):

actually I take it back, `submodule.coe_smul`

does exist but doesn't apply here because you have your own coe

#### Mario Carneiro (Jan 01 2021 at 22:26):

you need `subnosixtorsion.coe_smul`

#### Christopher Hoskin (Jan 01 2021 at 22:26):

This gets me a `goal accomplished!`

```
instance submodule_nosixtorsion (A' : submodule R A) : nosixtorsion R A' :=
{
no_6_torsion :=
begin
introv h,
rw ← set_coe.ext_iff at h,
simpa using @no_6_torsion R _ A _ _ a h,
end
}
```

#### Mario Carneiro (Jan 01 2021 at 22:26):

you have three new definitions just before this and no lemmas about it

#### Eric Wieser (Jan 01 2021 at 22:28):

Solved for your reduced version without the new `subsixmodule`

type:

```
import algebra.module
universes u v
variables (R : Type u) [comm_ring R]
class nosixtorsion (A : Type v) [add_comm_monoid A] extends semimodule R A :=
(no_6_torsion : ∀ (a : A), (6 : R)•a=0 → a=0)
instance submodule_nosixtorsion (A : Type v) [add_comm_monoid A]
[nosixtorsion R A] (A' : submodule R A) : nosixtorsion R A' :=
{ no_6_torsion := λ a h, set_coe.ext $ nosixtorsion.no_6_torsion ↑a (set_coe.ext_iff.mpr h)
```

#### Christopher Hoskin (Jan 01 2021 at 22:33):

Thank you very much both for your help. This also seems to work for me:

```
import algebra.module
universes u v
variables (R : Type u) [comm_ring R]
class nosixtorsion (A : Type v) [add_comm_group A] extends semimodule R A :=
(no_6_torsion : ∀ (a : A), 6•a=0 → a=0)
variables (A : Type v) [add_comm_group A] [nosixtorsion R A]
instance submodule_nosixtorsion (A' : submodule R A) : nosixtorsion R A' :=
{
no_6_torsion :=
begin
introv h,
rw ← set_coe.ext_iff at h,
simpa using @nosixtorsion.no_6_torsion R _ A _ _ a h,
end
}
```

#### Eric Wieser (Jan 01 2021 at 22:35):

The one line proof in my message above appears to work for your `subnosixtorsion`

structure too

#### Christopher Hoskin (Jan 01 2021 at 22:43):

@Eric Wieser - yes - the one line proof seems to require `(6 : R)`

instead of `6`

in the `nosixtorsion.no_6_torsion`

definition (which is fine).

Thank you again for your help.

#### Eric Wieser (Jan 01 2021 at 22:57):

I wonder if docs#submodule.semimodule is not general enough to work when 6 is nat...

#### Eric Wieser (Jan 01 2021 at 22:58):

I think there ought to be a statement about `is_scalar_tower`

there

#### Mario Carneiro (Jan 01 2021 at 22:59):

Why wouldn't it be general enough?

#### Mario Carneiro (Jan 01 2021 at 23:00):

you can coerce nat to R and use `\u 6`

in any case

#### Mario Carneiro (Jan 01 2021 at 23:00):

although you might also want to use `gsmul`

for a concrete multiple like 6

#### Mario Carneiro (Jan 01 2021 at 23:00):

so that it works on additive groups

#### Eric Wieser (Jan 01 2021 at 23:09):

Couldn't there be an instance `(A' : submodule R A) [is_scalar_tower S R A'] : semimodule S A'`

?

#### Eric Wieser (Jan 01 2021 at 23:09):

Or does that already exist?

#### Mario Carneiro (Jan 01 2021 at 23:29):

that kind of thing looks scary to me, I wouldn't want to do it without a pressing need

#### Eric Wieser (Jan 01 2021 at 23:37):

We have that type of thing for tensor_product and linear_map already

#### Eric Wieser (Jan 01 2021 at 23:39):

Where we avoid nasty typeclass problems in the former by providing a fast path for the 99% case (src#tensor_product.semimodule vs src#tensor_product.semimodule')

#### Eric Wieser (Jan 02 2021 at 11:31):

Mario Carneiro said:

that kind of thing looks scary to me, I wouldn't want to do it without a pressing need

I've made a PR at #5569 to find out exactly how scary this is

#### Eric Wieser (Jan 02 2021 at 11:35):

Christopher Hoskin said:

Eric Wieser - yes - the one line proof seems to require

`(6 : R)`

instead of`6`

in the`nosixtorsion.no_6_torsion`

definition (which is fine).

The one-line proof appears to work fine if you replace `nosixtorsion.no_6_torsion`

with `nosixtorsion.no_6_torsion R`

(since the lemma can no longer deduce`R`

from the theorem statement if it's not the type of `6`

)

Last updated: May 14 2021 at 00:42 UTC