non finsupp finsupp.dom_congr

Stream: Is there code for X?

[Kevin Buzzard]

import algebra.monoid_algebra.basic

variables {S T A : Type*} [add_comm_group A]

/-
finsupp.dom_congr :
  Π {α : Type u_4} {β : Type u_5} {M : Type u_6} [_inst_1 : add_comm_monoid M],
    α ≃ β → (α →₀ M) ≃+ (β →₀ M)
    -/

-- what is the non-finsupp version of finsupp.dom_congr
#find ((S ≃ T) → ((S → A) ≃+ (T → A)))

What's the regular function version called? I don't know how to find out without asking.

[Eric Wieser]

docs#add_equiv.arrow_congr?

[Kevin Buzzard]

Oh nice! Thanks! I didn't know → was called arrow.

[Eric Wieser]

It's a bit annoying that we sometimes have one definition (M ≃ N) → (P ≃+ Q) → ((M → P) ≃+ (N → Q)) (like arrow_congr) and other times (like finsupp.dom_congr) have two, (M ≃ N) → ((M → P) ≃+ (N → P)) and (P ≃+ Q) → ((M → P) ≃+ (M → Q)). IMO the separate definitions make slightly more sense as they're simpler operations.