## Stream: new members

### Topic: Is there a structure for algebras over a given field?

#### Jakob Scholbach (Feb 27 2021 at 20:02):

I have defined an intermediate field generated by a few elements like so:

def intermediate_field_generated_by (F L : Type) [field F] [field L] [algebra F L] (generators : set L) : intermediate_field F L :=
subfield.to_intermediate_field (subfield.closure (generators ∪ set.range (algebra_map F L)))
( λ x, begin
apply subfield.subset_closure,
simp,
end )


How can I use this to just extract the datum of the F-algebra (F is the small field here)? If I attempt to def something taking values in algebra F it does not work (and I see why from the definition of the structure algebra. Is there a structure that is adapted to this situation? Thanks!

#### Thomas Browning (Feb 27 2021 at 20:03):

Could you use intermediate_field.adjoin together with intermediate_field.to_subalgebra?

#### Thomas Browning (Feb 27 2021 at 20:05):

This gives you an F-subalgebra of L:

def intermediate_field_generated_by (F L : Type) [field F] [field L] [algebra F L] (generators : set L) : subalgebra F L :=


#### Jakob Scholbach (Feb 27 2021 at 20:05):

Thanks, yes, this works! (I should check the mathlib more thoroughly!)

#### Thomas Browning (Feb 27 2021 at 20:06):

Great, although what exactly do you want when you say that you want the datum of the F-algebra?

#### Thomas Browning (Feb 27 2021 at 20:06):

Technically, intermediate_field.adjoin F generators is already an F-algebra

#### Thomas Browning (Feb 27 2021 at 20:07):

(meaning that there is an instance [algebra F (intermediate_field.adjoin F generators)])

#### Jakob Scholbach (Feb 27 2021 at 20:07):

I want to apply it to prove statements such as https://stacks.math.columbia.edu/tag/09HC, so I need to adjoin elements. I was not aware that this structure is already there in mathlib.

#### Thomas Browning (Feb 27 2021 at 20:09):

I see. If you're doing stuff with separable extensions, you should be aware that the primitive element theorem is in mathlib, which can sometimes be used to avoid nasty induction arguments.

#### Jakob Scholbach (Feb 27 2021 at 20:17):

+1

Last updated: May 11 2021 at 00:31 UTC