Quotient ring basic issue

Stream: mathlib4

[Khang]

I'm trying to start work on quotient rings and ideals, but while trying to warm up on some basic lemmas I faced difficulty, which boils down to this:

import Mathlib.RingTheory.Ideal.Quotient.Defs

variable {R S : Type*} [Ring R] (I : Ideal R) [I.IsTwoSided] [Ring (R ⧸ I)]
  {a b : R}

example (a : R ⧸ I) : Ideal.Quotient.mk I a.out = a := Ideal.Quotient.mk_out a

example (a b : R ⧸ I) : a + b = Ideal.Quotient.mk I (a.out + b.out) := by
  rw [RingHom.map_add]
  rw [Ideal.Quotient.mk_out a, Ideal.Quotient.mk_out b]
  -- ⊢ a + b = a + b
  sorry

The first example works fine: I can recover a value a by Ideal.Quotient.mk I a.out = a. But when I try to throw addition into the mix things get strange. I tried using rfl in the place of sorry, it gives the error

tactic 'rfl' failed, the left-hand side
     @HAdd.hAdd (R ⧸ I) (R ⧸ I) (R ⧸ I)
       (@instHAdd (R ⧸ I)
         (@Distrib.toAdd (R ⧸ I)
           (@NonUnitalNonAssocSemiring.toDistrib (R ⧸ I) Ring.toNonAssocRing.toNonUnitalNonAssocSemiring)))
       a b
   is not definitionally equal to the right-hand side
     @HAdd.hAdd (R ⧸ I) (R ⧸ I) (R ⧸ I)
       (@instHAdd (R ⧸ I)
         (@Distrib.toAdd (R ⧸ I)
           (@NonUnitalNonAssocSemiring.toDistrib (R ⧸ I)
             (Ideal.Quotient.ring I).toNonAssocSemiring.toNonUnitalNonAssocSemiring)))
       a b

which, yes, I guess makes sense but why is it choosing two different ways of getting to a NonUnitalNonAssocSemiring?

[Eric Wieser]

[Ring (R ⧸ I)] is not a safe assumption, it adds a separate ring structure

[Eric Wieser]

Why did you add it?

[Khang]

I added it in hopes that Mathlib defined things like addition as ⟦a + b⟧ = ⟦a⟧ + ⟦b⟧ somewhere.

I find that if I type

#synth Ring (R ⧸ I)

then Lean would look into this to construct the Ring on R / I:

instance ring (I : Ideal R) [I.IsTwoSided] : Ring (R ⧸ I) := fast_instance%
  { __ : AddCommGroup (R ⧸ I) := inferInstance
    __ : Ring (Quotient.ringCon I).Quotient := inferInstance }

[Khang]

Also, if this separate ring structure is not what I'm going for, how should I go about implementing my own Ring structure over R ⧸ I so I can proceed?

[Kenny Lau]

why do you need your own ring structure

[Khang]

I want to be able to have

example {a b : R} : (⟦a + b⟧ : R ⧸ I) = ⟦a⟧ + ⟦b⟧ := sorry

So I can move on, but with the Mathlib's default implementation of a ring over R ⧸ I doesn't allow me to prove that

[Eric Wieser]

import Mathlib.RingTheory.Ideal.Quotient.Defs

variable {R S : Type*} [Ring R] (I : Ideal R) [I.IsTwoSided]
  {a b : R}

example {a b : R} : (⟦a + b⟧ : R ⧸ I) = (show R ⧸ I from ⟦a⟧) + ⟦b⟧ := rfl -- works

[Eric Wieser]

You're not supposed to use ⟦ ⟧ here, you should use docs#Ideal.Quotient.mk instead

[Eric Wieser]

Which you can write as

example {a b : R} : (↑(a + b) : R ⧸ I) = ↑a + ↑b := rfl

[Eric Wieser]

This is all a notational mess that we should clean up, but if you ignore the notation mathlib uses you'll find the lemmas don't apply

[Khang]

Thanks @Eric Wieser ! These will definitely help me move forward.

[Khang]

I also noticed you used a show ... from ... idiom, something I've never seen before. How is

(show R ⧸ I from ⟦a⟧) + ⟦b⟧

different from

(⟦a⟧ : R ⧸ I) + ⟦b⟧

? I would assume it's the same, but the latter doesn't work when placed in your example.

[Ruben Van de Velde]

I'm fuzzy on the details myself, but I think show gives more guarantees that your term is of the correct type?

[Eric Wieser]

show leaves behind a record of what the requested type was, (_ : _) does not