Naming functor maps

Stream: general

[Yaël Dillies]

docs#with_zero.map, docs#with_one.map, docs#add_units.map, docs#units.map, etc... are all bundlings of a functor map. I would have liked them to be called add_hom.with_zero, mul_hom.with_one,add_hom.units, mul_hom.units and indeed I see two problems with the current names:

• There are several ways of bundling those maps, and the current ones only have the merit to be the most common. Consider this:

variables {α β : Type*} [mul_one_class α] [mul_one_class β]

/-- Turn a `monoid_hom` into a `monoid_with_zero_hom` by adjoining a `0` to the domain and codomain.
-/
protected def with_zero.map_as_well (f : α →* β) : with_zero α →*₀ with_zero β :=
{ to_fun := option.map f,
  ... }

The current convention would be to name this... with_zero.map. I can't seem to justify such ambiguity when a more explicit convention exists (namely, add_hom.with_zero for the existing with_zero.map and monoid_hom.with_zero for the above).

• For with_zero and with_one specifically, the names conflict with a missing definition. Namely, the adaptation of docs#option.map. with_zero/with_one being irreducible, this definition is necessary.

[Yaël Dillies]

My proposition is not perfect, as it de-emphasizes the fact that those bundlings really are functor maps and because it creates ambiguity with the case where only one side is mapped. See those two definitions from #11677:

variables {α β : Type*} [semilattice_sup α] [semilattice_sup β]

@[simps] protected def  sup_hom.with_bot (f : sup_hom α β) : sup_hom (with_bot α) (with_bot β) :=
{ to_fun := option.map f,
  ... }

@[simps] def  sup_hom.with_bot' [order_bot β] (f : sup_hom α β) : sup_hom (with_bot α) β :=
{ to_fun := λ a, a.elim ⊥ f,
  ... }

[Yaël Dillies]

This conversation applies to a lesser extent to maps of equivs, eg docs#equiv.option_congr.

[Yaël Dillies]

People who might have an opinion: @Eric Wieser, @Bhavik Mehta, @Anne Baanen

[Eric Wieser]

I agree that the current names with the type before the dot are not ideal.

[Eric Wieser]

sup_hom.with_bot' looks a bit like what I would expect with_bot.lift_sup_hom to be called

[Anne Baanen]

Overall I think we should de-emphasize the domain/codomain and emphasize the mapped type in these names.

[Anne Baanen]

Out-there option: some sort of has_map typeclass?

[Kevin Buzzard]

There's also the issue that monoid homs are group homs too so they map submonoids to submonoids and subgroups to subgroups