Zulip Chat Archive

Stream: maths

Topic: Ring quotient by zero ideal.


Ashwin Iyengar (May 25 2020 at 14:23):

I'm trying to show that the commutative nonzero ring homomorphism RR/(0)R \to R/(0) is an isomorphism, by constructing an inverse. I'm doing this:

noncomputable def quo_by_zero_ideal_bij : R +* (: ideal R).quotient :=
{ inv_fun   := λ x, classical.some (quot.exists_rep x),
  left_inv  := sorry,
  right_inv := sorry,
  ..ideal.quotient.mk_hom ( : ideal R) }

But intuitively I would think that this really should be computable. Is my intuition correct?

Ashwin Iyengar (May 25 2020 at 14:24):

Maybe the right thing to do is show that the set of lifts is a singleton and then pick the element from the singleton?

Reid Barton (May 25 2020 at 14:25):

In general you should use quotient.lift to define a function out of a quotient

Ashwin Iyengar (May 25 2020 at 14:26):

Ahh ok! Thanks.

Reid Barton (May 25 2020 at 14:26):

In this case, I shouldn't be surprised if there's already something defined for mapping out of a quotient ring

Ashwin Iyengar (May 25 2020 at 14:26):

Yep there is, found it in ideals.lean

Chris Hughes (May 25 2020 at 14:26):

The first isomorphism theorem is probably also there.

Yury G. Kudryashov (May 25 2020 at 15:33):

See also https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#submodule.quot_equiv_of_eq_bot

Yury G. Kudryashov (May 25 2020 at 15:33):

AFAIR ideals are submodules in Lean.


Last updated: Dec 20 2023 at 11:08 UTC