torsion

Stream: mathlib4

[edklencl]

Screenshot_20250128_164138.jpg

[edklencl]

Can you give me a hint

[Damiano Testa]

#mwe ?

[BANGJI HU]

import Mathlib

open AddSubgroup (zmultiples)
open QuotientAddGroup

-- Define QmodZ and RmodZ
abbrev QmodZ := ℚ ⧸ zmultiples (1 : ℚ)
abbrev RmodZ := ℝ ⧸ zmultiples (1 : ℝ)

-- Define the torsion subgroup for an additive group
def AddTorsion (G : Type*) [AddCommGroup G] : AddSubgroup G where
carrier := { x : G | ∃ n : ℕ, n ≠ 0 ∧ n • x = 0 }
add_mem' := by
intro a b ha hb
rcases ha with ⟨n, hn, hna⟩
rcases hb with ⟨m, hm, hmb⟩
use n * m
constructor
sorry
zero_mem' := by
use 1
simp
neg_mem' := by
intro x hx
rcases hx with ⟨n, hn, hnx⟩
use n
simp [hn, hnx]

[Kevin Buzzard]

What did you try? Do you know the maths proof? Can you put the sorry in your code rather than just posting code with errors? All of these things would make your post a better question. It is well known to the community here that you continually ask very low-effort questions; my comments above are guiding you to how to ask a better one.

[Rémy Degenne]

And please stop using two different accounts.

[Kevin Buzzard]

And finally, it would be great if you could do all these things the first time, rather than after being prompted.

What did you try? Do you know the maths proof?

Let us know the answers to these.

[BANGJI HU]

yes ,i try to proove the subgroup is close under addtion,and i try to use ring tactic but fail, i know the math proof

[Kevin Buzzard]

Tell us the math proof! If you know the maths proof and you've got this far, then just finish the job :-) What exactly are you stuck on? Right now you are just asking us to do your work.

[BANGJI HU]

of course i have to use the carrier to proof it is close under addtion

[BANGJI HU]

what tactic should i use to finishi the proof

[BANGJI HU]

Screenshot_20250128_164138 (1).jpg

[BANGJI HU]

why ring does not work

[Johan Commelin]

hand bob said:

of course i have to use the carrier to proof it is close under addtion

You would get 0 points if you handed in :this: as homework solution in my exercise class. So... tell us the maths proof.

[BANGJI HU]

i have check it from mathlib def IsTorsion :=
∀ g : G, IsOfFinOrder g and i try to define the subgroup

[BANGJI HU]

fine i will check it in mathlib

[Kevin Buzzard]

hand bob said:

why ring does not work

Because the axioms for a ring involve +, - and *, and your goal involves • which is not in that list.

[Kevin Buzzard]

The challenge is to write down a rigorous mathematical step-by-step proof of $(nm)\cdot(a+b)=0$ from the axioms you have. Because if you can do that, the translation into Lean is easy and you could do it yourself.

[BANGJI HU]

thanks

[BANGJI HU]

by the way have you heard of deepseek

[Kevin Buzzard]

That question is off-topic for this channel (the answer is "it's on the front pages of all the newspapers in the UK today so of course I've heard of it" but please take any further discussion of this to a relevant channel)

[BANGJI HU]

i define the addtorsion subgroup and i try to use bijiection to proof it ,but the type seem to be mismatch

[BANGJI HU]

open AddSubgroup (zmultiples)

open QuotientAddGroup
-- Define QmodZ and RmodZ

abbrev QmodZ := ℚ ⧸ zmultiples (1 : ℚ)

abbrev RmodZ := ℝ ⧸ zmultiples (1 : ℝ)
-- Define the torsion subgroup for an additive group

def AddTorsion (G : Type*) [AddCommGroup G] : AddSubgroup G where

  carrier := { x : G | ∃ n : ℕ, n ≠ 0 ∧ n • x = 0 }

  add_mem' := by

   intro a b ha hb

   rcases ha with ⟨n, hn, hna⟩

   rcases hb with ⟨m, hm, hmb⟩

   use n * m

   constructor

   · exact mul_ne_zero hn hm

   have h1 : (n * m) • a = m • (n • a) := by

    rw [smul_smul]

    rw [mul_comm]

   have h2 : (n * m) • b = n • (m • b) := by

    rw [@mul_nsmul']

   rw [nsmul_add]  -- Split (n * m) • (a + b) into sum

   rw [h1, h2]     -- Use our rewrite lemmas

   rw [hna, hmb]   -- Use hypotheses about a and b

   simp

    -- Use the facts that n • a = 0 and m • b = 0

  zero_mem' := by

    use 1

    simp

  neg_mem' := by

    intro x hx

    rcases hx with ⟨n, hn, hnx⟩

    use n

    simp [hn, hnx]
-- First define a canonical embedding from Q to R

theorem part_a : AddTorsion RmodZ = QmodZ := by
  exact [AddSubgroup.ext_iff]

[Kim Morrison]

Please post proper code blocks. If the sandbox link isn't there, you didn't do it correctly.

[Edward van de Meent]

(there should be a line break between ``` and import Mathlib :-)