Documentation

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) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :

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

Equations
Instances For
theorem IntermediateField.mem_adjoin_iff (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {S : Set E} (x : E) :
∃ (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) [] {E : Type u_2} [] [Algebra F E] {α : E} (x : E) :
x Fα ∃ (r : ) (s : ), x = () r / () s
@[simp]
theorem IntermediateField.adjoin_le_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} {T : } :
S T
theorem IntermediateField.gc {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
GaloisConnection fun (x : ) => x
def IntermediateField.gi {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
GaloisInsertion fun (x : ) => x

Galois insertion between adjoin and coe.

Equations
• IntermediateField.gi = { choice := fun (s : Set E) (hs : () s) => ().copy s , gc := , le_l_u := , choice_eq := }
Instances For
instance IntermediateField.instCompleteLattice {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Equations
• IntermediateField.instCompleteLattice = let __spread.0 := IntermediateField.gi.liftCompleteLattice; CompleteLattice.mk
instance IntermediateField.instInhabited {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Equations
• IntermediateField.instInhabited = { default := }
instance IntermediateField.instUnique {F : Type u_1} [] :
Equations
• IntermediateField.instUnique = let __src := ; { toInhabited := __src, uniq := }
theorem IntermediateField.coe_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
= Set.range ()
theorem IntermediateField.mem_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {x : E} :
x x Set.range ()
@[simp]
theorem IntermediateField.bot_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
.toSubalgebra =
@[simp]
theorem IntermediateField.coe_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
= Set.univ
@[simp]
theorem IntermediateField.mem_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {x : E} :
@[simp]
theorem IntermediateField.top_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
.toSubalgebra =
@[simp]
theorem IntermediateField.top_toSubfield {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
.toSubfield =
@[simp]
theorem IntermediateField.coe_inf {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) (T : ) :
(S T) = S T
@[simp]
theorem IntermediateField.mem_inf {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } {T : } {x : E} :
x S T x S x T
@[simp]
theorem IntermediateField.inf_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) (T : ) :
(S T).toSubalgebra = S.toSubalgebra T.toSubalgebra
@[simp]
theorem IntermediateField.inf_toSubfield {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) (T : ) :
(S T).toSubfield = S.toSubfield T.toSubfield
@[simp]
theorem IntermediateField.coe_sInf {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : Set ()) :
(sInf S) = sInf ((fun (x : ) => x) '' S)
@[simp]
theorem IntermediateField.sInf_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : Set ()) :
(sInf S).toSubalgebra = sInf (IntermediateField.toSubalgebra '' S)
@[simp]
theorem IntermediateField.sInf_toSubfield {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : Set ()) :
(sInf S).toSubfield = sInf (IntermediateField.toSubfield '' S)
@[simp]
theorem IntermediateField.coe_iInf {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Sort u_3} (S : ι) :
(iInf S) = ⋂ (i : ι), (S i)
@[simp]
theorem IntermediateField.iInf_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Sort u_3} (S : ι) :
(iInf S).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra
@[simp]
theorem IntermediateField.iInf_toSubfield {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Sort u_3} (S : ι) :
(iInf S).toSubfield = ⨅ (i : ι), (S i).toSubfield
@[simp]
theorem IntermediateField.equivOfEq_apply {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } {T : } (h : S = T) (x : S.toSubalgebra) :
= x,
def IntermediateField.equivOfEq {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } {T : } (h : S = T) :
S ≃ₐ[F] T

Construct an algebra isomorphism from an equality of intermediate fields

Equations
• = S.equivOfEq T.toSubalgebra
Instances For
@[simp]
theorem IntermediateField.equivOfEq_symm {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } {T : } (h : S = T) :
@[simp]
theorem IntermediateField.equivOfEq_rfl {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) :
= AlgEquiv.refl
@[simp]
theorem IntermediateField.equivOfEq_trans {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } {T : } {U : } (hST : S = T) (hTU : T = U) :
.trans =
noncomputable def IntermediateField.botEquiv (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] :

The bottom intermediate_field is isomorphic to the field.

Equations
• = (.equivOfEq ).trans ()
Instances For
theorem IntermediateField.botEquiv_def {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (x : F) :
(() x) = x
@[simp]
theorem IntermediateField.botEquiv_symm {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (x : F) :
.symm x = () x
noncomputable instance IntermediateField.algebraOverBot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Algebra () F
Equations
• IntermediateField.algebraOverBot = ().toAlgebra
theorem IntermediateField.coe_algebraMap_over_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
(algebraMap () F) =
instance IntermediateField.isScalarTower_over_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Equations
• =
@[simp]
theorem IntermediateField.topEquiv_apply {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
∀ (a : .toSubalgebra), IntermediateField.topEquiv a = a
@[simp]
theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
∀ (a : E), (IntermediateField.topEquiv.symm a) = ((Subalgebra.topEquiv).symm a)
def IntermediateField.topEquiv {F : Type u_1} [] {E : Type u_2} [] [Algebra 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
Instances For
@[simp]
theorem IntermediateField.restrictScalars_bot_eq_self {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :
@[simp]
theorem IntermediateField.restrictScalars_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra K E] [Algebra K F] [] :
@[simp]
theorem IntermediateField.map_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (f : E →ₐ[F] K) :
theorem IntermediateField.map_sup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (s : ) (t : ) (f : E →ₐ[F] K) :
theorem IntermediateField.map_iSup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] {ι : Sort u_4} (f : E →ₐ[F] K) (s : ι) :
= ⨆ (i : ι), IntermediateField.map f (s i)
theorem AlgHom.fieldRange_eq_map {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (f : E →ₐ[F] K) :
f.fieldRange =
theorem AlgHom.map_fieldRange {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] {L : Type u_4} [] [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} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] {f : E →ₐ[F] K} :
f.fieldRange =
@[simp]
theorem AlgEquiv.fieldRange_eq_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (f : E ≃ₐ[F] K) :
(f).fieldRange =
theorem IntermediateField.fieldRange_comp_val {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (L : ) (f : E →ₐ[F] K) :
(f.comp L.val).fieldRange =
noncomputable def IntermediateField.equivMap {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (L : ) (f : E →ₐ[F] K) :
L ≃ₐ[F] ()

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

Equations
Instances For
@[simp]
theorem IntermediateField.coe_equivMap_apply {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : Type u_3} [] [Algebra F K] (L : ) (f : E →ₐ[F] K) (x : L) :
((L.equivMap f) x) = f x
theorem IntermediateField.adjoin_eq_range_algebraMap_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
() = Set.range (algebraMap (()) E)
theorem IntermediateField.adjoin.algebraMap_mem (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (x : F) :
() x
theorem IntermediateField.adjoin.range_algebraMap_subset (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
Set.range () ()
instance IntermediateField.adjoin.fieldCoe (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
CoeTC F ()
Equations
• = { coe := fun (x : F) => () x, }
theorem IntermediateField.subset_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
S ()
instance IntermediateField.adjoin.setCoe (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
CoeTC S ()
Equations
• = { coe := fun (x : S) => x, }
theorem IntermediateField.adjoin.mono (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (T : Set E) (h : S T) :
theorem IntermediateField.adjoin_contains_field_as_subfield {E : Type u_2} [] (S : Set E) (F : ) :
F ()
theorem IntermediateField.subset_adjoin_of_subset_left {E : Type u_2} [] (S : Set E) {F : } {T : Set E} (HT : T F) :
T ()
theorem IntermediateField.subset_adjoin_of_subset_right (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) {T : Set E} (H : T S) :
T ()
@[simp]
theorem IntermediateField.adjoin_empty (F : Type u_3) (E : Type u_4) [] [] [Algebra F E] :
F⟮⟯ =
@[simp]
theorem IntermediateField.adjoin_univ (F : Type u_3) (E : Type u_4) [] [] [Algebra F E] :
theorem IntermediateField.adjoin_le_subfield (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) {K : } (HF : Set.range () K) (HS : S K) :
().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) [] {E : Type u_2} [] [Algebra F E] {F' : Type u_3} [Field F'] [Algebra F' E] {S : Set E} {S' : Set E} :
() () Set.range () () S ()
theorem IntermediateField.adjoin_adjoin_left (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (T : Set E) :

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

@[simp]
theorem IntermediateField.adjoin_insert_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (x : E) :
=
theorem IntermediateField.adjoin_adjoin_comm (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (T : Set E) :

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

theorem IntermediateField.adjoin_map (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) {E' : Type u_3} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') :
@[simp]
theorem IntermediateField.lift_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) (S : Set K) :
= IntermediateField.adjoin F (Subtype.val '' S)
theorem IntermediateField.lift_adjoin_simple (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) (α : K) :
= Fα
@[simp]
theorem IntermediateField.lift_bot (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) :
@[simp]
theorem IntermediateField.lift_top (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) :
@[simp]
theorem IntermediateField.adjoin_self (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) :
theorem IntermediateField.restrictScalars_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (K : ) (S : Set E) :
theorem IntermediateField.extendScalars_adjoin {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : } {S : Set E} (h : ) :
theorem IntermediateField.restrictScalars_adjoin_of_algEquiv {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {L : Type u_3} {L' : Type u_4} [] [Field L'] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : () = (algebraMap L' E) i) (S : Set E) :

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) [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
().toSubalgebra
theorem IntermediateField.adjoin_eq_algebra_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (inv_mem : x, x⁻¹ ) :
().toSubalgebra =
theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (K : ) (h : K.toSubalgebra = ) :
theorem IntermediateField.adjoin_eq_top_of_algebra (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (S : Set E) (hS : = ) :
theorem IntermediateField.adjoin_induction (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {s : Set E} {p : EProp} {x : E} (h : ) (mem : xs, p x) (algebraMap : ∀ (x : F), p (() x)) (add : ∀ (x y : E), p xp yp (x + y)) (neg : ∀ (x : E), p xp (-x)) (inv : ∀ (x : E), p xp x⁻¹) (mul : ∀ (x y : E), p xp yp (x * y)) :
p x

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.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IntermediateField.mem_adjoin_simple_self (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
α Fα
def IntermediateField.AdjoinSimple.gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
Fα

generator of F⟮α⟯

Equations
• = α,
Instances For
@[simp]
theorem IntermediateField.AdjoinSimple.coe_gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
theorem IntermediateField.AdjoinSimple.algebraMap_gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
(algebraMap (Fα) E) = α
@[simp]
theorem IntermediateField.AdjoinSimple.isIntegral_gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
theorem IntermediateField.adjoin_simple_adjoin_simple (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) (β : E) :
IntermediateField.restrictScalars F (Fα)β = Fα, β
theorem IntermediateField.adjoin_simple_comm (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) (β : E) :
IntermediateField.restrictScalars F (Fα)β = IntermediateField.restrictScalars F (Fβ)α
theorem IntermediateField.adjoin_algebraic_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} (hS : xS, ) :
().toSubalgebra =
theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} (hα : ) :
theorem isSplittingField_iff_intermediateField {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {p : } :

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

theorem IntermediateField.isSplittingField_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {p : } {K : } :
theorem IntermediateField.adjoin_rootSet_isSplittingField {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {p : } (hp : Polynomial.Splits () p) :
theorem IntermediateField.le_sup_toSubalgebra {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (E1 : ) (E2 : ) :
E1.toSubalgebra E2.toSubalgebra (E1 E2).toSubalgebra
theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (E1 : ) (E2 : ) [] :
(E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_left {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (E1 : ) (E2 : ) [] :
(E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (E1 : ) (E2 : ) (halg : ) :
(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} [] [] [Algebra K L] (E1 : ) (E2 : ) [] :
(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} [] [] [Algebra K L] (E1 : ) (E2 : ) [] :
(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} [] [] [Algebra K L] (E1 : ) (E2 : ) [] :
(E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
instance IntermediateField.finiteDimensional_sup {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (E1 : ) (E2 : ) [] [] :
FiniteDimensional K (E1 E2)
Equations
• =
theorem IntermediateField.coe_iSup_of_directed {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {ι : Type u_5} {t : ι} [] (dir : Directed (fun (x x_1 : ) => x x_1) t) :
(iSup t) = ⋃ (i : ι), (t i)
theorem IntermediateField.toSubalgebra_iSup_of_directed {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {ι : Type u_5} {t : ι} (dir : Directed (fun (x x_1 : ) => x x_1) t) :
(iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
instance IntermediateField.finiteDimensional_iSup_of_finite {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {ι : Type u_5} {t : ι} [h : ] [∀ (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} [] [] [Algebra K L] {ι : Type u_5} {t : ι} {s : } [∀ (i : ι), FiniteDimensional K (t i)] :
FiniteDimensional K (is, t i)
Equations
• =
theorem IntermediateField.finiteDimensional_iSup_of_finset' {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {ι : Type u_5} {t : ι} {s : } (h : is, FiniteDimensional K (t i)) :
FiniteDimensional K (is, t i)
theorem IntermediateField.isSplittingField_iSup {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {ι : Type u_5} {t : ι} {p : ι} {s : } (h0 : (s.prod fun (i : ι) => p i) 0) (h : is, Polynomial.IsSplittingField K ((t i)) (p i)) :
Polynomial.IsSplittingField K ((is, t i)) (s.prod fun (i : ι) => p i)

A compositum of splitting fields is a splitting field

theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic {F : Type u_1} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) (halg : ) :
().toSubalgebra =

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} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) [halg : ] :
().toSubalgebra =
theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right {F : Type u_1} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) [halg : ] :
().toSubalgebra =
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic {F : Type u_1} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) (halg : ) :
Module.rank E () 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} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) [halg : ] :
Module.rank E () Module.rank F L
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_right {F : Type u_1} [] (E : Type u_2) [] [Algebra F E] {K : Type u_3} [] [Algebra F K] [Algebra E K] [] (L : ) [halg : ] :
Module.rank E () Module.rank F L
theorem IntermediateField.adjoin_simple_le_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} {K : } :
Fα K α K
theorem IntermediateField.biSup_adjoin_simple {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : Set E) :
xS, Fx =
theorem IntermediateField.adjoin_simple_isCompactElement {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (x : E) :

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

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

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

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

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

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

The lattice of intermediate fields is compactly generated.

Equations
• =
theorem IntermediateField.exists_finset_of_mem_iSup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Type u_3} {f : ι} {x : E} (hx : x ⨆ (i : ι), f i) :
∃ (s : ), x is, f i
theorem IntermediateField.exists_finset_of_mem_supr' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Type u_3} {f : ι} {x : E} (hx : x ⨆ (i : ι), f i) :
∃ (s : Finset ((i : ι) × (f i))), x is, Fi.snd
theorem IntermediateField.exists_finset_of_mem_supr'' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {ι : Type u_3} {f : ι} (h : ∀ (i : ι), Algebra.IsAlgebraic F (f i)) {x : E} (hx : x ⨆ (i : ι), f i) :
∃ (s : Finset ((i : ι) × (f i))), x is, IntermediateField.adjoin F ((minpoly F i.snd).rootSet E)
theorem IntermediateField.exists_finset_of_mem_adjoin {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} {x : E} (hx : ) :
∃ (T : ), T S
@[simp]
theorem IntermediateField.adjoin_eq_bot_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} :
S
theorem IntermediateField.adjoin_simple_eq_bot_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} :
Fα = α
@[simp]
theorem IntermediateField.adjoin_zero {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
F0 =
@[simp]
theorem IntermediateField.adjoin_one {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
F1 =
@[simp]
theorem IntermediateField.adjoin_intCast {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (n : ) :
Fn =
@[simp]
theorem IntermediateField.adjoin_natCast {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (n : ) :
Fn =
theorem IntermediateField.adjoin_int {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (n : ) :
Fn =

Alias of IntermediateField.adjoin_intCast.

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

Alias of IntermediateField.adjoin_natCast.

@[simp]
theorem IntermediateField.rank_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : } :
Module.rank F K = 1 K =
@[simp]
theorem IntermediateField.finrank_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {K : } :
K =
@[simp]
theorem IntermediateField.rank_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
= 1
@[simp]
theorem IntermediateField.finrank_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
@[simp]
theorem IntermediateField.rank_bot' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Module.rank () E =
@[simp]
theorem IntermediateField.finrank_bot' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
@[simp]
theorem IntermediateField.rank_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
Module.rank () E = 1
@[simp]
theorem IntermediateField.finrank_top {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
= 1
@[simp]
theorem IntermediateField.rank_top' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
=
@[simp]
theorem IntermediateField.finrank_top' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
theorem IntermediateField.rank_adjoin_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} :
= 1 S
theorem IntermediateField.rank_adjoin_simple_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} :
Module.rank F Fα = 1 α
theorem IntermediateField.finrank_adjoin_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : Set E} :
S
theorem IntermediateField.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} :
= 1 α
theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (h : ∀ (x : E), Module.rank F Fx = 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} [] {E : Type u_2} [] [Algebra F E] (h : ∀ (x : E), = 1) :
theorem IntermediateField.subsingleton_of_rank_adjoin_eq_one {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (h : ∀ (x : E), Module.rank F Fx = 1) :
theorem IntermediateField.subsingleton_of_finrank_adjoin_eq_one {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (h : ∀ (x : E), = 1) :
theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [] (h : ∀ (x : E), 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} [] {E : Type u_2} [] [Algebra F E] [] (h : ∀ (x : E), 1) :
theorem IntermediateField.minpoly_gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
= minpoly F α
theorem IntermediateField.aeval_gen_minpoly (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] (α : E) :
(minpoly F α) = 0
noncomputable def IntermediateField.adjoinRootEquivAdjoin (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {α : E} (h : ) :
AdjoinRoot (minpoly F α) ≃ₐ[F] Fα

algebra isomorphism between AdjoinRoot and F⟮α⟯

Equations
Instances For
theorem IntermediateField.adjoinRootEquivAdjoin_apply_root (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {α : E} (h : ) :
theorem IntermediateField.adjoin_root_eq_top {K : Type u} [] (p : ) [Fact ()] :
K =
noncomputable def IntermediateField.powerBasisAux {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
Basis (Fin (minpoly K x).natDegree) K Kx

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
• = .basis.map .toLinearEquiv
Instances For
@[simp]
theorem IntermediateField.adjoin.powerBasis_gen {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
@[simp]
theorem IntermediateField.adjoin.powerBasis_dim {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
.dim = (minpoly K x).natDegree
noncomputable def IntermediateField.adjoin.powerBasis {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
PowerBasis K Kx

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

Equations
• = { gen := , dim := (minpoly K x).natDegree, basis := , basis_eq_pow := }
Instances For
theorem IntermediateField.adjoin.finiteDimensional {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
FiniteDimensional K Kx
theorem IntermediateField.isAlgebraic_adjoin_simple {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
Algebra.IsAlgebraic K Kx
theorem IntermediateField.adjoin.finrank {K : Type u} [] {L : Type u_3} [] [Algebra K L] {x : L} (hx : ) :
= (minpoly K x).natDegree
theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {K : Type u} [] [Algebra F K] [Algebra E K] [] {S : Set K} (hprim : ) :

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) [] {E : Type u_2} [] [Algebra F E] {α : E} [] (hprim : Fα = ) (K : ) :
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.

theorem IntermediateField.exists_lt_finrank_of_infinite_dimensional {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [] (hnfd : ) (n : ) :
∃ (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} [] {L : Type u_3} [] [Algebra K L] (x : L) [] :
(minpoly K x).natDegree
theorem minpoly.degree_le {K : Type u} [] {L : Type u_3} [] [Algebra K L] (x : L) [] :
(minpoly K x).degree
theorem IntermediateField.isAlgebraic_iSup {K : Type u} [] {L : Type u_3} [] [Algebra K L] {ι : Type u_4} {t : ι} (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} [] {L : Type u_3} [] [Algebra K L] {S : Set L} (hS : xS, ) :
theorem IntermediateField.finiteDimensional_adjoin {K : Type u} [] {L : Type u_3} [] [Algebra K L] {S : Set L} [Finite S] (hS : xS, ) :

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) [] {E : Type u_2} [] [Algebra F E] {α : E} {K : Type u} [] [Algebra F K] (h : ) :
(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
• = .liftEquiv'.trans (().subtypeEquiv )
Instances For
theorem IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {α : E} {K : Type u} [] [Algebra F K] (h : ) (x : { x : K // x (minpoly F α).aroots K }) :
(.symm x) = x
noncomputable def IntermediateField.fintypeOfAlgHomAdjoinIntegral (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {α : E} {K : Type u} [] [Algebra F K] (h : ) :
Fintype (Fα →ₐ[F] K)

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

Equations
Instances For
theorem IntermediateField.card_algHom_adjoin_integral (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] {α : E} {K : Type u} [] [Algebra F K] (h : ) (h_sep : (minpoly F α).Separable) (h_splits : Polynomial.Splits () (minpoly F α)) :
Fintype.card (Fα →ₐ[F] K) = (minpoly F α).natDegree
theorem Polynomial.irreducible_comp {K : Type u} [] {f : } {g : } (hfm : f.Monic) (hgm : g.Monic) (hf : ) (hg : ∀ (E : Type u) [inst : ] [inst_1 : Algebra K E] (x : E), minpoly K x = fIrreducible (Polynomial.map (algebraMap K Kx) g - Polynomial.C )) :
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} [] {E : Type u_2} [] [Algebra F E] (S : ) :

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

Equations
• S.FG = ∃ (t : ),
Instances For
theorem IntermediateField.fg_adjoin_finset {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (t : ) :
().FG
theorem IntermediateField.fg_def {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {S : } :
S.FG ∃ (t : Set E), t.Finite
theorem IntermediateField.fg_bot {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
.FG
theorem IntermediateField.fG_of_fG_toSubalgebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) (h : S.FG) :
S.FG
theorem IntermediateField.fg_of_noetherian {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) [] :
S.FG
theorem IntermediateField.induction_on_adjoin_finset {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (S : ) (P : ) (base : P ) (ih : ∀ (K : ), xS, P KP ()) :
P ()
theorem IntermediateField.induction_on_adjoin_fg {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (P : ) (base : P ) (ih : ∀ (K : ) (x : E), P KP ()) (K : ) (hK : K.FG) :
P K
theorem IntermediateField.induction_on_adjoin {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [] (P : ) (base : P ) (ih : ∀ (K : ) (x : E), P KP ()) (K : ) :
P K
noncomputable def PowerBasis.equivAdjoinSimple {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (pb : ) :
Kpb.gen ≃ₐ[K] L

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

Equations