Stating the theorem that no ring isomorphism 2Z and 3Z

Stream: new members

[Tom]

I am trying to state the theorem that the rings 2ℤ and 3ℤ are not isomorphic. However I am not sure which type to use to represent the quotient set on ℤ given by ℤMod2 and ℤMod3.

Any ideas appreciated, I have a feeling that its something to do with the Quotient type perhaps.

Here is my attempt so far which fails to typecheck.

def zmod2_not_isomorphic_to_zmod3 : IsEmpty ((ℤ ⧸ ZMod 2) ≃+* ℤ ⧸ ZMod 3) := by
  sorry

I get failed to synthesize HasQuotient ℤ Type as an error. Is this because ℤ needs to be replaced with the ring of ℤ maybe.

[Aaron Liu]

Just use docs#ZMod

[Snir Broshi]

Ideal.span {2} and Ideal.span {3}?

[Snir Broshi]

docs#Int.quotientSpanNatEquivZMod if you still want to talk about quotients

[Aaron Liu]

like this

import Mathlib

theorem isEmpty_zmod2_ringEquiv_zmod3 : IsEmpty (ZMod 2 ≃+* ZMod 3) := by
  sorry

[Aaron Liu]

Tom said:

I am trying to state the theorem that the rings 2ℤ and 3ℤ are not isomorphic.

What is 2ℤ and 3ℤ? Do you mean $\mathbb{Z}/2\mathbb{Z}$ and $\mathbb{Z}/3\mathbb{Z}$?

[Snir Broshi]

Aaron Liu said:

like this

import Mathlib

theorem isEmpty_zmod2_ringEquiv_zmod3 : IsEmpty (ZMod 2 ≃+* ZMod 3) := by
  sorry

This isn't 2ℤ and 3ℤ, this is ℤ/2ℤ and ℤ/3ℤ.

[Tom]

Yep $\mathbb{Z}/2\mathbb{Z}$ and $\mathbb{Z}/3\mathbb{Z}$

[Snir Broshi]

Aaron Liu said:

What is 2ℤ and 3ℤ?

Ideal.span {2} and Ideal.span {3}

[Aaron Liu]

oh those aren't rings

[Aaron Liu]

they're nonunital rings

[Snir Broshi]

Yeah and they're both cyclic as additive groups so they are isomorphic

[Aaron Liu]

they're not isomorphic as nonunital rings

[Tom]

I flicked open dummit and foote which isnt the textbook I am working through to get more practice exercises and thats where I saw 2ℤ and 3ℤ. I assumed this was different notation for  $\mathbb{Z}/2\mathbb{Z}$ and $\mathbb{Z}/3\mathbb{Z}$. So I may have just confused myself by textbook hopping.

[Aaron Liu]

I think they're referring to the nonunital rings

[Snir Broshi]

nℤ is usually notation for the ideal in ℤ generated by n, and it's also the additive identity of ℤ/nℤ, where cosets are denoted by nℤ+k

[Aaron Liu]

I found the exercise

[Aaron Liu]

Prove that the rings $2\mathbb{Z}$ and $3\mathbb{Z}$ are not isomorphic.

[Snir Broshi]

ℤ/nℤ denotes residues mod n precisely because nℤ denotes the ideal, so taking a quotient by that ideal gives the residues

[Tom]

Ideals is the next chapter on the textbook I am actually working on :D

[Snir Broshi]

Aaron Liu said:

Prove that the rings $2\mathbb{Z}$ and $3\mathbb{Z}$ are not isomorphic.

Maybe rings in the book are defined to be nonunital, or the book uses strange notation for ZMod

[Aaron Liu]

yeah my best guess is nonunital rings since they do also mention $\mathbb{Z}/12\mathbb{Z}$

[Tom]

Before the exercise it states

Let R be a ring with identity 1 \neq 0.

[Aaron Liu]

if all rings were unital the R having identity would be redundant

[Aaron Liu]

so I'm gonna say these are the nonunital rings

[Aaron Liu]

try this

import Mathlib

theorem isEmpty_idealSpan_singleton_two_ringEquiv_idealSpan_singleton_three :
    IsEmpty (Ideal.span {2} ≃+* Ideal.span {3}) := by
  sorry

[Tom]

Okay thanks, will try that. Thanks @Aaron Liu and @Snir Broshi for your time!

[Junyan Xu]

Those are 2ℕ and 3ℕ ...

[Snir Broshi]

yeah they need : ℤ

[Aaron Liu]

ahh default numerals nat strikes again