New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(group_theory/torsion): Q/Z and Fq[X] are torsion groups #12310
Conversation
431ab2e
to
f24e7a5
Compare
f24e7a5
to
04bf48f
Compare
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
/-- The group ℚ ⧸ ℤ. -/ | ||
@[reducible] def qmodz := ℚ ⧸ (algebra.linear_map ℤ ℚ).range | ||
|
||
namespace qmodz | ||
|
||
open rat | ||
|
||
/-- ℚ ⧸ ℤ is a torsion group -/ | ||
lemma is_torsion : add_monoid.is_torsion qmodz := | ||
λ q, begin | ||
induction q using quotient.induction_on', | ||
simp_rw [is_of_fin_add_order_iff_nsmul_eq_zero, submodule.quotient.mk'_eq_mk, | ||
←submodule.quotient.mk_smul, submodule.quotient.mk_eq_zero, linear_map.mem_range, | ||
algebra.linear_map_apply, algebra_map_int_eq, ring_hom.eq_int_cast, nsmul_eq_mul, mul_comm], | ||
exact ⟨q.denom, q.pos, q.num, mul_denom_eq_num.symm⟩, | ||
end |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think group_theory/specific_groups
is probably a good place for this.
namespace polynomial | ||
|
||
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 | ||
|
||
end polynomial |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This maybe belongs in field_theory.finite
somewhere? Perhaps best to ask on Zulip.
Is it reasonable to add these specific proofs of the existence of non-finite torsion groups? If so, is this the right spot to put that, or should they be distributed into
group_theory/specific_groups
? mathlib doesn't seem to know much aboutQ/Z
at the minute in particular.