Modules with no 6-torsion

Stream: new members

[Christopher Hoskin]

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]

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]

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]

Is there a reason you need subnosixtorsion, even though it has no members that are different from submodule?

[Christopher Hoskin]

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

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

I noticed that. Perhaps you meant to use \forall a \in A in no_6_torsion instead of \forall a : A?

[Christopher Hoskin]

Lean seems to assume a is a natural number if I do that.

[Mario Carneiro]

you need a type ascription on 6

[Eric Wieser]

(6 : R) I assume?

[Christopher Hoskin]

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]

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]

Oh, there is a missing simp lemma here

[Christopher Hoskin]

I'm wondering if I need to apply set_coe.ext to h somehow?

[Mario Carneiro]

yes, like this:

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

[Mario Carneiro]

the problem is that the latter theorem doesn't exist

[Mario Carneiro]

actually I take it back, submodule.coe_smul does exist but doesn't apply here because you have your own coe

[Mario Carneiro]

you need subnosixtorsion.coe_smul

[Christopher Hoskin]

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]

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

[Eric Wieser]

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]

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]

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

[Christopher Hoskin]

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

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

[Eric Wieser]

I think there ought to be a statement about is_scalar_tower there

[Mario Carneiro]

Why wouldn't it be general enough?

[Mario Carneiro]

you can coerce nat to R and use \u 6 in any case

[Mario Carneiro]

although you might also want to use gsmul for a concrete multiple like 6

[Mario Carneiro]

so that it works on additive groups

[Eric Wieser]

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

[Eric Wieser]

Or does that already exist?

[Mario Carneiro]

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

[Eric Wieser]

We have that type of thing for tensor_product and linear_map already

[Eric Wieser]

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]

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]

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 deduceR from the theorem statement if it's not the type of 6)