Ring quotient by zero ideal.

Stream: maths

[Ashwin Iyengar]

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]

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]

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

[Ashwin Iyengar]

Ahh ok! Thanks.

[Reid Barton]

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

[Ashwin Iyengar]

Yep there is, found it in ideals.lean

[Chris Hughes]

The first isomorphism theorem is probably also there.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

AFAIR ideals are submodules in Lean.