duplication: Algebra.algHom = IsScalarTower.toAlgHom

Stream: mathlib4

[Jz Pan]

Seems that docs#Algebra.algHom and docs#IsScalarTower.toAlgHom are the same map, the latter has more APIs. Should we remove docs#Algebra.algHom in favor of docs#IsScalarTower.toAlgHom ?

[Snir Broshi]

It seems that #22912 introduced Algebra.algHom as

def Algebra.algHom (R : Type*) [CommSemiring R] (S : Type*)
    [Semiring S] [Algebra R S] : R →ₐ[R] S := ...

but then they noticed that this is a special case of a tower so it was generalized even though the tower version already existed.

[Snir Broshi]

(and the tower version was introduced in mathlib3#3272, named to_alg_hom)

[Eric Wieser]

Meanwhile, Algebra.algHom as in the message above is docs#Algebra.ofId

[Eric Wieser]

Which seems like a lousy name

[Antoine Chambert-Loir]

As I answered in a comments of the merged PR, I find it mathematically awkward to rely on IsScalarTower for an algebra morphism that should be there just after the definition of an algebra, and whose absence at this place in the library will prevent people to discover it. For automation, it is probably better to have only one, and maybe that could be achieved by a clever use of simp tags.

[Jz Pan]

Sorry but I don't understand your argument. To define A →ₐ[R] B the condition IsScalarTower R A B is required, so IMO it is an inherent property of IsScalarTower. To define R →ₐ[R] A the IsScalarTower is not necessary, but there is already docs#Algebra.ofId for you.

As for the discoverability problem, a simple search IsScalarTower, |- AlgHom .. on Loogle will reveal docs#IsScalarTower.toAlgHom, and Algebra, |- AlgHom ?a ?a ?b will reveal docs#Algebra.ofId.

[Snir Broshi]

(ofId was introduced in mathlib3#536 as of_id, together with the definition of Algebra)

[Aaron Liu]

Algebra.ofId is also just a special case of IsScalarTower.algHom IsScalarTower.toAlgHom (why is it to) so would we get rid of it too

[Snir Broshi]

There is precedent for having special cases in files higher in the import hierarchy, e.g. EMetricSpace/PseudoEMetricSpace come before PseudoMetricSpace which comes before MetricSpace, and among them have some instance diamonds on purpose just to make the instances available earlier