is_torsion Fq[X]

Stream: maths

[Julian Berman]

Hello. Can I ask for advice on a good place to put:

import group_theory.torsion
open_locale polynomial
variables {Fq : Type*} [field Fq] [fintype Fq]
/-- Fq[X] is a torsion group -/
lemma is_torsion : add_monoid.is_torsion Fq[X] :=
λ f, begin
  rw is_of_fin_add_order_iff_nsmul_eq_zero,
  refine ⟨fintype.card Fq, fintype.card_pos, _⟩,
  rw [nsmul_eq_smul_cast Fq _ f, finite_field.cast_card_eq_zero, zero_smul],
end

Does putting it in field_theory.finite.polynomial make any sense?

[Alex J. Best]

It seems this really is a quite special case of something much more generally useful? That vector spaces over finite fields are torsion? Or maybe something more general still about modules over torsion abelian groups?

[Julian Berman]

Given how little I know I'm sure that's likely, so if you have a suggestion for which of those to go after I'm happy to do it instead.

[Alex J. Best]

Sure I'll have a go at extracting the weakest things for which your proof works :smile:

[Julian Berman]

Thanks! If you don't mind not spoiling the proof immediately that'd be appreciated as well.

[Alex J. Best]

What do you mean sorry? Like just tell you the answer but not the modifications to the proof?

[Julian Berman]

Yeah hah just that

[Alex J. Best]

Not sure if its optimal but the following refactoring seems more natural to me:

import group_theory.torsion
section
variables {Fq : Type*} [semiring Fq] (t : add_monoid.is_torsion Fq)
include t

lemma is_torsion (R : Type*) [add_comm_monoid R] [module Fq R] : add_monoid.is_torsion R :=
λ f, begin
  --proof left for the reader
end
end

section

variables {Fq : Type*} [ring Fq] [fintype Fq]

-- should prove the original goal
lemma is_torsion' (R : Type*) [add_comm_monoid R] [module Fq R] : add_monoid.is_torsion R :=
is_torsion (is_add_torsion_of_fintype : add_monoid.is_torsion Fq) R

end

[Reid Barton]

What does it mean for a monoid to be torsion? Is it a group?

[Alex J. Best]

Yeah I guess the real assumptions for the first part are closer to the second! And we may as well assume group / ring throughout

[Reid Barton]

The documentation in group_theory.torsion and group_theory.order_of_element is a bit confusing, it talks as though "group" and "monoid" are interchangeable.

[Eric Rodriguez]

I feel like this is also done in file#group_theory.exponent, but just because people rarely talk about exponent of groups. I guess that all torsion monoids are groups, though...

[Julian Berman]

Yeah. I think other-Julian was explaining that to me (that elsewhere it's an implementation detail that things are defined on monoid) but that here things are always groups anyhow. But I may have still poorly written the docstring, maybe I should just have used group everywhere in it

[Eric Rodriguez]

maybe just put it in the impl details section

[Eric Rodriguez]

cc @Julian Külshammer

[Alex J. Best]

  have : is_of_fin_add_order (1 : Fq) := t 1,
  rw is_of_fin_add_order_iff_nsmul_eq_zero at this ⊢,
  rcases this with ⟨w, h_w, h_h⟩,
  refine ⟨w, h_w, _⟩,
  rw [nsmul_eq_smul_cast Fq _ f],
  convert zero_smul _ _,
  rwa [nat.smul_one_eq_coe] at h_h,

[Eric Rodriguez]

here's a proof that I can't be asked to PR but is probably worth having:

@[to_additive]
noncomputable def is_torsion.group [monoid G] [h : is_torsion G] : group G :=
{ inv := λ g, g ^ (order_of g - 1),
  mul_left_inv := λ g,
  begin
    erw [←pow_succ', tsub_add_cancel_of_le, pow_order_of_eq_one],
    exact order_of_pos' (h g)
  end,
  ..‹monoid G› }

[Reid Barton]

btw what are the technical reasons for making is_torsion a property of monoids in the first place?

[Julian Berman]

I copied where to put it from order_of_element, so there may not be any good one other than my cargo culting. If I move it to group and everything works is that all that would need checking?

It would however lose the ability to state Eric's proof above though right (#12432, thanks Eric)?

[Kevin Buzzard]

Reid Barton said:

btw what are the technical reasons for making is_torsion a property of monoids in the first place?

My money's on "because it compiles" :-/

[Kevin Buzzard]

and you can have the added benefit of being able to promote a torsion monoid to a group thus enabling some exciting diamonds.

[Eric Wieser]

Arguably it's good that it's defined on monoids because it means we can state and prove "you may as well have just used a group" rather than just asserting it in a docstring

[Yaël Dillies]

Note that in the convexity API people made me change [ordered_ring 𝕜] [add_comm_monoid E] [module 𝕜 E] to [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E]

[Reid Barton]

Eric Wieser said:

Arguably it's good that it's defined on monoids because it means we can state and prove "you may as well have just used a group" rather than just asserting it in a docstring

But... you could have just used a group, so why does it matter?

[Reid Barton]

I fail to see a motivation here--I'm not saying there can't be one, I just don't know. But, if we do leave is_torsion as a property of a monoid, we should make very clear in the documentation that a "torsion monoid" is just a torsion group.

[Reid Barton]

Because for a mathematician "torsion monoid" doesn't make sense as a name for a structure in which every element $x$ satisfies $x^n = 1$ for some $n$, because we already have a name for that--torsion group.

[Mario Carneiro]

In lean there is a difference: a group comes with an inverse operation and a torsion monoid doesn't

[Mario Carneiro]

You can construct an inverse operation but it doesn't have one built in

[Mario Carneiro]

By the same argument you can ask why a group has a 1 and inverse in the first place since the multiplication uniquely defines the rest of it

[Kevin Buzzard]

Right, so you're agreeing that this should be a predicate on groups, because we should have the inverse rather than having to infer it?

[Mario Carneiro]

well if you want a torsion group then you can say [group A] [is_torsion A] but it seems like torsion monoid is a well formed concept