Transcendence degree in towers #
This file records consequences of algebraic independence and Mathlib's transcendence-degree
tower inequality lift_trdeg_add_le for towers of commutative rings.
Main results #
TauCeti.trdeg_eq_of_isAlgebraic_base: an injective algebraic extension of the base ring preserves transcendence degree in any commutative algebra over the larger base.TauCeti.isAlgebraic_of_trdeg_eq: if the top ring has the same finite transcendence degree over the bottom and middle rings, then the middle ring is algebraic over the bottom ring;TauCeti.isAlgebraic_of_trdeg_eq_oneis the case of transcendence degree one.
theorem
TauCeti.trdeg_eq_of_isAlgebraic_base
{R : Type u}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
[NoZeroDivisors S]
[FaithfulSMul R S]
[Algebra.IsAlgebraic R S]
:
An injective algebraic extension of the base ring preserves transcendence degree, provided the larger base has no zero divisors. The top algebra may have zero divisors, and its structure map need not be injective.
theorem
TauCeti.isAlgebraic_of_trdeg_eq
{R : Type u}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
[Nontrivial R]
[FaithfulSMul R S]
[FaithfulSMul S A]
(h : Algebra.trdeg S A = Algebra.trdeg R A)
(hfin : Algebra.trdeg R A < Cardinal.aleph0)
:
In an injective tower R → S → A, if A has the same finite transcendence degree over
R and S, then S is algebraic over R. Finiteness allows cancellation in the
transcendence-degree tower inequality.
theorem
TauCeti.isAlgebraic_of_trdeg_eq_one
{R : Type u}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
[Nontrivial R]
[FaithfulSMul R S]
[FaithfulSMul S A]
(h : Algebra.trdeg R A = 1)
(h' : Algebra.trdeg S A = 1)
:
In an injective tower R → S → A, if A has transcendence degree one over both
R and S, then S is algebraic over R.