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 ≤ (IntermediateField.adjoin F S).toSubalgebra
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)
:
(IntermediateField.adjoin F S).toSubalgebra = 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)
:
K = IntermediateField.adjoin F S
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 = ⊤)
:
@[simp]
theorem
IntermediateField.AdjoinSimple.isIntegral_gen
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : E)
:
IsIntegral F (IntermediateField.AdjoinSimple.gen F α) ↔ IsIntegral F α
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)
:
(IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
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 = Algebra.adjoin F {α}
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_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)
:
(IntermediateField.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].
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]
:
(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
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]
:
(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
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
@[deprecated IntermediateField.fg_of_fg_toSubalgebra (since := "2024-10-28")]
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
Alias of IntermediateField.fg_of_fg_toSubalgebra.
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 (IntermediateField.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)
:
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.
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.
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)
:
(IsFractionRing.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.
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)
:
(IsFractionRing.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.