Naming congruence of maps

Stream: mathlib4

[Yaël Dillies]

There is a general pattern that if A →something B is a type of maps and e : A ≃something A' is an isomorphism, then we get an isomorphism (A →something B) ≃something (A' →something B), and similarly for e : B ≃something B'

[Yaël Dillies]

Naming of these "congruence" isomorphisms is all over the place, and it would be good to unify them

[Yaël Dillies]

Eric and I are adding a few in #25142 and #25182, and we would like to know what the community thinks before we commit to more names

[Yaël Dillies]

Here are some examples (taken from Eric's PR):

• docs#AlternatingMap.domLCongr
• docs#ContinuousLinearEquiv.compContinuousMultilinearMapL
• docs#ContinuousLinearEquiv.continuousAlternatingMapCongrLeft
• docs#ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv (not a linear equiv)
• docs#ContinuousLinearEquiv.continuousMultilinearMapCongrRight
• docs#ContinuousLinearEquiv.continuousAlternatingMapCongrRight

[Yaël Dillies]

and some examples coming from my PR instead:

• docs#MulEquiv.monoidHomCongr
• docs#MonoidHom.precompEquiv
• docs#MonoidHom.postcompEquiv

[Eric Wieser]

Some more examples:

• docs#LinearEquiv.congrLeft
• docs#LinearEquiv.funCongrLeft (the two somethings are not from the same category here)

[Eric Wieser]

It looks like maybe FooEquiv.barMapCongrSide is the plurality winner right now, perhaps with some exception that says FooEquiv.fooMapCongrSide becomes FooEquiv.congrSide?

[Eric Wieser]

#24159 seems to support this (it renamed one of the items on your list)