Adjoining Elements to Fields #
This file relates IntermediateField.adjoin to Algebra.adjoin.
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.
Equations
Instances For
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)
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
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)
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)
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)
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)
:
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)
:
theorem
IntermediateField.fg_top
(F : Type u_1)
[Field F]
(E : Type u_2)
[Field E]
[Algebra F E]
[Algebra.EssFiniteType F E]
:
theorem
IntermediateField.essFiniteType_iff
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{K : IntermediateField F E}
:
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)
:
@[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)
:
Alias of IntermediateField.adjoin_toSubalgebra_of_isAlgebraic.
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 ฮฑ)
:
@[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 ฮฑ)
:
@[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)
:
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)
:
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)
:
Alias of the forward direction of IntermediateField.adjoin_eq_top_iff_of_isAlgebraic.
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)
:
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)
:
Alias of the forward direction of IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic.
@[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}
:
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
@[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
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)
:
Ring homomorphism between A[b] and Aโฎโbโฏ.
Equations
Instances For
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 โฅ(Algebra.adjoin A {b}) โฅAโฎ(algebraMap B C) bโฏ
Equations
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 (โฅ(Algebra.adjoin A {b})) (โฅAโฎ(algebraMap B C) bโฏ) C
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)
:
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]
:
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]
:
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)
:
The compositum of two intermediate fields is equal to the compositum of them as subalgebras, if one of them is algebraic over the base field.
theorem
IntermediateField.sup_toSubalgebra_of_left
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
(E1 E2 : IntermediateField K L)
[FiniteDimensional K โฅE1]
:
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]
:
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)
:
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_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]
:
@[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]
:
Alias of IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left.
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]
:
@[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]
:
Alias of IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right.
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
theorem
IntermediateField.fg_of_noetherian
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : IntermediateField F E)
[IsNoetherian F E]
:
S.FG
theorem
IntermediateField.induction_on_adjoin
{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
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)
:
If F is a field, A is an F-algebra with fraction field K, L is a field,
g : A โโ[F] L lifts to f : K โโ[F] L,
then the image of f is the field generated by the image of g.
Note: this does not require IsScalarTower F A K.
theorem
IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq
{F : Type u_1}
{A : Type u_2}
{K : Type u_3}
{L : Type u_4}
[Field F]
[CommRing A]
[Algebra F A]
[Field K]
[Algebra F K]
[Algebra A K]
[IsFractionRing A K]
[Field L]
[Algebra F L]
{g : A โโ[F] L}
{f : K โโ[F] L}
(h : (โf).comp (algebraMap A K) = โg)
{s : Set L}
(hs : g.range = Algebra.adjoin F s)
:
If F is a field, A is an F-algebra with fraction field K, L is a field,
g : A โโ[F] L lifts to f : K โโ[F] L,
s is a set such that the image of g is the subalgebra generated by s,
then the image of f is the intermediate field generated by s.
Note: this does not require IsScalarTower F A K.
theorem
IsFractionRing.liftAlgHom_fieldRange
{F : Type u_1}
{A : Type u_2}
{K : Type u_3}
{L : Type u_4}
[Field F]
[CommRing A]
[Algebra F A]
[Field K]
[Algebra F K]
[Algebra A K]
[IsFractionRing A K]
[Field L]
[Algebra F L]
{g : A โโ[F] L}
[IsScalarTower F A K]
(hg : Function.Injective โg)
:
The image of IsFractionRing.liftAlgHom is the intermediate field generated by the image
of the algebra hom.
theorem
IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq
{F : Type u_1}
{A : Type u_2}
{K : Type u_3}
{L : Type u_4}
[Field F]
[CommRing A]
[Algebra F A]
[Field K]
[Algebra F K]
[Algebra A K]
[IsFractionRing A K]
[Field L]
[Algebra F L]
{g : A โโ[F] L}
[IsScalarTower F A K]
(hg : Function.Injective โg)
{s : Set L}
(hs : g.range = Algebra.adjoin F s)
:
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.