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

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)

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

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

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

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) : 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.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 α) = α

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

@[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 (since := "2024-04-05")]

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 (since := "2024-04-05")]

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.

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