Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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!

view this post on Zulip Thomas Browning (Feb 27 2021 at 20:03):

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

view this post on Zulip 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 :=
  (intermediate_field.adjoin F generators).to_subalgebra

view this post on Zulip Jakob Scholbach (Feb 27 2021 at 20:05):

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

view this post on Zulip 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?

view this post on Zulip Thomas Browning (Feb 27 2021 at 20:06):

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

view this post on Zulip Thomas Browning (Feb 27 2021 at 20:07):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jakob Scholbach (Feb 27 2021 at 20:17):

+1


Last updated: May 11 2021 at 00:31 UTC