subalgebra pain

Stream: maths

[Chris Hughes]

I have some fields, K and L and N : subalgebra K L. I now need algebra K (algebra.adjoin N {(x : L)} : subalgebra N L) What's the best way to get this instance and all the 4 choose 3 is_scalar tower instances I might need?

[Eric Wieser]

Does docs#subalgebra.algebra exist and answer your question?

[Eric Wieser]

Hmm, it doesn't allow scalar towers

[Eric Wieser]

I guess either that should be fixed, or the tower version is defined elsewhere

[Chris Hughes]

That would give me algebra N (algebra.adjoin N {x}), but I need algebra K (algebra.adjoin N {x})

[Chris Hughes]

I know N is a K algebra, so it's basically transitivity of algebra, but then I'll probably need the fact that everything commutes.

[Eric Wieser]

I think the conditions should be the same as docs#submodule.module'

[Chris Hughes]

I think so.

[Chris Hughes]

But we'll need two extra is_scalar_tower instances for this.

[Eric Wieser]

Why two? Isn't K L N enough

[Chris Hughes]

You need K (algebra.adjoin N {x}) L and N (algebra.adjoin N {x}) L. If you have a chain of n fields you're going to need n choose 3 is_scalar_tower instances.

[Chris Hughes]

I actually already have is_scalar_tower N (algebra.adjoin N {x}) L, so I guess it's just one extra. is_scalar_tower never felt like it would work for more complicated diagrams, but maybe it does.

[Kevin Buzzard]

I think is_scalar_tower just says "one triangle commutes in this diagram" and in a complex diagram there might be lots of triangles

[Johan Commelin]

Maybe a little bit of meta code could help us add all those triangles to the context.

[Johan Commelin]

Certainly lean 4 macros should be able to help us there.

[Johan Commelin]

long_scalar_tower [A, B, C, D, E] just expands to 5 choose 3 versions of [is_scalar_tower foo bar baz]

[Eric Wieser]

I'll add the missing instance here tomorrow, probably

[Chris Hughes]

I really wanted this quickly so #9062

[Eric Wieser]

I have the more general version I was thinking of locally, just with an easy sorry left

[Eric Wieser]

has docs#subalgebra.algebra' now resolved this?

[Chris Hughes]

Yes. It was all motivated by #9110