## 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 $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

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):

AFAIR ideals are submodules in Lean.

Last updated: May 19 2021 at 02:10 UTC