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 (in scope IntermediateField).

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.

Equations

• IntermediateField.adjoin F S = { toSubsemiring := (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)).toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

theorem IntermediateField.mem_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (x : E) : x ∈ IntermediateField.adjoin F S ↔ ∃ (r : MvPolynomial (↑S) F) (s : MvPolynomial (↑S) F), x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s

theorem IntermediateField.mem_adjoin_simple_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (x : E) : x ∈ F⟮α⟯ ↔ ∃ (r : Polynomial F) (s : Polynomial F), x = (Polynomial.aeval α) r / (Polynomial.aeval α) s

@[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

theorem IntermediateField.gc {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : GaloisConnection (IntermediateField.adjoin F) fun (x : IntermediateField F E) => ↑x

def IntermediateField.gi {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : GaloisInsertion (IntermediateField.adjoin F) fun (x : IntermediateField F E) => ↑x

Galois insertion between adjoin and coe.

Equations

• IntermediateField.gi = { choice := fun (s : Set E) (hs : ↑(IntermediateField.adjoin F s) ≤ s) => (IntermediateField.adjoin F s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

instance IntermediateField.instCompleteLattice {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : CompleteLattice (IntermediateField F E)

Equations

• IntermediateField.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance IntermediateField.instInhabited {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Inhabited (IntermediateField F E)

Equations

• IntermediateField.instInhabited = { default := ⊤ }

instance IntermediateField.instUnique {F : Type u_1} [Field F] : Unique (IntermediateField F F)

Equations

• IntermediateField.instUnique = { toInhabited := inferInstanceAs (Inhabited (IntermediateField F F)), uniq := ⋯ }

theorem IntermediateField.coe_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ↑⊥ = Set.range ⇑(algebraMap F E)

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)

@[simp]

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

@[simp]

theorem IntermediateField.coe_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ↑⊤ = Set.univ

@[simp]

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

@[simp]

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

@[simp]

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

@[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

@[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

@[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

@[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) : (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield

@[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 : IntermediateField F E) => ↑x) '' S)

@[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)

@[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)) : (sInf S).toSubfield = sInf (IntermediateField.toSubfield '' S)

@[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)

@[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

@[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) : (iInf S).toSubfield = ⨅ (i : ι), (S i).toSubfield

@[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 : ↥S.toSubalgebra) : (IntermediateField.equivOfEq h) x = ⟨↑x, ⋯⟩

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) : ↥S ≃ₐ[F] ↥T

Construct an algebra isomorphism from an equality of intermediate fields

Equations

• IntermediateField.equivOfEq h = S.equivOfEq T.toSubalgebra ⋯

@[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) : (IntermediateField.equivOfEq h).symm = IntermediateField.equivOfEq ⋯

@[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 ⋯ = AlgEquiv.refl

@[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) : (IntermediateField.equivOfEq hST).trans (IntermediateField.equivOfEq hTU) = IntermediateField.equivOfEq ⋯

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

The bottom intermediate_field is isomorphic to the field.

Equations

• IntermediateField.botEquiv F E = (⊥.equivOfEq ⊥ ⋯).trans (Algebra.botEquiv F E)

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

@[simp]

theorem IntermediateField.botEquiv_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) : (IntermediateField.botEquiv F E).symm x = (algebraMap F ↥⊥) x

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

Equations

• IntermediateField.algebraOverBot = (↑(IntermediateField.botEquiv F E)).toAlgebra

theorem IntermediateField.coe_algebraMap_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ⇑(algebraMap (↥⊥) F) = ⇑(IntermediateField.botEquiv F E)

instance IntermediateField.isScalarTower_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : IsScalarTower (↥⊥) F E

Equations

• ⋯ = ⋯

@[simp]

theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ∀ (a : E), ↑(IntermediateField.topEquiv.symm a) = ↑((↑↑Subalgebra.topEquiv).symm a)

@[simp]

theorem IntermediateField.topEquiv_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ∀ (a : ↥⊤.toSubalgebra), IntermediateField.topEquiv a = ↑a

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

The top IntermediateField is isomorphic to the field.

This is the intermediate field version of Subalgebra.topEquiv.

Equations

• IntermediateField.topEquiv = (⊤.equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv

@[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

@[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 ⊤ = ⊤

@[simp]

theorem IntermediateField.map_bot {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) : IntermediateField.map f ⊥ = ⊥

theorem IntermediateField.map_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (s : IntermediateField F E) (t : IntermediateField F E) (f : E →ₐ[F] K) : IntermediateField.map f (s ⊔ t) = IntermediateField.map f s ⊔ IntermediateField.map f t

theorem IntermediateField.map_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {ι : Sort u_4} (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : IntermediateField.map f (iSup s) = ⨆ (i : ι), IntermediateField.map f (s i)

theorem IntermediateField.map_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (s : IntermediateField F E) (t : IntermediateField F E) (f : E →ₐ[F] K) : IntermediateField.map f (s ⊓ t) = IntermediateField.map f s ⊓ IntermediateField.map f t

theorem IntermediateField.map_iInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {ι : Sort u_4} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : IntermediateField.map f (iInf s) = ⨅ (i : ι), IntermediateField.map f (s i)

theorem 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) : f.fieldRange = IntermediateField.map f ⊤

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

theorem 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} : f.fieldRange = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem 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) : (↑f).fieldRange = ⊤

theorem IntermediateField.fieldRange_comp_val {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) : (f.comp L.val).fieldRange = IntermediateField.map f L

noncomputable def IntermediateField.equivMap {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) : ↥L ≃ₐ[F] ↥(IntermediateField.map f L)

An intermediate field is isomorphic to its image under an AlgHom (which is automatically injective)

Equations

• L.equivMap f = (AlgEquiv.ofInjective (f.comp L.val) ⋯).trans (IntermediateField.equivOfEq ⋯)

@[simp]

theorem IntermediateField.coe_equivMap_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) (x : ↥L) : ↑((L.equivMap f) x) = f ↑x

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 (↥(IntermediateField.adjoin F S)) E)

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

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)

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

Equations

• IntermediateField.adjoin.fieldCoe F S = { coe := fun (x : F) => ⟨(algebraMap F E) x, ⋯⟩ }

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)

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

Equations

• IntermediateField.adjoin.setCoe F S = { coe := fun (x : ↑S) => ⟨↑x, ⋯⟩ }

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

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

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 (↥F) S)

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)

@[simp]

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

@[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 = ⊤

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.adjoin F S).toSubfield ≤ K

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

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')

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 (↥(IntermediateField.adjoin F S)) T) = IntermediateField.adjoin F (S ∪ T)

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

@[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)

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 (↥(IntermediateField.adjoin F S)) T) = IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F T)) S)

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

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)

@[simp]

theorem IntermediateField.lift_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set ↥K) : IntermediateField.lift (IntermediateField.adjoin F S) = IntermediateField.adjoin F (Subtype.val '' S)

theorem IntermediateField.lift_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (α : ↥K) : IntermediateField.lift F⟮α⟯ = F⟮↑α⟯

@[simp]

theorem IntermediateField.lift_bot (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) : IntermediateField.lift ⊥ = ⊥

@[simp]

theorem IntermediateField.lift_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) : IntermediateField.lift ⊤ = K

@[simp]

theorem IntermediateField.adjoin_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) : IntermediateField.adjoin F ↑K = K

theorem IntermediateField.restrictScalars_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set E) : IntermediateField.restrictScalars F (IntermediateField.adjoin (↥K) S) = IntermediateField.adjoin F (↑K ∪ S)

theorem IntermediateField.extendScalars_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} {S : Set E} (h : K ≤ IntermediateField.adjoin F S) : IntermediateField.extendScalars h = IntermediateField.adjoin (↥K) S

theorem IntermediateField.restrictScalars_adjoin_of_algEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {L : Type u_3} {L' : Type u_4} [Field L] [Field L'] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i) (S : Set E) : IntermediateField.restrictScalars F (IntermediateField.adjoin L S) = IntermediateField.restrictScalars F (IntermediateField.adjoin L' S)

If E / L / F and E / L' / F are two field extension towers, L ≃ₐ[F] L' is an isomorphism compatible with E / L and E / L', then for any subset S of E, L(S) and L'(S) are equal as intermediate fields of E / F.

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

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 ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) : (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S

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

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

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) (mem : ∀ x ∈ s, p x) (algebraMap : ∀ (x : F), p ((_root_.algebraMap F E) x)) (add : ∀ (x y : E), p x → p y → p (x + y)) (neg : ∀ (x : E), p x → p (-x)) (inv : ∀ (x : E), p x → p x⁻¹) (mul : ∀ (x y : E), p x → p y → p (x * y)) : p x

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

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

Equations

• One or more equations did not get rendered due to their size.

def IntermediateField.delabAdjoinNotation : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

partial def IntermediateField.delabAdjoinNotation.delabInsertArray : Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Term)

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

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

generator of F⟮α⟯

Equations

• IntermediateField.AdjoinSimple.gen F α = ⟨α, ⋯⟩

@[simp]

theorem IntermediateField.AdjoinSimple.coe_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) : ↑(IntermediateField.AdjoinSimple.gen F α) = α

theorem IntermediateField.AdjoinSimple.algebraMap_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) : (algebraMap (↥F⟮α⟯) E) (IntermediateField.AdjoinSimple.gen F α) = α

@[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 α

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 (↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯

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 (↥F⟮α⟯)⟮β⟯ = IntermediateField.restrictScalars F (↥F⟮β⟯)⟮α⟯

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 ∈ S, IsAlgebraic F x) : (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S

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 {α}

theorem isSplittingField_iff_intermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} : Polynomial.IsSplittingField F E p ↔ Polynomial.Splits (algebraMap F E) p ∧ IntermediateField.adjoin F (p.rootSet E) = ⊤

Characterize IsSplittingField with IntermediateField.adjoin instead of Algebra.adjoin.

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 (↥K) p ↔ Polynomial.Splits (algebraMap F ↥K) p ∧ K = IntermediateField.adjoin F (p.rootSet E)

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 (↥(IntermediateField.adjoin F (p.rootSet E))) p

theorem IntermediateField.le_sup_toSubalgebra {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra

theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [Algebra.IsAlgebraic K ↥E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_left {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [Algebra.IsAlgebraic K ↥E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2) : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

The compositum of two intermediate fields is equal to the compositum of them as subalgebras, if one of them is algebraic over the base field.

theorem IntermediateField.sup_toSubalgebra_of_left {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K ↥E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

@[deprecated IntermediateField.sup_toSubalgebra_of_left]

theorem IntermediateField.sup_toSubalgebra {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K ↥E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Alias of IntermediateField.sup_toSubalgebra_of_left.

theorem IntermediateField.sup_toSubalgebra_of_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K ↥E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

instance IntermediateField.finiteDimensional_sup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2] : FiniteDimensional K ↥(E1 ⊔ E2)

Equations

• ⋯ = ⋯

theorem IntermediateField.coe_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} [Nonempty ι] (dir : Directed (fun (x1 x2 : IntermediateField K L) => x1 ≤ x2) t) : ↑(iSup t) = ⋃ (i : ι), ↑(t i)

theorem IntermediateField.toSubalgebra_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} (dir : Directed (fun (x1 x2 : IntermediateField K L) => x1 ≤ x2) t) : (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra

instance IntermediateField.finiteDimensional_iSup_of_finite {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} [h : Finite ι] [∀ (i : ι), FiniteDimensional K ↥(t i)] : FiniteDimensional K ↥(⨆ (i : ι), t i)

Equations

• ⋯ = ⋯

instance IntermediateField.finiteDimensional_iSup_of_finset {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {s : Finset ι} [∀ (i : ι), FiniteDimensional K ↥(t i)] : FiniteDimensional K ↥(⨆ i ∈ s, t i)

Equations

• ⋯ = ⋯

theorem IntermediateField.finiteDimensional_iSup_of_finset' {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {s : Finset ι} (h : ∀ i ∈ s, FiniteDimensional K ↥(t i)) : FiniteDimensional K ↥(⨆ i ∈ s, t i)

theorem IntermediateField.isSplittingField_iSup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {p : ι → Polynomial K} {s : Finset ι} (h0 : ∏ i ∈ s, p i ≠ 0) (h : ∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)) : Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

A compositum of splitting fields is a splitting field

theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L) : (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

If K / E / F is a field extension tower, L is an intermediate field of K / F, such that either E / F or L / F is algebraic, then E(L) = E[L].

theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] : (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F ↥L] : (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

theorem IntermediateField.adjoin_rank_le_of_isAlgebraic {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L) : Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L

If K / E / F is a field extension tower, L is an intermediate field of K / F, such that either E / F or L / F is algebraic, then [E(L) : E] ≤ [L : F]. A corollary of Subalgebra.adjoin_rank_le since in this case E(L) = E[L].

theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_left {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] : Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L

theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_right {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F ↥L] : Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L

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

theorem IntermediateField.biSup_adjoin_simple {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) : ⨆ x ∈ S, F⟮x⟯ = IntermediateField.adjoin F S

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.

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.

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

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

instance IntermediateField.instIsCompactlyGenerated {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.

Equations

• ⋯ = ⋯

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 : Finset ι), x ∈ ⨆ i ∈ s, f i

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 : Finset ((i : ι) × ↥(f i))), x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯

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 ↥(f i)) {x : E} (hx : x ∈ ⨆ (i : ι), f i) : ∃ (s : Finset ((i : ι) × ↥(f i))), x ∈ ⨆ i ∈ s, IntermediateField.adjoin F ((minpoly F i.snd).rootSet E)

theorem IntermediateField.exists_finset_of_mem_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {x : E} (hx : x ∈ IntermediateField.adjoin F S) : ∃ (T : Finset E), ↑T ⊆ S ∧ x ∈ IntermediateField.adjoin F ↑T

@[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 ⊆ ↑⊥

theorem IntermediateField.adjoin_simple_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} : F⟮α⟯ = ⊥ ↔ α ∈ ⊥

@[simp]

theorem IntermediateField.adjoin_zero {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : F⟮0⟯ = ⊥

@[simp]

theorem IntermediateField.adjoin_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : F⟮1⟯ = ⊥

@[simp]

theorem IntermediateField.adjoin_intCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℤ) : F⟮↑n⟯ = ⊥

@[simp]

theorem IntermediateField.adjoin_natCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℕ) : F⟮↑n⟯ = ⊥

@[deprecated IntermediateField.adjoin_intCast]

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

Alias of IntermediateField.adjoin_intCast.

@[deprecated IntermediateField.adjoin_natCast]

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

Alias of IntermediateField.adjoin_natCast.

@[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 ↥K = 1 ↔ K = ⊥

@[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} : Module.finrank F ↥K = 1 ↔ K = ⊥

@[simp]

theorem IntermediateField.rank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.rank F ↥⊥ = 1

@[simp]

theorem IntermediateField.finrank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank F ↥⊥ = 1

@[simp]

theorem IntermediateField.rank_bot' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.rank (↥⊥) E = Module.rank F E

@[simp]

theorem IntermediateField.finrank_bot' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank (↥⊥) E = Module.finrank F E

@[simp]

theorem IntermediateField.rank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.rank (↥⊤) E = 1

@[simp]

theorem IntermediateField.finrank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank (↥⊤) E = 1

@[simp]

theorem IntermediateField.rank_top' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.rank F ↥⊤ = Module.rank F E

@[simp]

theorem IntermediateField.finrank_top' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank F ↥⊤ = Module.finrank F E

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 ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥

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 ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

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} : Module.finrank F ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥

theorem IntermediateField.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} : Module.finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

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 ↥F⟮x⟯ = 1) : ⊥ = ⊤

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

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), Module.finrank F ↥F⟮x⟯ = 1) : ⊥ = ⊤

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 ↥F⟮x⟯ = 1) : Subsingleton (IntermediateField F E)

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), Module.finrank F ↥F⟮x⟯ = 1) : Subsingleton (IntermediateField F E)

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), Module.finrank F ↥F⟮x⟯ ≤ 1) : ⊥ = ⊤

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

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), Module.finrank F ↥F⟮x⟯ ≤ 1) : Subsingleton (IntermediateField F E)

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 α

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

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] ↥F⟮α⟯

algebra isomorphism between AdjoinRoot and F⟮α⟯

Equations

• IntermediateField.adjoinRootEquivAdjoin F h = AlgEquiv.ofBijective (AdjoinRoot.liftHom (minpoly F α) (IntermediateField.AdjoinSimple.gen F α) ⋯) ⋯

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 α

@[simp]

theorem IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) : (IntermediateField.adjoinRootEquivAdjoin F h).symm (IntermediateField.AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)

theorem IntermediateField.adjoin_root_eq_top {K : Type u} [Field K] (p : Polynomial K) [Fact (Irreducible p)] : K⟮AdjoinRoot.root p⟯ = ⊤

noncomputable def IntermediateField.powerBasisAux {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : Basis (Fin (minpoly K x).natDegree) K ↥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.

Equations

• IntermediateField.powerBasisAux hx = (AdjoinRoot.powerBasis ⋯).basis.map (IntermediateField.adjoinRootEquivAdjoin K hx).toLinearEquiv

@[simp]

theorem IntermediateField.adjoin.powerBasis_dim {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : (IntermediateField.adjoin.powerBasis hx).dim = (minpoly K x).natDegree

@[simp]

theorem IntermediateField.adjoin.powerBasis_gen {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : (IntermediateField.adjoin.powerBasis hx).gen = IntermediateField.AdjoinSimple.gen K x

noncomputable def IntermediateField.adjoin.powerBasis {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : PowerBasis K ↥K⟮x⟯

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

Equations

• IntermediateField.adjoin.powerBasis hx = { gen := IntermediateField.AdjoinSimple.gen K x, dim := (minpoly K x).natDegree, basis := IntermediateField.powerBasisAux hx, basis_eq_pow := ⋯ }

theorem IntermediateField.adjoin.finiteDimensional {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : FiniteDimensional K ↥K⟮x⟯

theorem IntermediateField.isAlgebraic_adjoin_simple {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K ↥K⟮x⟯

theorem IntermediateField.adjoin.finrank {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] {S : Set K} (hprim : IntermediateField.adjoin F S = ⊤) : IntermediateField.adjoin E S = ⊤

If K / E / F is a field extension tower, S ⊂ K is such that F(S) = K, then E(S) = K.

theorem IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} [FiniteDimensional F E] (hprim : F⟮α⟯ = ⊤) (K : IntermediateField F E) : IntermediateField.adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K

If E / F is a finite extension such that E = F(α), then for any intermediate field K, the F adjoin the coefficients of minpoly K α is equal to K itself.

instance IntermediateField.instFiniteSubtypeMemBot (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.Finite F ↥⊥

Equations

• ⋯ = ⋯

theorem IntermediateField.exists_lt_finrank_of_infinite_dimensional {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (hnfd : ¬FiniteDimensional F E) (n : ℕ) : ∃ (L : IntermediateField F E), FiniteDimensional F ↥L ∧ n < Module.finrank F ↥L

If E / F is an infinite algebraic extension, then there exists an intermediate field L / F with arbitrarily large finite extension degree.

theorem minpoly.natDegree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ Module.finrank K L

theorem minpoly.degree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] : (minpoly K x).degree ≤ ↑(Module.finrank K L)

theorem minpoly.degree_dvd {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : (minpoly K x).natDegree ∣ Module.finrank K L

If x : L is an integral element in a field extension L over K, then the degree of the minimal polynomial of x over K divides [L : K].

theorem IntermediateField.isAlgebraic_iSup {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {ι : Type u_4} {t : ι → IntermediateField K L} (h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)) : Algebra.IsAlgebraic K ↥(⨆ (i : ι), t i)

A compositum of algebraic extensions is algebraic

theorem IntermediateField.isAlgebraic_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) : Algebra.IsAlgebraic K ↥(IntermediateField.adjoin K S)

theorem IntermediateField.finiteDimensional_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} [Finite ↑S] (hS : ∀ x ∈ S, IsIntegral K x) : FiniteDimensional K ↥(IntermediateField.adjoin K S)

If L / K is a field extension, S is a finite subset of L, such that every element of S is integral (= algebraic) over K, then K(S) / K is a finite extension. A direct corollary of finiteDimensional_iSup_of_finite.

noncomputable def IntermediateField.algHomAdjoinIntegralEquiv (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) : (↥F⟮α⟯ →ₐ[F] K) ≃ { x : K // x ∈ (minpoly F α).aroots K }

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

Equations

• IntermediateField.algHomAdjoinIntegralEquiv F h = (IntermediateField.adjoin.powerBasis h).liftEquiv'.trans ((Equiv.refl K).subtypeEquiv ⋯)

theorem IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (x : { x : K // x ∈ (minpoly F α).aroots K }) : ((IntermediateField.algHomAdjoinIntegralEquiv F h).symm x) (IntermediateField.AdjoinSimple.gen F α) = ↑x

noncomputable def IntermediateField.fintypeOfAlgHomAdjoinIntegral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) : Fintype (↥F⟮α⟯ →ₐ[F] K)

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

Equations

• IntermediateField.fintypeOfAlgHomAdjoinIntegral F h = PowerBasis.AlgHom.fintype (IntermediateField.adjoin.powerBasis h)

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} [Field K] [Algebra F K] (h : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)) : Fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree

theorem Polynomial.irreducible_comp {K : Type u} [Field K] {f : Polynomial K} {g : Polynomial K} (hfm : f.Monic) (hgm : g.Monic) (hf : Irreducible f) (hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) : Irreducible (f.comp g)

Let f, g be monic polynomials over K. If f is irreducible, and g(x) - α is irreducible in K⟮α⟯ with α a root of f, then f(g(x)) is irreducible.

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.

Equations

• S.FG = ∃ (t : Finset E), IntermediateField.adjoin F ↑t = S

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

theorem IntermediateField.fg_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} : S.FG ↔ ∃ (t : Set E), t.Finite ∧ IntermediateField.adjoin F t = S

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

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 : S.FG) : S.FG

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] : S.FG

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 ∈ S, P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) : P (IntermediateField.adjoin F ↑S)

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 (↥K)⟮x⟯)) (K : IntermediateField F E) (hK : K.FG) : P K

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 (↥K)⟮x⟯)) (K : IntermediateField F E) : P K

noncomputable def AdjoinRoot.algHomOfDvd {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : q ∣ p) : AdjoinRoot p →ₐ[K] AdjoinRoot q

The canonical algebraic homomorphism from AdjoinRoot p to AdjoinRoot q, where the polynomial q : K[X] divides p.

Equations

• AdjoinRoot.algHomOfDvd hpq = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯

theorem AdjoinRoot.coe_algHomOfDvd {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : q ∣ p) : (↑↑(AdjoinRoot.algHomOfDvd hpq).toRingHom).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)

theorem AdjoinRoot.algHomOfDvd_apply_root {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : q ∣ p) : (AdjoinRoot.algHomOfDvd hpq) (AdjoinRoot.root p) = AdjoinRoot.root q

algHomOfDvd sends AdjoinRoot.root p to AdjoinRoot.root q.

noncomputable def AdjoinRoot.algEquivOfEq {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (h_eq : p = q) : AdjoinRoot p ≃ₐ[K] AdjoinRoot q

The canonical algebraic equivalence between AdjoinRoot p and AdjoinRoot q, where the two polynomials p q : K[X] are equal.

Equations

• AdjoinRoot.algEquivOfEq hp h_eq = AlgEquiv.ofAlgHom (AdjoinRoot.algHomOfDvd ⋯) (AdjoinRoot.algHomOfDvd ⋯) ⋯ ⋯

theorem AdjoinRoot.coe_algEquivOfEq {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (h_eq : p = q) : (AdjoinRoot.algEquivOfEq hp h_eq).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)

theorem AdjoinRoot.algEquivOfEq_toAlgHom {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (h_eq : p = q) : ↑(AdjoinRoot.algEquivOfEq hp h_eq) = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯

theorem AdjoinRoot.algEquivOfEq_apply_root {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (h_eq : p = q) : (AdjoinRoot.algEquivOfEq hp h_eq) (AdjoinRoot.root p) = AdjoinRoot.root q

algEquivOfEq sends AdjoinRoot.root p to AdjoinRoot.root q.

noncomputable def AdjoinRoot.algEquivOfAssociated {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (hpq : Associated p q) : AdjoinRoot p ≃ₐ[K] AdjoinRoot q

The canonical algebraic equivalence between AdjoinRoot p and AdjoinRoot q, where the two polynomials p q : K[X] are associated.

Equations

• AdjoinRoot.algEquivOfAssociated hp hpq = AlgEquiv.ofAlgHom (AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯) (AdjoinRoot.liftHom q (AdjoinRoot.root p) ⋯) ⋯ ⋯

theorem AdjoinRoot.coe_algEquivOfAssociated {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (hpq : Associated p q) : (AdjoinRoot.algEquivOfAssociated hp hpq).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)

theorem AdjoinRoot.algEquivOfAssociated_toAlgHom {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (hpq : Associated p q) : ↑(AdjoinRoot.algEquivOfAssociated hp hpq) = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯

theorem AdjoinRoot.algEquivOfAssociated_apply_root {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hp : p ≠ 0) (hpq : Associated p q) : (AdjoinRoot.algEquivOfAssociated hp hpq) (AdjoinRoot.root p) = AdjoinRoot.root q

algEquivOfAssociated sends AdjoinRoot.root p to AdjoinRoot.root q.

theorem minpoly.eq_of_root {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {y : L} (hx : IsAlgebraic K x) (h_ev : (Polynomial.aeval y) (minpoly K x) = 0) : minpoly K y = minpoly K x

If y : L is a root of minpoly K x, then minpoly K y = minpoly K x.

noncomputable def minpoly.algEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯

The canonical algEquiv between K⟮x⟯and K⟮y⟯, sending x to y, where x and y have the same minimal polynomial over K.

Equations

• minpoly.algEquiv hx h_mp = (IntermediateField.adjoinRootEquivAdjoin K ⋯).symm.trans ((AdjoinRoot.algEquivOfEq ⋯ h_mp).trans (IntermediateField.adjoinRootEquivAdjoin K ⋯))

theorem minpoly.algEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : (minpoly.algEquiv hx h_mp) (IntermediateField.AdjoinSimple.gen K x) = IntermediateField.AdjoinSimple.gen K y

minpoly.algEquiv sends the generator of K⟮x⟯ to the generator of K⟮y⟯.

noncomputable def PowerBasis.equivAdjoinSimple {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) : ↥K⟮pb.gen⟯ ≃ₐ[K] L

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

Equations

• pb.equivAdjoinSimple = (IntermediateField.adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯

@[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) : pb.equivAdjoinSimple ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) = (Polynomial.aeval pb.gen) f

@[simp]

theorem PowerBasis.equivAdjoinSimple_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) : pb.equivAdjoinSimple (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen

@[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) : pb.equivAdjoinSimple.symm ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f

@[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) : pb.equivAdjoinSimple.symm pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen

theorem IntermediateField.map_comap_eq {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField.map f (IntermediateField.comap f S) = S ⊓ f.fieldRange

theorem IntermediateField.map_comap_eq_self {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) : IntermediateField.map f (IntermediateField.comap f S) = S

theorem IntermediateField.map_comap_eq_self_of_surjective {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} (hf : Function.Surjective ⇑f) (S : IntermediateField K L') : IntermediateField.map f (IntermediateField.comap f S) = S

theorem IntermediateField.comap_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L) : IntermediateField.comap f (IntermediateField.map f S) = S