Compositum of fields

Stream: Is there code for X?

[Kevin Buzzard]

We don't have this, right? Given $L$ and $M$ two $K$-algebras, I want the compositum $LM$, some $K$-algebra containing $L$ and $M$ and generated by them. Do we want an IsCompositum predicate and if so, what should it eat? In my application (class field theory) I need an explicit construction (and $L$,$M$ are unrelated extensions of $K$ and both types). Any thoughts on the best way to formalize this if we don't have it already?

[Damiano Testa]

Do the conditions that you specify determine LM uniquely?

[Damiano Testa]

I think that I've seen this mostly in the context of subfields of a given field. Where the important part is that there is a common ambient for both.

[Damiano Testa]

I'm thinking of adding a cube root of 2 to Q and then the compositum of this field with itself could be either just itself or the splitting field of x ^ 3 - 2.

[Damiano Testa]

Maybe you could use any subalgebra of $L \otimes_K M$ with the conditions that you mention?

[Kevin Buzzard]

No they don't, but if one of $L$ and $M$ are Galois then they do.

[Damiano Testa]

So, I think that the tensor product should contain all possibilities.

[Damiano Testa]

(Up to isomorphism, of course.)

[Riccardo Brasca]

I am almost sure everything we have in mathlib is about subobjects of an ambient space.

[Andrew Yang]

IsCompositum probably takes [Algebra L E] [Algebra M E] and says that (algebraMap L E).fieldRange \sup (algebraMap M E).fieldRange = \top

[Kenny Lau]

Yeah that's basically what we did.

[Adam Topaz]

Don’t you want to take the quotient of $L\otimes_K M$ by a maximal ideal?

[Kenny Lau]

that is also what we did. we made both Compositum and IsCompositum.

[Adam Topaz]

Ok cool

[Antoine Chambert-Loir]

I would say that you don't want a construction because it depends on choices in general, but IsCompositum E K L M would say that the E-algebra M is generated by its subalgebras K and L makes sense. Then, you'd need the existence of compositum and their uniqueness (up to isomorphism) if as you say K or Lis Galois over E, or if one of them is K is “regular” (which is more or less the definition of regular, with possible characterizations in terms of tensor product with alg. closure of K)

[Kenny Lau]

we can still make an arbitrary one, it's the philosophy of junk value