Naming of liftAlgHom in PiTensorProduct

Stream: mathlib4

[Robert Maxton]

Having looked into Mathlib.RingTheory.PiTensorProduct to show equivalence to FreeProduct in the commutative case, I found docs#PiTensorProduct.liftAlgHom. Unlike e.g. docs#RingQuot.liftAlgHom or many others which lift AlgHoms to AlgHoms, PiTensorProduct.liftAlgHom lifts a MultilinearMap to an AlgHom.

Is this the sort of thing that should just be changed, either by renaming or by providing the expected API, or is this an insufficient reason to change an existing file? I'm new to working in large collaborations so this is as much a question about social norms as anything else

[Robert Maxton]

Paging @Jujian Zhang whose name is on the file

[Robert Maxton]

(Personally I would strongly prefer, especially in PiTensorProduct which is the canonical coproduct in $R\textbf{-CAlg}$, that the name lift be reserved for "homogenous" lifts of morphisms within a specific category, whether that be $R\textbf{-Mod}$ for MultilinearMap or $R\textbf{-Alg}$ in this case. I'll need to write the $R\textbf{-Alg}$ version either way to prove the equivalence, so this is mostly a question about naming priority.)

[Eric Wieser]

I think the homogenous version is usual called map not lift? Maybe I misunderstand which version you're describing.

[Robert Maxton]

map usually relates functions that are semantically "parallel" or equivalent; the general form is Functor.map
lift usually factors a function into a standard part general to the type constructor and the specific part to the function you're factoring

[Robert Maxton]

map usually produces functions that have a type constructor application on both sides of the arrow
map (f : α → β) : τ α → τ β
lift usually produces functions that have an application on the domain only
lift (f : α → β) : τ α → β

[Eric Wieser]

Ah, then you're using a different meaning of homogenous to the one I thought

[Eric Wieser]

Do you object to the naming of docs#TensorAlgebra.lift, or docs#WithOne.lift ?

[Robert Maxton]

Ah, yeah. By "homogenous" I mean that lift should take AlgHoms and return an AlgHom

[Robert Maxton]

Eric Wieser said:

Do you object to the naming of docs#TensorAlgebra.lift, or docs#WithOne.lift ?

Somewhat, but it's much lessened there by the fact that e.g. TensorAlgebra concept is inherently one that turns something that isn't an algebra into an algebra, so homogeneity/staying within a category is impossible
In that regard while PiTensorProduct.lift mildly bugs me, it's liftAlgHom, which is in the Algebra subfile and has AlgHom in the name but doesn't take a family of AlgHoms, that I actually object to

[Eric Wieser]

Ah, sorry for not doing this earlier. Now that I clicked on the link, I think morally PiTensorProduct.liftAlgHom takes a "MultiAlgebraMap`, but that type doesn't exist (and may not be useful anywhere else), so it takes it in pieces as a multilinear map and some extra assumptions.

[Eric Wieser]

Is it necessarily the case that on algebras, such a map always factorizes as a collection of algebra maps composed with the product "multialgebra map"?

[Robert Maxton]

I dunno about factorizes but it's certainly true that such a map is always uniquely defined by such
that's basically what makes it the categorical coproduct; if I give you a family of maps I've specified exactly one map out of the tensor product and vice versa

[Robert Maxton]

Conceptually, for a family of maps f : (i : ι) → A i →ₗ[R] S, this is basically just

--wrong
liftAlgHom (MultilinearMap.mkPiAlgebra R ι S |>.compLinearMap f) ...

But mkPiAlgebra, and similar functions like bigprod, require Fintype ι, which I haven't assumed yet and don't want to

[Robert Maxton]

They can theoretically work with finite support on a non-Fintype too, which as a coproduct I believe I do actually have here, but I haven't figured out how to use that fact yet
I may end up resorting to transfinite induction/well-ordering