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, K[x] might not include x⁻¹.

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.

@[simp]

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

theorem IntermediateField.mem_adjoin_iff_div {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {x : E} : x ∈ adjoin F S ↔ ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / 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} : 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 (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 (adjoin F) fun (x : IntermediateField F E) => ↑x

Galois insertion between adjoin and coe.

@[implicit_reducible]

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

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemMin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K₁ K₂ : IntermediateField F E) : Algebra ↥(K₁ ⊓ K₂) ↥K₁

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemMin_1 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K₁ K₂ : IntermediateField F E) : Algebra ↥(K₁ ⊓ K₂) ↥K₂

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 = 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 = adjoin F (⋃₀ (SetLike.coe '' S))

@[implicit_reducible]

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

@[implicit_reducible]

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

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) = ⋂ s ∈ S, ↑s

@[simp]

theorem IntermediateField.mem_sInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set (IntermediateField F E)} {x : E} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

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

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

The bottom IntermediateField is isomorphic to the field.

theorem IntermediateField.botEquiv_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) : (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) : (botEquiv F E).symm x = (algebraMap F ↥⊥) x

@[implicit_reducible]

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

theorem IntermediateField.coe_algebraMap_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ⇑(algebraMap (↥⊥) F) = ⇑(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

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.

@[simp]

theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (a : E) : ↑(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 : ↥⊤) : 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) : 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] : restrictScalars K ⊤ = ⊤

@[simp]

theorem IntermediateField.restrictScalars_eq_top_iff {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 : IntermediateField F E} : restrictScalars K L = ⊤ ↔ L = ⊤

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) : restrictScalars K L ⊔ restrictScalars K L' = 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) : restrictScalars K L ⊓ restrictScalars K L' = 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) : 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) : map f (s ⊔ t) = map f s ⊔ 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) : map f (iSup s) = ⨆ (i : ι), 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) : map f (s ⊓ t) = map f s ⊓ 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) : map f (iInf s) = ⨅ (i : ι), 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.adjoin_eq_range_algebraMap_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) : ↑(adjoin F S) = Set.range ⇑(algebraMap (↥(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 ∈ 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) ⊆ ↑(adjoin F S)

@[implicit_reducible]

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

@[simp]

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

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

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

@[implicit_reducible]

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

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) : adjoin F S ≤ adjoin F T

theorem IntermediateField.adjoin_contains_field_as_subfield {E : Type u_2} [Field E] (S : Set E) (F : Subfield E) : ↑F ⊆ ↑(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 ⊆ ↑(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 ⊆ ↑(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] : 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) : (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} : ↑(adjoin F S) ⊆ ↑(adjoin F' S') ↔ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin F' S') ∧ S ⊆ ↑(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) : restrictScalars F (adjoin (↥(adjoin F S)) T) = adjoin F (S ∪ T)

Adjoining S and then T is the same as adjoining 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) : adjoin F (insert x ↑(adjoin F S)) = 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) : restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(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') : map f (adjoin F S) = 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) : lift (adjoin F S) = 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) : 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) : 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) : lift ⊤ = K

theorem IntermediateField.lift_sup (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (L L' : IntermediateField F ↥K) : lift (L ⊔ L') = lift L ⊔ lift L'

theorem IntermediateField.lift_inf (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (L L' : IntermediateField F ↥K) : lift (L ⊓ L') = lift L ⊓ lift L'

@[simp]

theorem IntermediateField.adjoin_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) : 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) : restrictScalars F (adjoin (↥K) S) = 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 ≤ adjoin F S) : extendScalars h = 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} : adjoin F (S ∪ T) = adjoin F S ⊔ 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) : restrictScalars F (adjoin (↥K) S) = K ⊔ 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) : adjoin F (⋃ (i : ι), f i) = ⨆ (i : ι), 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 = 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) : restrictScalars F (adjoin L S) = restrictScalars F (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.adjoin_induction (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {s : Set E} {p : (x : E) → x ∈ 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 ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯) (inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯) (mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯) {x : E} (h : x ∈ 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} ⦃φ₁ φ₂ : ↥(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 = 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.

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

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

@[simp]

theorem IntermediateField.AdjoinSimple.coe_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) : ↑(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) (gen F α) = α

@[simp]

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

theorem IntermediateField.adjoin_simple_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α β : E) : 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) : restrictScalars F (↥F⟮α⟯)⟮β⟯ = restrictScalars F (↥F⟮β⟯)⟮α⟯

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⟯ = adjoin F S

def IntermediateField.RingHom.adjoinAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : ↥A⟮b⟯ →+* ↥A⟮(algebraMap B C) b⟯

Ring homomorphism between A⟮b⟯ and A⟮↑b⟯.

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : Algebra ↥A⟮b⟯ ↥A⟮(algebraMap B C) b⟯

instance IntermediateField.instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : IsScalarTower (↥A⟮b⟯) (↥A⟮(algebraMap B C) b⟯) C

@[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} : 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⟯ = ⊥

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.

We use the class Algebra.EssFiniteType F E instead of (⊤ : IntermediateField F E).FG to say that E is finitely generated as an F extension. See IntermediateField.fg_top_iff.

theorem IntermediateField.fg_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (t : Finset E) : (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 ∧ 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) : (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.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 (restrictScalars F (↥K)⟮x⟯)) : P (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 (restrictScalars F (↥K)⟮x⟯)) (K : IntermediateField F E) (hK : K.FG) : P K

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') : map f (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) : map f (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') : map f (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) : comap f (map f S) = S

@[simp]

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

@[simp]

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

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

theorem Subfield.extendScalars_inf {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') : extendScalars h ⊓ extendScalars h' = 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) : 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) : 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') : extendScalars h ⊔ extendScalars h' = 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') : extendScalars h ⊓ extendScalars h' = extendScalars ⋯