Zulip Chat Archive

Stream: general

Topic: eq.rec_on


Johan Commelin (Feb 14 2019 at 18:09):

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 (Feb 14 2019 at 18:11):

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

Kevin Buzzard (Feb 14 2019 at 18:11):

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

Kevin Buzzard (Feb 14 2019 at 18:12):

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

Kevin Buzzard (Feb 14 2019 at 18:12):

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

Johan Commelin (Feb 14 2019 at 18:26):

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 (Feb 14 2019 at 18:31):

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 (Feb 14 2019 at 18:34):

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

Chris Hughes (Feb 14 2019 at 18:34):

They're in mathlib

Johan Commelin (Feb 14 2019 at 18:35):

When did that happen?

Johan Commelin (Feb 14 2019 at 18:35):

How did I miss that?

Kenny Lau (Feb 14 2019 at 18:35):

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

Chris Hughes (Feb 14 2019 at 18:35):

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

Kenny Lau (Feb 14 2019 at 18:35):

what do you mean by hard to prove?

Kenny Lau (Feb 14 2019 at 18:36):

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

Kenny Lau (Feb 14 2019 at 18:36):

and that turns out to work

Kenny Lau (Feb 14 2019 at 18:36):

so again, bundled maps for the win

Johan Commelin (Feb 14 2019 at 18:36):

No, I think ring_equiv is fine for my purposes.

Chris Hughes (Feb 14 2019 at 18:36):

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

Chris Hughes (Feb 14 2019 at 18:37):

Maybe that's easy actually

Kenny Lau (Feb 14 2019 at 18:38):

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 (Feb 14 2019 at 18:39):

@Mario Carneiro What's going on here?

Chris Hughes (Feb 14 2019 at 18:41):

But that last one would be rfl if you used lift

Johan Commelin (Feb 14 2019 at 18:47):

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

Kenny Lau (Feb 14 2019 at 18:56):

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 (Feb 14 2019 at 18:58):

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 (Feb 14 2019 at 18:58):

It's conceivable one could automate this with a tactic

Johan Commelin (Feb 14 2019 at 19:02):

But the version that proves the lemma is significantly shorter.

Kenny Lau (Feb 14 2019 at 19:03):

yes, always extract lemmas


Last updated: Dec 20 2023 at 11:08 UTC