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.

Stacks Tag 09FZ (first part)

Equations

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

@[simp]

theorem IntermediateField.adjoin_toSubfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) : (IntermediateField.adjoin F S).toSubfield = Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)

theorem IntermediateField.mem_adjoin_range_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} (i : ι → E) (x : E) : x ∈ IntermediateField.adjoin F (Set.range i) ↔ ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F), x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem IntermediateField.sup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) : S ⊔ T = IntermediateField.adjoin F (↑S ∪ ↑T)

theorem IntermediateField.sSup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) : sSup S = IntermediateField.adjoin F (⋃₀ (SetLike.coe '' S))

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 = ⊥

theorem IntermediateField.bot_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ⊥.toSubfield = (algebraMap F E).fieldRange

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

@[simp]

theorem IntermediateField.sup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S 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.sSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) (hS : S.Nonempty) : (sSup S).toSubfield = sSup (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.iSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Nonempty ι] (S : ι → IntermediateField F E) : (iSup S).toSubfield = ⨆ (i : ι), (S i).toSubfield

def IntermediateField.equivOfEq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S 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_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) (x : ↥S.toSubalgebra) : (IntermediateField.equivOfEq h) x = ⟨↑x, ⋯⟩

@[simp]

theorem IntermediateField.equivOfEq_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S 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 T 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

• ⋯ = ⋯

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 = Subalgebra.topEquiv

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

@[simp]

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

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

theorem IntermediateField.restrictScalars_sup {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] (L L' : IntermediateField F E) : IntermediateField.restrictScalars K L ⊔ IntermediateField.restrictScalars K L' = IntermediateField.restrictScalars K (L ⊔ L')

theorem IntermediateField.restrictScalars_inf {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] (L L' : IntermediateField F E) : IntermediateField.restrictScalars K L ⊓ IntermediateField.restrictScalars K L' = IntermediateField.restrictScalars K (L ⊓ L')

@[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 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 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 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 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 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 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.adjoin_union (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : Set E} : IntermediateField.adjoin F (S ∪ T) = IntermediateField.adjoin F S ⊔ IntermediateField.adjoin F T

theorem IntermediateField.restrictScalars_adjoin_eq_sup (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) = K ⊔ IntermediateField.adjoin F S

theorem IntermediateField.adjoin_iUnion (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ι → Set E) : IntermediateField.adjoin F (⋃ (i : ι), f i) = ⨆ (i : ι), IntermediateField.adjoin F (f i)

theorem IntermediateField.iSup_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ι → IntermediateField F E) : ⨆ (i : ι), f i = IntermediateField.adjoin F (⋃ (i : ι), ↑(f i))

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 : (x : E) → x ∈ IntermediateField.adjoin F s → Prop} (mem : ∀ (x : E) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (x : F), p ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s), p x hx → p y hy → p (x + y) ⋯) (inv : ∀ (x : E) (hx : x ∈ IntermediateField.adjoin F s), p x hx → p x⁻¹ ⋯) (mul : ∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s), p x hx → p y hy → p (x * y) ⋯) {x : E} (h : x ∈ IntermediateField.adjoin F s) : p x h

theorem IntermediateField.adjoin_algHom_ext (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {s : Set E} ⦃φ₁ φ₂ : ↥(IntermediateField.adjoin F s) →ₐ[F] K⦄ (h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) : φ₁ = φ₂

theorem IntermediateField.algHom_ext_of_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {S : IntermediateField F E} {s : Set E} (hS : S = IntermediateField.adjoin F s) ⦃φ₁ φ₂ : ↥S →ₐ[F] K⦄ (h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨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) : 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) : 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 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 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 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 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 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

theorem IntermediateField.sup_toSubalgebra_of_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 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 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2] : FiniteDimensional K ↥(E1 ⊔ E2)

Equations

• ⋯ = ⋯

theorem IntermediateField.rank_sup_le_of_isAlgebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2) : Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

If E1 and E2 are intermediate fields, and at least one them are algebraic, then the rank of the compositum of E1 and E2 is less than or equal to the product of that of E1 and E2. Note that this result is also true without algebraic assumption, but the proof becomes very complicated.

theorem IntermediateField.finrank_sup_le {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) : Module.finrank K ↥(E1 ⊔ E2) ≤ Module.finrank K ↥E1 * Module.finrank K ↥E2

If E1 and E2 are intermediate fields, then the Module.finrank of the compositum of E1 and E2 is less than or equal to the product of that of E1 and E2.

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⟮α⟯

Stacks Tag 09G1 (Algebraic case)

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

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 := ⋯ }

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

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

If x is an algebraic element of field K, then its minimal polynomial has degree [K(x) : K].

Stacks Tag 09GN

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 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.

Stacks Tag 09FZ (second part)

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_adjoin_of_finite {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {t : Set E} (h : t.Finite) : (IntermediateField.adjoin F t).FG

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

theorem IntermediateField.fg_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) : (S ⊔ T).FG

theorem IntermediateField.fg_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ (i : ι), (S i).FG) : (⨆ (i : ι), S i).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

@[deprecated IntermediateField.fg_of_fg_toSubalgebra]

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

Alias of IntermediateField.fg_of_fg_toSubalgebra.

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

@[simp]

theorem Subfield.extendScalars_self {L : Type u_2} [Field L] (F : Subfield L) : Subfield.extendScalars ⋯ = ⊥

@[simp]

theorem Subfield.extendScalars_top {L : Type u_2} [Field L] (F : Subfield L) : Subfield.extendScalars ⋯ = ⊤

theorem Subfield.extendScalars_sup {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') : Subfield.extendScalars h ⊔ Subfield.extendScalars h' = Subfield.extendScalars ⋯

theorem Subfield.extendScalars_inf {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') : Subfield.extendScalars h ⊓ Subfield.extendScalars h' = Subfield.extendScalars ⋯

@[simp]

theorem IntermediateField.extendScalars_self {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (F : IntermediateField K L) : IntermediateField.extendScalars ⋯ = ⊥

@[simp]

theorem IntermediateField.extendScalars_top {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (F : IntermediateField K L) : IntermediateField.extendScalars ⋯ = ⊤

theorem IntermediateField.extendScalars_sup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E') : IntermediateField.extendScalars h ⊔ IntermediateField.extendScalars h' = IntermediateField.extendScalars ⋯

theorem IntermediateField.extendScalars_inf {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E') : IntermediateField.extendScalars h ⊓ IntermediateField.extendScalars h' = IntermediateField.extendScalars ⋯

theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L} (h : (↑f).comp (algebraMap A K) = ↑g) : f.fieldRange = IntermediateField.adjoin F ↑g.range

If F is a field, A is an F-algebra with fraction field K, L is a field, g : A →ₐ[F] L lifts to f : K →ₐ[F] L, then the image of f is the field generated by the image of g. Note: this does not require IsScalarTower F A K.

theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L} (h : (↑f).comp (algebraMap A K) = ↑g) {s : Set L} (hs : g.range = Algebra.adjoin F s) : f.fieldRange = IntermediateField.adjoin F s

If F is a field, A is an F-algebra with fraction field K, L is a field, g : A →ₐ[F] L lifts to f : K →ₐ[F] L, s is a set such that the image of g is the subalgebra generated by s, then the image of f is the intermediate field generated by s. Note: this does not require IsScalarTower F A K.

theorem IsFractionRing.liftAlgHom_fieldRange {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} [IsScalarTower F A K] (hg : Function.Injective ⇑g) : (IsFractionRing.liftAlgHom hg).fieldRange = IntermediateField.adjoin F ↑g.range

The image of IsFractionRing.liftAlgHom is the intermediate field generated by the image of the algebra hom.

theorem IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} [IsScalarTower F A K] (hg : Function.Injective ⇑g) {s : Set L} (hs : g.range = Algebra.adjoin F s) : (IsFractionRing.liftAlgHom hg).fieldRange = IntermediateField.adjoin F s

The image of IsFractionRing.liftAlgHom is the intermediate field generated by s, if the image of the algebra hom is the subalgebra generated by s.