AlgHom.equalizer / LinearMap.eqLocus

Stream: mathlib4

[Antoine Chambert-Loir]

mathlib know various versions of equalizers, the natural substructure where two morphisms are equal, for linear maps, it is called eqLocus, see docs#LinearMap.eqLocus and docs#AddHom.eqLocus, but for algebra maps, it is called equalizer, see docs#AlgHom.equalizer and docs#StarAlgHom.equalizer.
Moreover, docs#AlgHom.equalizer takes two docs#AlgHom as inputs, while docs#LinearMap.eqLocus takes two member of some docs#LinearMapClass

I have two questions.

• Should the names be aligned?

• Should they all take …Class as inputs?

[Kim Morrison]

I'd be happy to seem the names aligned (my preference is for equalizer, even if we end up extending this to categories where it is not even a categorical equalizer).

[Kim Morrison]

No opinion re: ...Class.

[Jireh Loreaux]

I've merged this (with Class, but without assigned names). Note that all the "algebra" flavors use equalizer, so we should align them simultaneously if we do it.