# Zulip Chat Archive

## Stream: maths

### Topic: Interface for algebras

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

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

#### Chris Hughes (Dec 18 2019 at 11:36):

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

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

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

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

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

Thanks, it's on the queue.

#### Johan Commelin (Dec 18 2019 at 12:57):

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

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

Thank you very much Chris!

Last updated: May 09 2021 at 10:11 UTC