Extensions with Finite Transcendence Degree

A field extension L/K has finite transcendence degree if the transcendence degree of L over K is finite. Equivalently, if L is an algebraic extension of a finitely generated field extension of K.

class FinTrdeg (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Prop

A field extension L/K is said to have finite transcendence degree if there is some intermediate extension L/E/K with E/K finitely generated and L/E algebraic.

• exists_fg_isAlgebraic : ∃ (E : IntermediateField K L), E.FG ∧ Algebra.IsAlgebraic (↥E) L

instance instFinTrdegOfIsAlgebraic (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : FinTrdeg K L

instance instFinTrdegOfEssFiniteType (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.EssFiniteType K L] : FinTrdeg K L

theorem finTrdeg_iff_trdeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : FinTrdeg K L ↔ Algebra.trdeg K L < Cardinal.aleph0

theorem FinTrdeg.of_trdeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Algebra.trdeg K L < Cardinal.aleph0 → FinTrdeg K L

Alias of the reverse direction of finTrdeg_iff_trdeg.

theorem trdeg_lt_aleph0 (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FinTrdeg K L] : Algebra.trdeg K L < Cardinal.aleph0

theorem FinTrdeg.trans (K : Type u_3) (E : Type u_4) (L : Type u_5) [Field K] [Field E] [Field L] [Algebra K E] [Algebra K L] [Algebra E L] [IsScalarTower K E L] [FinTrdeg K E] [FinTrdeg E L] : FinTrdeg K L

theorem finite_of_isTranscendenceBasis {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FinTrdeg K L] {ι : Type u_3} {x : ι → L} (hx : IsTranscendenceBasis K x) : Finite ι

theorem finite_of_algebraicIndependent {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FinTrdeg K L] {ι : Type u_3} {x : ι → L} (hx : AlgebraicIndependent K x) : Finite ι

theorem FinTrdeg.of_isTranscendenceBasis {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] {x : ι → L} (hx : IsTranscendenceBasis K x) : FinTrdeg K L

theorem exists_finset_isTranscendenceBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FinTrdeg K L] : ∃ (s : Finset L), IsTranscendenceBasis K Subtype.val