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, ..};


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

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

Last updated: May 14 2021 at 00:42 UTC