Algebraicity from transcendence degree in towers

This file records consequences of Mathlib's transcendence-degree tower inequality lift_trdeg_add_le for injective towers of commutative rings.

Main results

• 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_one is the case of transcendence degree one.

theorem TauCeti.isAlgebraic_of_trdeg_eq {R : Type u} {S : Type v} {A : Type w} [CommRing R] [Nontrivial R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [FaithfulSMul R S] [FaithfulSMul S A] (h : Algebra.trdeg S A = Algebra.trdeg R A) (hfin : Algebra.trdeg R A < Cardinal.aleph0) : Algebra.IsAlgebraic R S

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] [Nontrivial R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [FaithfulSMul R S] [FaithfulSMul S A] (h : Algebra.trdeg R A = 1) (h' : Algebra.trdeg S A = 1) : Algebra.IsAlgebraic R S

In an injective tower R → S → A, if A has transcendence degree one over both R and S, then S is algebraic over R.