Zulip Chat Archive

Stream: general

Topic: What is and isn't in scope for `ext`?


Eric Wieser (Feb 10 2021 at 18:25):

I recently made some changes to ext that allow it to recurse into tensor products and products when equating linear maps. I'm wondering where to draw the line on what should and what shouldn't be an ext lemma.

For instance, this is almost certainly a badext lemma, as the user could just apply induction:

@[ext]
lemma function.nat_ext {β : Type*} {f g :   β}
  (h0 : f 0 = g 0)
  (h :  n, f n = g n  f n.succ = g n.succ) : f = g :=
funext $ λ x, nat.rec h0 h x

What about when the bundled function allows one of the inductive cases to be eliminated? Is this a bad ext lemma?

import algebra.group.hom

@[ext]
lemma zero_hom.nat_ext {β : Type*} [has_zero β] {f g : zero_hom  β}
  (h :  n, f n = g n  f n.succ = g n.succ) : f = g :=
zero_hom.ext $ λ x, nat.rec (f.map_zero.trans g.map_zero.symm) h x

In the same line of ext lemma, we have docs#add_monoid_hom.ext_nat which is marked ext, and docs#ring_hom.ext_nat which is not.

Eric Wieser (Feb 10 2021 at 18:33):

The actual context of the question is whether this should be an ext lemma:

/-- Two linear maps agree if they agree on 1, `ι`, and agree on a product if they agree on its parts. -/
@[ext]
def exterior_algebra.hom_extₗ {N : Type*} [add_comm_monoid N] [semimodule R N] {f g : exterior_algebra R M →ₗ[R] N}
  (h_one : f 1 = g 1)
  (h_mul :  x y, f x = g x  f y = g y  f (x * y) = g (x * y))
  (h_ι : f.comp (ι R M) = g.comp (ι R M)) : f = g :=

Mario Carneiro (Feb 10 2021 at 18:53):

I don't think ext lemmas should be recursive

Mario Carneiro (Feb 10 2021 at 18:53):

which would exclude all three examples

Eric Wieser (Feb 10 2021 at 18:54):

Do you object to linear_map.prod_ext (#6124) then too?

Mario Carneiro (Feb 10 2021 at 18:55):

bad link

Eric Wieser (Feb 10 2021 at 18:55):

Fixed

Mario Carneiro (Feb 10 2021 at 18:56):

no, that's fine

Mario Carneiro (Feb 10 2021 at 18:56):

recursive here meaning that there are equalities in the assumptions of a hypothesis to the theorem

Mario Carneiro (Feb 10 2021 at 18:57):

the theorem hypotheses should just be plain equalities or universally quantified equalities

Eric Wieser (Feb 10 2021 at 18:57):

That's a reasonable rule

Eric Wieser (Feb 10 2021 at 18:57):

Which means that presumably ring_hom.ext_nat should be marked ext

Mario Carneiro (Feb 10 2021 at 19:03):

There's also the matter of "canonicality" though; too many ext lemmas and it's not clear what's going to get applied when you use ext, since you don't specify which ext lemma to apply

Mario Carneiro (Feb 10 2021 at 19:03):

it is basically the same kind of situation as typeclass instances being "unique"

Mario Carneiro (Feb 10 2021 at 19:04):

ring_hom.ext_nat looks more like a subsingleton instance to me

Eric Wieser (Nov 08 2023 at 10:41):

Mario Carneiro said:

docs#RingHom.ext_nat looks more like a subsingleton instance to me

Reviving an old thread since I can't find whether we discussed this elsewhere; should ext try subsingleton elimination at every step? Or should we instead add ext lemmas with no hypotheses for the special cases where we actually expect a subsingleton?

#8168 explores this latter option by adding theorem ext_id (f g : R →ₐ[R] A) : f = g, and this cleans up some side goals downstream


Last updated: Dec 20 2023 at 11:08 UTC