AlgHom definition

Stream: mathlib4

[Antoine Chambert-Loir]

In mathlib4, docs#AlgHom is constructed from a docs#RingHom and a commutes' property that involves docs#algebraMap

/-- Defining the homomorphism in the category R-Alg. -/
structure AlgHom (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] extends RingHom A B where
  commutes' : ∀ r : R, toFun (algebraMap R A r) = algebraMap R B r

Why isn't it defined by combining docs#RingHom and docs#LinearMap, as in

/-- (Re)defining the homomorphism in the category R-Alg. -/
structure AlgHom' (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] extends RingHom A B, LinearMap R A B

(My impression is that it would automatize a lot of stuff later.)

[Antoine Chambert-Loir]

(this requires some non straightforward modifications, though, since for example, Mathlib.Algebra.Algebra.Prod is loaded by Mathlib.LinearMap.Prod, as I discovered in trying to push this modification up to the definition of a product of algebras)

[Antoine Chambert-Loir]

I fell upon this while updating mathlib so that docs#MulActionHom could be semilinear, and redefining docs#LinearMap in terms of that, etc. and at some point, the coercion from docs#AlgHom to docs#LinearMap was lost, I don't understand how/why. (This is in #6057, branch#SMulSemiHom)

[Eric Wieser]

I think @Jireh Loreaux has an open PR with this change

[Utensil Song]

#8686 ?

[Antoine Chambert-Loir]

Apparently, #8686 does not touch docs#AlgHom

[Jireh Loreaux]

The point of #8686 is to make docs#AlgEquiv apply more generally. I guess if we did the same for docs#AlgHom we could use it for unital non-associative algebras.

[Jireh Loreaux]

In a few days I will try to finish up #8686. Then we can see if we also want to redefine AlgHom at the same time.