Adjoining Elements to Fields #

This file relates IntermediateField.adjoin to Algebra.adjoin.

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 ≤ (adjoin F S).toSubalgebra

source

🔸 coverage

@[implicit_reducible]

def IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

Algebra ↥(Algebra.adjoin F S) ↥(adjoin F S)

IntermediateField.adjoin as an algebra over Algebra.adjoin.

Instances For

source

📐 coverage

@[simp]

theorem IntermediateField.algebraAdjoinAdjoin.coe_algebraMap (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : ↥(Algebra.adjoin F S)) :

↑((algebraMap ↥(Algebra.adjoin F S) ↥(adjoin F S)) x) = ↑x

source

📐 coverage

@[simp]

theorem IntermediateField.algebraAdjoinAdjoin.algebraMap_eq_gen_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :

(algebraMap ↥F[x] ↥F⟮x⟯) ⟨x, ⋯⟩ = AdjoinSimple.gen F x

source

📐 coverage

theorem IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (X : Type u_3) [SMul X F] [SMul X E] [IsScalarTower X F E] :

IsScalarTower X ↥(Algebra.adjoin F S) ↥(adjoin F S)

source

📐 coverage

theorem IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1 (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (X : Type u_3) [MulAction E X] :

IsScalarTower (↥(Algebra.adjoin F S)) (↥(adjoin F S)) X

source

📐 coverage

theorem IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

FaithfulSMul ↥(Algebra.adjoin F S) ↥(adjoin F S)

source

📐 coverage

theorem IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

IsFractionRing ↥(Algebra.adjoin F S) ↥(adjoin F S)

source

📐 coverage

theorem IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

Algebra.IsAlgebraic ↥(Algebra.adjoin F S) ↥(adjoin F S)

source

📐 coverage

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

(adjoin F S).toSubalgebra = Algebra.adjoin F S

source

📐 coverage

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

source

📐 coverage

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 = ⊤) :

adjoin F S = ⊤

source

📐 coverage

theorem IntermediateField.fg_top_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊤.FG ↔ Algebra.EssFiniteType F E

source

📐 coverage

theorem IntermediateField.fg_top (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [Algebra.EssFiniteType F E] :

⊤.FG

source

📐 coverage

theorem IntermediateField.essFiniteType_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :

Algebra.EssFiniteType F ↥K ↔ K.FG

source

📐 coverage

@[simp]

theorem IntermediateField.AdjoinSimple.isIntegral_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

IsIntegral F (gen F α) ↔ IsIntegral F α

source

📐 coverage

theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x) :

(adjoin F S).toSubalgebra = Algebra.adjoin F S

source

📐 coverage

@[deprecated IntermediateField.adjoin_toSubalgebra_of_isAlgebraic (since := "2025-11-24")]

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

(adjoin F S).toSubalgebra = Algebra.adjoin F S

Alias of IntermediateField.adjoin_toSubalgebra_of_isAlgebraic.

source

📐 coverage

theorem IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (hα : IsAlgebraic F α) :

F⟮α⟯.toSubalgebra = F[α]

source

📐 coverage

@[deprecated "Use `adjoin_simple_toSubalgebra_of_isAlgebraic` instead" (since := "2025-11-24")]

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 = F[α]

source

📐 coverage

@[simp]

theorem IntermediateField.adjoin_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (S : Set E) :

(adjoin F S).toSubalgebra = Algebra.adjoin F S

source

📐 coverage

theorem IntermediateField.adjoin_eq_top_iff_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x) :

adjoin F S = ⊤ ↔ Algebra.adjoin F S = ⊤

source

📐 coverage

theorem Algebra.adjoin_eq_top_of_intermediateField {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 = ⊤ → adjoin F S = ⊤

Alias of the forward direction of IntermediateField.adjoin_eq_top_iff_of_isAlgebraic.

source

📐 coverage

theorem IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} (hx : IsAlgebraic F x) :

F⟮x⟯ = ⊤ ↔ F[x] = ⊤

source

📐 coverage

theorem Algebra.adjoin_eq_top_of_primitive_element {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} (hx : IsAlgebraic F x) :

F⟮x⟯ = ⊤ → F[x] = ⊤

Alias of the forward direction of IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic.

source

📐 coverage

@[simp]

theorem IntermediateField.adjoin_eq_top_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] {S : Set E} :

adjoin F S = ⊤ ↔ Algebra.adjoin F S = ⊤

source

📐 coverage

theorem Algebra.finite_of_essFiniteType_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [EssFiniteType F E] [Algebra.IsAlgebraic F E] :

Module.Finite F E

source

📐 coverage

@[deprecated Algebra.finite_of_essFiniteType_of_isAlgebraic (since := "2025-12-08")]

theorem IntermediateField.finite_of_fg_of_isAlgebraic {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.EssFiniteType F E] [Algebra.IsAlgebraic F E] :

Module.Finite F E

Alias of Algebra.finite_of_essFiniteType_of_isAlgebraic.

source

🔸 coverage

noncomputable def IntermediateField.RingHom.adjoinAlgebraMapOfAlgebra {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [CommSemiring 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⟯.

Instances For

source

🔸 coverage

@[implicit_reducible]

noncomputable instance IntermediateField.instAlgebraSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [CommSemiring 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⟯

source

📐 coverage

instance IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [CommSemiring 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

source

📐 coverage

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

source

📐 coverage

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

source

📐 coverage

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

source

📐 coverage

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.

source

📐 coverage

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

source

📐 coverage

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

source

📐 coverage

theorem IntermediateField.adjoin_intermediateField_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) :

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

source

📐 coverage

theorem IntermediateField.adjoin_intermediateField_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] :

(adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

source

📐 coverage

@[deprecated IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left (since := "2025-11-24")]

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

(adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

Alias of IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left.

source

📐 coverage

theorem IntermediateField.adjoin_intermediateField_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] :

(adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

source

📐 coverage

@[deprecated IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right (since := "2025-11-24")]

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

(adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

Alias of IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right.

source

📐 coverage

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

source

📐 coverage

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

source

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

P K

source

📐 coverage

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.

source

📐 coverage

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.

source

📐 coverage

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

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

source

📐 coverage

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

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

Documentation

Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Adjoining Elements to Fields #