Documentation

Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Algebraic independence persists to the algebraic closure #

Main results #

theorem AlgebraicIndependent.extendScalars {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ιA} (S : Type u_5) [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] :
theorem AlgebraicIndependent.extendScalars_of_isIntegral {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ιA} (S : Type u_5) [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] :
@[deprecated AlgebraicIndependent.extendScalars (since := "2025-02-08")]
theorem AlgebraicIndependent.extendScalars_of_isSimpleRing {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ιA} (S : Type u_5) [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] :

Alias of AlgebraicIndependent.extendScalars.

@[deprecated AlgebraicIndependent.extendScalars (since := "2025-02-08")]
theorem AlgebraicIndependent.subalgebra {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ιA} (S : Type u_5) [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] :

Alias of AlgebraicIndependent.extendScalars.

@[deprecated AlgebraicIndependent.extendScalars_of_isIntegral (since := "2025-02-08")]
theorem AlgebraicIndependent.subalgebra_of_isIntegral {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ιA} (S : Type u_5) [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] :

Alias of AlgebraicIndependent.extendScalars_of_isIntegral.

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] :
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) :
theorem Algebra.IsIntegral.algebraicIndependent_iff {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ιA} (S : Type u_5) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsIntegral R S] :
theorem Algebra.IsIntegral.isTranscendenceBasis_iff {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ιA} (S : Type u_5) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsIntegral R S] :
theorem Algebra.IsAlgebraic.algebraicIndependent_iff {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ιA} (S : Type u_5) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] :
theorem Algebra.IsAlgebraic.isTranscendenceBasis_iff {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ιA} (S : Type u_5) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] :
theorem IntermediateField.isAlgebraic_adjoin_iff {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [Field F] [Field E] [Algebra F E] [Ring S] [Algebra E S] {x : S} :
IsAlgebraic (↥(adjoin F s)) x IsAlgebraic (↥(Algebra.adjoin F s)) x
theorem IntermediateField.isAlgebraic_adjoin_iff_top {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [Field F] [Field E] [Algebra F E] [Ring S] [Algebra E S] :
theorem IntermediateField.isAlgebraic_adjoin_iff_bot {F : Type u_2} {E : Type u_3} {R : Type u_4} {s : Set E} [Field F] [Field E] [Algebra F E] [CommRing R] [Algebra R F] [Algebra R E] [IsScalarTower R F E] :
theorem IntermediateField.transcendental_adjoin_iff {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [Field F] [Field E] [Algebra F E] [Ring S] [Algebra E S] {x : S} :
theorem IntermediateField.algebraicIndependent_adjoin_iff {ι : Type u_1} {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [Field F] [Field E] [Algebra F E] [CommRing S] [Algebra E S] {x : ιS} :
theorem IntermediateField.isTranscendenceBasis_adjoin_iff {ι : Type u_1} {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [Field F] [Field E] [Algebra F E] [CommRing S] [Algebra E S] {x : ιS} :