Adjoining Elements to Fields #

In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. For example, Algebra.adjoin K {x} might not include x⁻¹.

Main results #

adjoin_adjoin_left: adjoining S and then T is the same as adjoining S ∪ T.
bot_eq_top_of_rank_adjoin_eq_one: if F⟮x⟯ has dimension 1 over F for every x in E then F = E

Notation #

F⟮α⟯: adjoin a single element α to F.

source

def IntermediateField.adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

IntermediateField F E

adjoin F S extends a field F by adjoining a set S ⊆ E.

Instances For

source

@[simp]

theorem IntermediateField.adjoin_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {T : IntermediateField F E} :

IntermediateField.adjoin F S ≤ T ↔ S ≤ ↑T

source

theorem IntermediateField.gc {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

GaloisConnection (IntermediateField.adjoin F) fun x => ↑x

source

def IntermediateField.gi {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

GaloisInsertion (IntermediateField.adjoin F) fun x => ↑x

Galois insertion between adjoin and coe.

Instances For

source

instance IntermediateField.instCompleteLatticeIntermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

CompleteLattice (IntermediateField F E)

source

instance IntermediateField.instInhabitedIntermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Inhabited (IntermediateField F E)

source

theorem IntermediateField.coe_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↑⊥ = Set.range ↑(algebraMap F E)

source

theorem IntermediateField.mem_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :

x ∈ ⊥ ↔ x ∈ Set.range ↑(algebraMap F E)

source

@[simp]

theorem IntermediateField.bot_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊥.toSubalgebra = ⊥

source

@[simp]

theorem IntermediateField.coe_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↑⊤ = Set.univ

source

@[simp]

theorem IntermediateField.mem_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :

x ∈ ⊤

source

@[simp]

theorem IntermediateField.top_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊤.toSubalgebra = ⊤

source

@[simp]

theorem IntermediateField.top_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IntermediateField.toSubfield ⊤ = ⊤

source

@[simp]

theorem IntermediateField.coe_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (T : IntermediateField F E) :

↑(S ⊓ T) = ↑S ∩ ↑T

source

@[simp]

theorem IntermediateField.mem_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} {x : E} :

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

source

@[simp]

theorem IntermediateField.inf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (T : IntermediateField F E) :

(S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

source

@[simp]

theorem IntermediateField.inf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (T : IntermediateField F E) :

IntermediateField.toSubfield (S ⊓ T) = IntermediateField.toSubfield S ⊓ IntermediateField.toSubfield T

source

@[simp]

theorem IntermediateField.coe_sInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

↑(sInf S) = sInf ((fun x => ↑x) '' S)

source

@[simp]

theorem IntermediateField.sInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

(sInf S).toSubalgebra = sInf (IntermediateField.toSubalgebra '' S)

source

@[simp]

theorem IntermediateField.sInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

IntermediateField.toSubfield (sInf S) = sInf (IntermediateField.toSubfield '' S)

source

@[simp]

theorem IntermediateField.coe_iInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

↑(iInf S) = ⋂ (i : ι), ↑(S i)

source

@[simp]

theorem IntermediateField.iInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

(iInf S).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra

source

@[simp]

theorem IntermediateField.iInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

IntermediateField.toSubfield (iInf S) = ⨅ (i : ι), IntermediateField.toSubfield (S i)

source

@[simp]

theorem IntermediateField.equivOfEq_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} (h : S = T) (x : { x // x ∈ S }) :

↑(IntermediateField.equivOfEq h) x = { val := ↑x, property := (_ : ↑x ∈ T) }

source

def IntermediateField.equivOfEq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} (h : S = T) :

{ x // x ∈ S } ≃ₐ[F] { x // x ∈ T }

Construct an algebra isomorphism from an equality of intermediate fields

Instances For

source

@[simp]

theorem IntermediateField.equivOfEq_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} (h : S = T) :

AlgEquiv.symm (IntermediateField.equivOfEq h) = IntermediateField.equivOfEq (_ : T = S)

source

@[simp]

theorem IntermediateField.equivOfEq_rfl {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) :

IntermediateField.equivOfEq (_ : S = S) = AlgEquiv.refl

source

@[simp]

theorem IntermediateField.equivOfEq_trans {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} {U : IntermediateField F E} (hST : S = T) (hTU : T = U) :

AlgEquiv.trans (IntermediateField.equivOfEq hST) (IntermediateField.equivOfEq hTU) = IntermediateField.equivOfEq (_ : S = U)

source

noncomputable def IntermediateField.botEquiv (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :

{ x // x ∈ ⊥ } ≃ₐ[F] F

The bottom intermediate_field is isomorphic to the field.

Instances For

source

theorem IntermediateField.botEquiv_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :

↑(IntermediateField.botEquiv F E) (↑(algebraMap F { x // x ∈ ⊥ }) x) = x

source

@[simp]

theorem IntermediateField.botEquiv_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :

↑(AlgEquiv.symm (IntermediateField.botEquiv F E)) x = ↑(algebraMap F { x // x ∈ ⊥ }) x

source

noncomputable instance IntermediateField.algebraOverBot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Algebra { x // x ∈ ⊥ } F

source

theorem IntermediateField.coe_algebraMap_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↑(algebraMap { x // x ∈ ⊥ } F) = ↑(IntermediateField.botEquiv F E)

source

instance IntermediateField.isScalarTower_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IsScalarTower { x // x ∈ ⊥ } F E

source

@[simp]

theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

∀ (a : E), ↑(↑(AlgEquiv.symm IntermediateField.topEquiv) a) = ↑(↑(MulEquiv.symm ↑↑Subalgebra.topEquiv) a)

source

@[simp]

theorem IntermediateField.topEquiv_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

∀ (a : { x // x ∈ ⊤.toSubalgebra }), ↑IntermediateField.topEquiv a = ↑a

source

def IntermediateField.topEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

{ x // x ∈ ⊤ } ≃ₐ[F] E

The top IntermediateField is isomorphic to the field.

This is the intermediate field version of Subalgebra.topEquiv.

Instances For

source

@[simp]

theorem IntermediateField.restrictScalars_bot_eq_self {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

IntermediateField.restrictScalars F ⊥ = K

source

@[simp]

theorem IntermediateField.restrictScalars_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] :

IntermediateField.restrictScalars K ⊤ = ⊤

source

theorem IntermediateField.AlgHom.fieldRange_eq_map {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E →ₐ[F] K) :

AlgHom.fieldRange f = IntermediateField.map f ⊤

source

theorem IntermediateField.AlgHom.map_fieldRange {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra F K] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :

IntermediateField.map g (AlgHom.fieldRange f) = AlgHom.fieldRange (AlgHom.comp g f)

source

theorem IntermediateField.AlgHom.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {f : E →ₐ[F] K} :

AlgHom.fieldRange f = ⊤ ↔ Function.Surjective ↑f

source

@[simp]

theorem IntermediateField.AlgEquiv.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E ≃ₐ[F] K) :

AlgHom.fieldRange ↑f = ⊤

source

theorem IntermediateField.adjoin_eq_range_algebraMap_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

↑(IntermediateField.adjoin F S) = Set.range ↑(algebraMap { x // x ∈ IntermediateField.adjoin F S } E)

source

theorem IntermediateField.adjoin.algebraMap_mem (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : F) :

↑(algebraMap F E) x ∈ IntermediateField.adjoin F S

source

theorem IntermediateField.adjoin.range_algebraMap_subset (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

Set.range ↑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F S)

source

instance IntermediateField.adjoin.fieldCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

CoeTC F { x // x ∈ IntermediateField.adjoin F S }

source

theorem IntermediateField.subset_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

S ⊆ ↑(IntermediateField.adjoin F S)

source

instance IntermediateField.adjoin.setCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

CoeTC ↑S { x // x ∈ IntermediateField.adjoin F S }

source

theorem IntermediateField.adjoin.mono (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (T : Set E) (h : S ⊆ T) :

IntermediateField.adjoin F S ≤ IntermediateField.adjoin F T

source

theorem IntermediateField.adjoin_contains_field_as_subfield {E : Type u_2} [Field E] (S : Set E) (F : Subfield E) :

↑F ⊆ ↑(IntermediateField.adjoin { x // x ∈ F } S)

source

theorem IntermediateField.subset_adjoin_of_subset_left {E : Type u_2} [Field E] (S : Set E) {F : Subfield E} {T : Set E} (HT : T ⊆ ↑F) :

T ⊆ ↑(IntermediateField.adjoin { x // x ∈ F } S)

source

theorem IntermediateField.subset_adjoin_of_subset_right (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {T : Set E} (H : T ⊆ S) :

T ⊆ ↑(IntermediateField.adjoin F S)

source

@[simp]

theorem IntermediateField.adjoin_empty (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :

F⟮⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_univ (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :

IntermediateField.adjoin F Set.univ = ⊤

source

theorem IntermediateField.adjoin_le_subfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {K : Subfield E} (HF : Set.range ↑(algebraMap F E) ⊆ ↑K) (HS : S ⊆ ↑K) :

IntermediateField.toSubfield (IntermediateField.adjoin F S) ≤ K

If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.

source

theorem IntermediateField.adjoin_subset_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {F' : Type u_3} [Field F'] [Algebra F' E] {S : Set E} {S' : Set E} :

↑(IntermediateField.adjoin F S) ⊆ ↑(IntermediateField.adjoin F' S') ↔ Set.range ↑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F' S') ∧ S ⊆ ↑(IntermediateField.adjoin F' S')

source

theorem IntermediateField.adjoin_adjoin_left (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (T : Set E) :

IntermediateField.restrictScalars F (IntermediateField.adjoin { x // x ∈ IntermediateField.adjoin F S } T) = IntermediateField.adjoin F (S ∪ T)

F[S][T] = F[S ∪ T]

source

@[simp]

theorem IntermediateField.adjoin_insert_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : E) :

IntermediateField.adjoin F (insert x ↑(IntermediateField.adjoin F S)) = IntermediateField.adjoin F (insert x S)

source

theorem IntermediateField.adjoin_adjoin_comm (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (T : Set E) :

IntermediateField.restrictScalars F (IntermediateField.adjoin { x // x ∈ IntermediateField.adjoin F S } T) = IntermediateField.restrictScalars F (IntermediateField.adjoin { x // x ∈ IntermediateField.adjoin F T } S)

F[S][T] = F[T][S]

source

theorem IntermediateField.adjoin_map (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {E' : Type u_3} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') :

IntermediateField.map f (IntermediateField.adjoin F S) = IntermediateField.adjoin F (↑f '' S)

source

theorem IntermediateField.algebra_adjoin_le_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

Algebra.adjoin F S ≤ (IntermediateField.adjoin F S).toSubalgebra

source

theorem IntermediateField.adjoin_eq_algebra_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (inv_mem : ∀ (x : E), x ∈ Algebra.adjoin F S → x⁻¹ ∈ Algebra.adjoin F S) :

(IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S

source

theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (K : IntermediateField F E) (h : K.toSubalgebra = Algebra.adjoin F S) :

K = IntermediateField.adjoin F S

source

theorem IntermediateField.adjoin_induction (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {s : Set E} {p : E → Prop} {x : E} (h : x ∈ IntermediateField.adjoin F s) (Hs : (x : E) → x ∈ s → p x) (Hmap : (x : F) → p (↑(algebraMap F E) x)) (Hadd : (x y : E) → p x → p y → p (x + y)) (Hneg : (x : E) → p x → p (-x)) (Hinv : (x : E) → p x → p x⁻¹) (Hmul : (x y : E) → p x → p y → p (x * y)) :

p x

source

def IntermediateField.«term_⟮_,,⟯» :

Lean.TrailingParserDescr

If x₁ x₂ ... xₙ : E then F⟮x₁,x₂,...,xₙ⟯ is the IntermediateField F E generated by these elements.

Instances For

source

def IntermediateField.delabAdjoinNotation :

Lean.PrettyPrinter.Delaborator.Delab

Instances For

source

partial def IntermediateField.delabAdjoinNotation.delabInsertArray :

Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Term)

source

theorem IntermediateField.mem_adjoin_simple_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

α ∈ F⟮α⟯

source

def IntermediateField.AdjoinSimple.gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

{ x // x ∈ F⟮α⟯ }

generator of F⟮α⟯

Instances For

source

@[simp]

theorem IntermediateField.AdjoinSimple.algebraMap_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

↑(algebraMap { x // x ∈ F⟮α⟯ } E) (IntermediateField.AdjoinSimple.gen F α) = α

source

@[simp]

theorem IntermediateField.AdjoinSimple.isIntegral_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

IsIntegral F (IntermediateField.AdjoinSimple.gen F α) ↔ IsIntegral F α

source

theorem IntermediateField.adjoin_simple_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (β : E) :

IntermediateField.restrictScalars F { x // x ∈ F⟮α⟯ }⟮β⟯ = F⟮α, β⟯

source

theorem IntermediateField.adjoin_simple_comm (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (β : E) :

IntermediateField.restrictScalars F { x // x ∈ F⟮α⟯ }⟮β⟯ = IntermediateField.restrictScalars F { x // x ∈ F⟮β⟯ }⟮α⟯

source

theorem IntermediateField.adjoin_algebraic_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (hS : ∀ (x : E), x ∈ S → IsAlgebraic F x) :

(IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S

source

theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (hα : IsIntegral F α) :

F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}

source

theorem IntermediateField.isSplittingField_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} {K : IntermediateField F E} :

Polynomial.IsSplittingField F { x // x ∈ K } p ↔ Polynomial.Splits (algebraMap F { x // x ∈ K }) p ∧ K = IntermediateField.adjoin F (Polynomial.rootSet p E)

source

theorem IntermediateField.adjoin_rootSet_isSplittingField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} (hp : Polynomial.Splits (algebraMap F E) p) :

Polynomial.IsSplittingField F { x // x ∈ IntermediateField.adjoin F (Polynomial.rootSet p E) } p

source

theorem IntermediateField.isSplittingField_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {t : ι → IntermediateField F E} {p : ι → Polynomial F} {s : Finset ι} (h0 : (Finset.prod s fun i => p i) ≠ 0) (h : ∀ (i : ι), i ∈ s → Polynomial.IsSplittingField F { x // x ∈ t i } (p i)) :

Polynomial.IsSplittingField F { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), t i } (Finset.prod s fun i => p i)

A compositum of splitting fields is a splitting field

source

theorem IntermediateField.adjoin_simple_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : IntermediateField F E} :

F⟮α⟯ ≤ K ↔ α ∈ K

source

theorem IntermediateField.adjoin_simple_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : E) :

CompleteLattice.IsCompactElement F⟮x⟯

Adjoining a single element is compact in the lattice of intermediate fields.

source

theorem IntermediateField.adjoin_finset_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Finset E) :

CompleteLattice.IsCompactElement (IntermediateField.adjoin F ↑S)

Adjoining a finite subset is compact in the lattice of intermediate fields.

source

theorem IntermediateField.adjoin_finite_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (h : Set.Finite S) :

CompleteLattice.IsCompactElement (IntermediateField.adjoin F S)

Adjoining a finite subset is compact in the lattice of intermediate fields.

source

instance IntermediateField.instIsCompactlyGeneratedIntermediateFieldInstCompleteLatticeIntermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IsCompactlyGenerated (IntermediateField F E)

The lattice of intermediate fields is compactly generated.

source

theorem IntermediateField.exists_finset_of_mem_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ (i : ι), f i) :

∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i

source

theorem IntermediateField.exists_finset_of_mem_supr' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ (i : ι), f i) :

∃ s, x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), F⟮↑i.snd⟯

source

theorem IntermediateField.exists_finset_of_mem_supr'' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} (h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }) {x : E} (hx : x ∈ ⨆ (i : ι), f i) :

∃ s, x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), IntermediateField.adjoin F (Polynomial.rootSet (minpoly F i.snd) E)

source

@[simp]

theorem IntermediateField.adjoin_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :

IntermediateField.adjoin F S = ⊥ ↔ S ⊆ ↑⊥

source

theorem IntermediateField.adjoin_simple_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :

F⟮α⟯ = ⊥ ↔ α ∈ ⊥

source

@[simp]

theorem IntermediateField.adjoin_zero {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

F⟮0⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

F⟮1⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_int {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℤ) :

F⟮↑n⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_nat {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℕ) :

F⟮↑n⟯ = ⊥

source

@[simp]

theorem IntermediateField.rank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :

Module.rank F { x // x ∈ K } = 1 ↔ K = ⊥

source

@[simp]

theorem IntermediateField.finrank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :

FiniteDimensional.finrank F { x // x ∈ K } = 1 ↔ K = ⊥

source

@[simp]

theorem IntermediateField.rank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Module.rank F { x // x ∈ ⊥ } = 1

source

@[simp]

theorem IntermediateField.finrank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

FiniteDimensional.finrank F { x // x ∈ ⊥ } = 1

source

theorem IntermediateField.rank_adjoin_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :

Module.rank F { x // x ∈ IntermediateField.adjoin F S } = 1 ↔ S ⊆ ↑⊥

source

theorem IntermediateField.rank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :

Module.rank F { x // x ∈ F⟮α⟯ } = 1 ↔ α ∈ ⊥

source

theorem IntermediateField.finrank_adjoin_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :

FiniteDimensional.finrank F { x // x ∈ IntermediateField.adjoin F S } = 1 ↔ S ⊆ ↑⊥

source

theorem IntermediateField.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :

FiniteDimensional.finrank F { x // x ∈ F⟮α⟯ } = 1 ↔ α ∈ ⊥

source

theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1) :

⊥ = ⊤

If F⟮x⟯ has dimension 1 over F for every x ∈ E then F = E.

source

theorem IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), FiniteDimensional.finrank F { x_1 // x_1 ∈ F⟮x⟯ } = 1) :

⊥ = ⊤

source

theorem IntermediateField.subsingleton_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1) :

Subsingleton (IntermediateField F E)

source

theorem IntermediateField.subsingleton_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), FiniteDimensional.finrank F { x_1 // x_1 ∈ F⟮x⟯ } = 1) :

Subsingleton (IntermediateField F E)

source

theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), FiniteDimensional.finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1) :

⊥ = ⊤

If F⟮x⟯ has dimension ≤1 over F for every x ∈ E then F = E.

source

theorem IntermediateField.subsingleton_of_finrank_adjoin_le_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), FiniteDimensional.finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1) :

Subsingleton (IntermediateField F E)

source

theorem IntermediateField.minpoly_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

minpoly F (IntermediateField.AdjoinSimple.gen F α) = minpoly F α

source

theorem IntermediateField.aeval_gen_minpoly (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

↑(Polynomial.aeval (IntermediateField.AdjoinSimple.gen F α)) (minpoly F α) = 0

source

noncomputable def IntermediateField.adjoinRootEquivAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :

AdjoinRoot (minpoly F α) ≃ₐ[F] { x // x ∈ F⟮α⟯ }

algebra isomorphism between AdjoinRoot and F⟮α⟯

Instances For

source

theorem IntermediateField.adjoinRootEquivAdjoin_apply_root (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :

↑(IntermediateField.adjoinRootEquivAdjoin F h) (AdjoinRoot.root (minpoly F α)) = IntermediateField.AdjoinSimple.gen F α

source

noncomputable def IntermediateField.powerBasisAux {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

Basis (Fin (Polynomial.natDegree (minpoly K x))) K { x // x ∈ K⟮x⟯ }

The elements 1, x, ..., x ^ (d - 1) form a basis for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Instances For

source

@[simp]

theorem IntermediateField.adjoin.powerBasis_gen {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

(IntermediateField.adjoin.powerBasis hx).gen = IntermediateField.AdjoinSimple.gen K x

source

@[simp]

theorem IntermediateField.adjoin.powerBasis_dim {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

(IntermediateField.adjoin.powerBasis hx).dim = Polynomial.natDegree (minpoly K x)

source

noncomputable def IntermediateField.adjoin.powerBasis {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

PowerBasis K { x // x ∈ K⟮x⟯ }

The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Instances For

source

theorem IntermediateField.adjoin.finiteDimensional {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

FiniteDimensional K { x // x ∈ K⟮x⟯ }

source

theorem IntermediateField.adjoin.finrank {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :

FiniteDimensional.finrank K { x // x ∈ K⟮x⟯ } = Polynomial.natDegree (minpoly K x)

source

theorem minpoly.natDegree_le {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :

Polynomial.natDegree (minpoly K x) ≤ FiniteDimensional.finrank K L

source

theorem minpoly.degree_le {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :

Polynomial.degree (minpoly K x) ≤ ↑(FiniteDimensional.finrank K L)

source

noncomputable def IntermediateField.algHomAdjoinIntegralEquiv (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u_3} [Field K] [Algebra F K] (h : IsIntegral F α) :

({ x // x ∈ F⟮α⟯ } →ₐ[F] K) ≃ { x // x ∈ Polynomial.aroots (minpoly F α) K }

Algebra homomorphism F⟮α⟯ →ₐ[F] K are in bijection with the set of roots of minpoly α in K.

Instances For

source

noncomputable def IntermediateField.fintypeOfAlgHomAdjoinIntegral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u_3} [Field K] [Algebra F K] (h : IsIntegral F α) :

Fintype ({ x // x ∈ F⟮α⟯ } →ₐ[F] K)

Fintype of algebra homomorphism F⟮α⟯ →ₐ[F] K

Instances For

source

theorem IntermediateField.card_algHom_adjoin_integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u_3} [Field K] [Algebra F K] (h : IsIntegral F α) (h_sep : Polynomial.Separable (minpoly F α)) (h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)) :

Fintype.card ({ x // x ∈ F⟮α⟯ } →ₐ[F] K) = Polynomial.natDegree (minpoly F α)

source

def IntermediateField.FG {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) :

Prop

An intermediate field S is finitely generated if there exists t : Finset E such that IntermediateField.adjoin F t = S.

Instances For

source

theorem IntermediateField.fg_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (t : Finset E) :

IntermediateField.FG (IntermediateField.adjoin F ↑t)

source

theorem IntermediateField.fg_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} :

IntermediateField.FG S ↔ ∃ t, Set.Finite t ∧ IntermediateField.adjoin F t = S

source

theorem IntermediateField.fg_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IntermediateField.FG ⊥

source

theorem IntermediateField.fG_of_fG_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (h : Subalgebra.FG S.toSubalgebra) :

IntermediateField.FG S

source

theorem IntermediateField.fg_of_noetherian {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) [IsNoetherian F E] :

IntermediateField.FG S

source

theorem IntermediateField.induction_on_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥) (ih : (K : IntermediateField F E) → (x : E) → x ∈ S → P K → P (IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯)) :

P (IntermediateField.adjoin F ↑S)

source

theorem IntermediateField.induction_on_adjoin_fg {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : IntermediateField F E → Prop) (base : P ⊥) (ih : (K : IntermediateField F E) → (x : E) → P K → P (IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯)) (K : IntermediateField F E) (hK : IntermediateField.FG K) :

P K

source

theorem IntermediateField.induction_on_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (P : IntermediateField F E → Prop) (base : P ⊥) (ih : (K : IntermediateField F E) → (x : E) → P K → P (IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯)) (K : IntermediateField F E) :

P K

source

def IntermediateField.Lifts (F : Type u_1) (E : Type u_2) (K : Type u_3) [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] :

Type (max u_2 u_3 u_2)

Lifts L → K of F → K

Instances For

source

instance IntermediateField.instPartialOrderLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] :

PartialOrder (IntermediateField.Lifts F E K)

source

noncomputable instance IntermediateField.instOrderBotLiftsToLEToPreorderInstPartialOrderLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] :

OrderBot (IntermediateField.Lifts F E K)

source

noncomputable instance IntermediateField.instInhabitedLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] :

Inhabited (IntermediateField.Lifts F E K)

source

theorem IntermediateField.Lifts.eq_of_le {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {x : IntermediateField.Lifts F E K} {y : IntermediateField.Lifts F E K} (hxy : x ≤ y) (s : { x // x ∈ x.fst }) :

↑x.snd s = ↑y.snd { val := ↑s, property := (_ : ↑s ∈ y.fst) }

source

theorem IntermediateField.Lifts.exists_max_two {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {c : Set (IntermediateField.Lifts F E K)} {x : IntermediateField.Lifts F E K} {y : IntermediateField.Lifts F E K} (hc : IsChain (fun x x_1 => x ≤ x_1) c) (hx : x ∈ insert ⊥ c) (hy : y ∈ insert ⊥ c) :

∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z

source

theorem IntermediateField.Lifts.exists_max_three {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {c : Set (IntermediateField.Lifts F E K)} {x : IntermediateField.Lifts F E K} {y : IntermediateField.Lifts F E K} {z : IntermediateField.Lifts F E K} (hc : IsChain (fun x x_1 => x ≤ x_1) c) (hx : x ∈ insert ⊥ c) (hy : y ∈ insert ⊥ c) (hz : z ∈ insert ⊥ c) :

∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w

source

def IntermediateField.Lifts.upperBoundIntermediateField {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {c : Set (IntermediateField.Lifts F E K)} (hc : IsChain (fun x x_1 => x ≤ x_1) c) :

IntermediateField F E

An upper bound on a chain of lifts

Instances For

source

noncomputable def IntermediateField.Lifts.upperBoundAlgHom {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {c : Set (IntermediateField.Lifts F E K)} (hc : IsChain (fun x x_1 => x ≤ x_1) c) :

{ x // x ∈ IntermediateField.Lifts.upperBoundIntermediateField hc } →ₐ[F] K

The lift on the upper bound on a chain of lifts

Instances For

source

noncomputable def IntermediateField.Lifts.upperBound {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {c : Set (IntermediateField.Lifts F E K)} (hc : IsChain (fun x x_1 => x ≤ x_1) c) :

IntermediateField.Lifts F E K

An upper bound on a chain of lifts

Instances For

source

theorem IntermediateField.Lifts.exists_upper_bound {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (c : Set (IntermediateField.Lifts F E K)) (hc : IsChain (fun x x_1 => x ≤ x_1) c) :

∃ ub, ∀ (a : IntermediateField.Lifts F E K), a ∈ c → a ≤ ub

source

noncomputable def IntermediateField.Lifts.liftOfSplits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)) :

IntermediateField.Lifts F E K

Extend a lift x : Lifts F E K to an element s : E whose conjugates are all in K

Instances For

source

theorem IntermediateField.Lifts.le_lifts_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)) :

x ≤ IntermediateField.Lifts.liftOfSplits x h1 h2

source

theorem IntermediateField.Lifts.mem_lifts_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)) :

s ∈ (IntermediateField.Lifts.liftOfSplits x h1 h2).fst

source

theorem IntermediateField.Lifts.exists_lift_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)) :

∃ y, x ≤ y ∧ s ∈ y.fst

source

theorem IntermediateField.algHom_mk_adjoin_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) :

Nonempty ({ x // x ∈ IntermediateField.adjoin F S } →ₐ[F] K)

source

theorem IntermediateField.algHom_mk_adjoin_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ⊤) (hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)) :

Nonempty (E →ₐ[F] K)

source

theorem IntermediateField.le_sup_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) :

E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra

source

theorem IntermediateField.sup_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [h1 : FiniteDimensional K { x // x ∈ E1 }] [h2 : FiniteDimensional K { x // x ∈ E2 }] :

(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

source

instance IntermediateField.finiteDimensional_sup {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [h1 : FiniteDimensional K { x // x ∈ E1 }] [h2 : FiniteDimensional K { x // x ∈ E2 }] :

FiniteDimensional K { x // x ∈ E1 ⊔ E2 }

source

instance IntermediateField.finiteDimensional_iSup_of_finite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {t : ι → IntermediateField K L} [h : Finite ι] [∀ (i : ι), FiniteDimensional K { x // x ∈ t i }] :

FiniteDimensional K { x // x ∈ ⨆ (i : ι), t i }

source

instance IntermediateField.finiteDimensional_iSup_of_finset {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {f : ι → IntermediateField K L} {s : Finset ι} [h : ∀ (i : ι), FiniteDimensional K { x // x ∈ f i }] :

FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }

source

theorem IntermediateField.finiteDimensional_iSup_of_finset' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {f : ι → IntermediateField K L} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }) :

FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }

source

theorem IntermediateField.isAlgebraic_iSup {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {f : ι → IntermediateField K L} (h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }) :

Algebra.IsAlgebraic K { x // x ∈ ⨆ (i : ι), f i }

A compositum of algebraic extensions is algebraic

source

noncomputable def PowerBasis.equivAdjoinSimple {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :

{ x // x ∈ K⟮pb.gen⟯ } ≃ₐ[K] L

pb.equivAdjoinSimple is the equivalence between K⟮pb.gen⟯ and L itself.

Instances For

source

@[simp]

theorem PowerBasis.equivAdjoinSimple_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :

↑(PowerBasis.equivAdjoinSimple pb) (↑(Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) = ↑(Polynomial.aeval pb.gen) f

source

@[simp]

theorem PowerBasis.equivAdjoinSimple_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :

↑(PowerBasis.equivAdjoinSimple pb) (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen

source

@[simp]

theorem PowerBasis.equivAdjoinSimple_symm_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :

↑(AlgEquiv.symm (PowerBasis.equivAdjoinSimple pb)) (↑(Polynomial.aeval pb.gen) f) = ↑(Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f

source

@[simp]

theorem PowerBasis.equivAdjoinSimple_symm_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :

↑(AlgEquiv.symm (PowerBasis.equivAdjoinSimple pb)) pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen