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.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)
:
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 α)
:
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)
(hS₂ : IntermediateField.adjoin F S = ⊤)
:
theorem
IntermediateField.finite_of_fg_of_isAlgebraic
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(h : ⊤.FG)
[Algebra.IsAlgebraic F E]
:
Module.Finite F E
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_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_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]
:
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]
:
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.