Zulip Chat Archive

Stream: general

Topic: Eliminating function applications


Eric Wieser (Jan 19 2021 at 18:30):

I've found myself faced with a goal like f a = a multiple times now, where f is some bundled morphism.
In these cases, I have tools availabe to work with equalities of morphisms directly, but f is some horrible expression so using suffices : f = id isn't feasible.

It's tempting to add a lemma like:

lemma linear_map.idem_iff_id {M : Type*} [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) :
  ( a, f a = a)  f = linear_map.id :=
λ hm, linear_map.ext hm, λ h, h.symm  λ a, rfl

Is this type of lemma sensible? Can anyone suggest a better name than idem_iff_id?

Floris van Doorn (Jan 19 2021 at 18:46):

If we have a version of docs#linear_map.ext_iff with g (and f) explicit, you could easily do what you want with that lemma by setting g := linear_map.id, and that would be a generalization of your lemma. I'm not sure if it's worth it to also add your lemma.


Last updated: Dec 20 2023 at 11:08 UTC