Module

SubfieldRoots.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.SubfieldRoots

2 declarations indexed from sourceView source ↗

Module documentation

Root finiteness in subfields

A finite separable extension of a subfield embeds in a finite extension of the ambient field. In characteristic zero this descends finiteness of primary roots of unity to finite extensions of the subfield.

Imports3

Nyll.GaloisCohomology.Kummer.Concrete.PrimaryRootsFiniteness
Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by2

theorem

finiteExtension_embedding_over_subfield

L24 ↗

Yamaguchi26AbfaithfulGalois.finiteExtension_embedding_over_subfield

Documentation

A finite separable extension of a subfield embeds in a finite extension of the ambient field, using a primitive generator.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace Yamaguchi26AbfaithfulGalois
universe u v w

Lean source · statement

theorem finiteExtension_embedding_over_subfield
    (K : Type u) (E : Type v) (L : Type w)
    [Field K] [Field E] [Field L] [Algebra K E] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    ∃ T : IntermediateField E (AlgebraicClosure E), FiniteDimensional E T ∧
      Nonempty (L →+* T)

theorem

finite_primaryComponent_finiteExtension_of_subfield

L55 ↗

Yamaguchi26AbfaithfulGalois.finite_primaryComponent_finiteExtension_of_subfield