Zulip Chat Archive

Stream: new members

Topic: Modules with no 6-torsion


view this post on Zulip 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), 6a=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

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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
}

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Christopher Hoskin (Jan 01 2021 at 22:15):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:16):

you need a type ascription on 6

view this post on Zulip Eric Wieser (Jan 01 2021 at 22:17):

(6 : R) I assume?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:23):

Oh, there is a missing simp lemma here

view this post on Zulip Christopher Hoskin (Jan 01 2021 at 22:23):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:24):

the problem is that the latter theorem doesn't exist

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:26):

you need subnosixtorsion.coe_smul

view this post on Zulip 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
}

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:26):

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

view this post on Zulip 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)

view this post on Zulip 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), 6a=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
}

view this post on Zulip Eric Wieser (Jan 01 2021 at 22:35):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 01 2021 at 22:57):

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

view this post on Zulip Eric Wieser (Jan 01 2021 at 22:58):

I think there ought to be a statement about is_scalar_tower there

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:59):

Why wouldn't it be general enough?

view this post on Zulip Mario Carneiro (Jan 01 2021 at 23:00):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 23:00):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 23:00):

so that it works on additive groups

view this post on Zulip 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'?

view this post on Zulip Eric Wieser (Jan 01 2021 at 23:09):

Or does that already exist?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 01 2021 at 23:37):

We have that type of thing for tensor_product and linear_map already

view this post on Zulip 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')

view this post on Zulip 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

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


Last updated: May 14 2021 at 00:42 UTC