Zulip Chat Archive

Stream: maths

Topic: Interface for algebras


view this post on Zulip Chris Hughes (Dec 18 2019 at 11:18):

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.

view this post on Zulip Patrick Massot (Dec 18 2019 at 11:33):

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

view this post on Zulip Chris Hughes (Dec 18 2019 at 11:36):

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

view this post on Zulip Patrick Massot (Dec 18 2019 at 12:01):

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

view this post on Zulip Chris Hughes (Dec 18 2019 at 12:15):

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

#1812

view this post on Zulip Johan Commelin (Dec 18 2019 at 12:21):

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...

view this post on Zulip Johan Commelin (Dec 18 2019 at 12:57):

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.

view this post on Zulip Johan Commelin (Dec 18 2019 at 12:57):

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

view this post on Zulip Patrick Massot (Dec 18 2019 at 13:15):

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

#1812

Thank you very much Chris!


Last updated: May 09 2021 at 10:11 UTC