Algebraic independence persists to the algebraic closure #
Main results #
AlgebraicIndependent.extendScalars: if A/S/R is a tower of algebras with S/R algebraic, then a family of elements in A that are algebraically independent over R remains algebraically independent over S, provided that S has no zero divisors.AlgebraicIndependent.algebraicClosure: an algebraically independent family remains algebraically independent over the algebraic closure.
theorem
AlgebraicIndependent.extendScalars
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[NoZeroDivisors S]
(hx : AlgebraicIndependent R x)
[alg : Algebra.IsAlgebraic R S]
(inj : Function.Injective ⇑(algebraMap S A))
:
theorem
AlgebraicIndependent.extendScalars_of_isSimpleRing
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[NoZeroDivisors S]
(hx : AlgebraicIndependent R x)
[Algebra.IsAlgebraic R S]
[IsSimpleRing S]
:
theorem
AlgebraicIndependent.extendScalars_of_isIntegral
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[NoZeroDivisors S]
(hx : AlgebraicIndependent R x)
[Algebra.IsIntegral R S]
(inj : Function.Injective ⇑(algebraMap S A))
:
theorem
AlgebraicIndependent.subalgebra
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(S : Subalgebra R A)
[NoZeroDivisors A]
[Algebra.IsAlgebraic R ↥S]
:
AlgebraicIndependent (↥S) x
theorem
AlgebraicIndependent.subalgebra_of_isIntegral
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(S : Subalgebra R A)
[NoZeroDivisors A]
[Algebra.IsIntegral R ↥S]
:
AlgebraicIndependent (↥S) x
theorem
AlgebraicIndependent.subalgebraAlgebraicClosure
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[IsDomain R]
[NoZeroDivisors A]
:
AlgebraicIndependent (↥(Subalgebra.algebraicClosure R A)) x
theorem
AlgebraicIndependent.integralClosure
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[NoZeroDivisors A]
:
AlgebraicIndependent (↥(integralClosure R A)) x
theorem
AlgebraicIndependent.algebraicClosure
{ι : Type u_1}
{F : Type u_5}
{E : Type u_6}
[Field F]
[Field E]
[Algebra F E]
{x : ι → E}
(hx : AlgebraicIndependent F x)
:
AlgebraicIndependent (↥(algebraicClosure F E)) x