Interface for algebras

Stream: maths

[Chris Hughes]

I'm trying to finish off algebraic closure.

The interface for algebras is really difficult to use as soon as there are a lot of fields involved.
Right now I have fields K, L and M, such that algebra K L, algebra L M and algebra K M, and the ring homs all commute, but not by definition.

If want to turn an L-algebra hom from M into a K-algebra hom. Normally I would use alg_hom.comap to do this, but that would require the canonical homs to commute by definition, which they do not.

I feel like maybe algebra should not be a class, and we should just use explicit homs.

[Patrick Massot]

Maybe related question: can anyone prove

import ring_theory.algebra_operations

example {R : Type*} [comm_ring R] : (algebra.to_module : module ℤ R) = add_comm_group.module := sorry

[Chris Hughes]

The solution to that is to redefine the Z-algebra instance so that they're defeq.

[Patrick Massot]

I have no idea how to do that. I know very little about that part of the library.

[Chris Hughes]

I have no idea how to do that. I know very little about that part of the library.

#1812

[Johan Commelin]

I'm trying to finish off algebraic closure.

The interface for algebras is really difficult to use as soon as there are a lot of fields involved.
Right now I have fields K, L and M, such that algebra K L, algebra L M and algebra K M, and the ring homs all commute, but not by definition.

If want to turn an L-algebra hom from M into a K-algebra hom. Normally I would use alg_hom.comap to do this, but that would require the canonical homs to commute by definition, which they do not.

I feel like maybe algebra should not be a class, and we should just use explicit homs.

This has been a major pain point and major concern for me as well. I have no idea what the library would look like if we use explicit homs. But I fear it won't look like maths as I know it. Otoh, most lean code doesn't look like that anyway...

[Johan Commelin]

I have no idea how to do that. I know very little about that part of the library.

#1812

Thanks, it's on the queue.

[Johan Commelin]

And merged :smiley: [Thank you Travis, thank you Mergify]

[Patrick Massot]

I have no idea how to do that. I know very little about that part of the library.

#1812

Thank you very much Chris!