eq.rec_on

Stream: general

[Johan Commelin]

Ok, so apparently eq.rec_on is evil. I'm not sure that I really understand when it is ok to use it, and when not. Can someone explain this to me in more detail?
I still find it somewhat hard to stomach that if I have two ideals in a ring, and they are provably equal, that I have to do so much work to get a ring isomorphism between the quotients. This is not transport of structure along some "canonical" isomorphism. This is equality. I had really hoped that proof irrelevance would help here.

[Kevin Buzzard]

Shouldn't this all be in Lean already? If $I\subseteq J$ then there should be a surjection $R/I\to R/J$.

[Kevin Buzzard]

At the very least there will be a surjection of $R$-modules.

[Kevin Buzzard]

But you're supposed to use quotient.lift not eq.rec

[Kevin Buzzard]

because this preserves computability mumble mumble don't know what I'm talking about

[Johan Commelin]

That still doesn't explain why eq.rec is evil, and why it exists, and why it is sometimes useful. Also, I know that workarounds exist. But really we are now writing >500 lines of code just to show that if two valuations are equivalent, then so are their valuation rings. And after 10 lines we know that if two valuations are equivalent, then they define two ideals that are equal. After that, it should be a no-brainer. But it's not.

[Kenny Lau]

import ring_theory.ideal_operations data.equiv.algebra

example {R : Type*} [comm_ring R] {I J : ideal R} (h : I = J) : I.quotient ≃r J.quotient :=
by subst h; exact ring_equiv.refl _

[Johan Commelin]

But that requires your bundled ring maps (-;
I don't have those yet.

[Chris Hughes]

They're in mathlib

[Johan Commelin]

When did that happen?

[Johan Commelin]

How did I miss that?

[Kenny Lau]

no that's a ring equiv, not a bundled ring hom

[Chris Hughes]

Don't you want a particular isomorphism though? This is the right one, but it's hard to prove.

[Kenny Lau]

what do you mean by hard to prove?

[Kenny Lau]

aha so "ring equiv" is like a cheating version of ring hom

[Kenny Lau]

and that turns out to work

[Kenny Lau]

so again, bundled maps for the win

[Johan Commelin]

No, I think ring_equiv is fine for my purposes.

[Chris Hughes]

prove that (quotient.mk \circ example) = quotient.mk

[Chris Hughes]

Maybe that's easy actually

[Kenny Lau]

import ring_theory.ideal_operations data.equiv.algebra

variables {R : Type*} [comm_ring R] {I J : ideal R} (h : I = J)
include h

def what : I.quotient ≃r J.quotient :=
eq.rec_on h $ ring_equiv.refl _

example (x) : (what h).to_fun (ideal.quotient.mk I x) = ideal.quotient.mk J x :=
by subst h; refl

[Johan Commelin]

@Mario Carneiro What's going on here?

[Chris Hughes]

But that last one would be rfl if you used lift

[Johan Commelin]

Sure, but Kenny's definition of what is way shorter.

[Kenny Lau]

import ring_theory.ideal_operations data.equiv.algebra

variables {R : Type*} [comm_ring R] {I J : ideal R} (h : I = J)
include h

def what : I.quotient ≃r J.quotient :=
{ to_fun := ideal.quotient.lift _ (ideal.quotient.mk J) (λ r hr, h ▸ ideal.quotient.eq_zero_iff_mem.2 hr),
  inv_fun := ideal.quotient.lift _ (ideal.quotient.mk I) (λ r hr, h.symm ▸ ideal.quotient.eq_zero_iff_mem.2 hr),
  left_inv := λ x, quotient.induction_on' x $ λ r, rfl,
  right_inv := λ x, quotient.induction_on' x $ λ r, rfl,
  hom := ⟨rfl, λ x y, quotient.induction_on₂' x y $ λ r s, rfl, λ x y, quotient.induction_on₂' x y $ λ r s, rfl⟩ }

example (x) : (what h).to_fun (ideal.quotient.mk I x) = ideal.quotient.mk J x := rfl

[Reid Barton]

You're never actually stuck when you have eq.rec_on in terms, it's just that you need to do this generalize/cases/refl dance any time you want to manipulate them. It's awkward to do this in the middle of a proof, so effectively you have to prove a lemma (like Kenny's example).

[Reid Barton]

It's conceivable one could automate this with a tactic

[Johan Commelin]

But the version that proves the lemma is significantly shorter.

[Kenny Lau]

yes, always extract lemmas