Is there a structure for algebras over a given field?

Stream: new members

[Jakob Scholbach]

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]

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

[Thomas Browning]

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 :=
  (intermediate_field.adjoin F generators).to_subalgebra

[Jakob Scholbach]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Jakob Scholbach]

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]

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]

+1