Transcendence basis #
This file defines the transcendence basis as a maximal algebraically independent subset.
Main results #
exists_isTranscendenceBasis: a ring extension has a transcendence basis
References #
TODO #
Define the transcendence degree and show it is independent of the choice of a transcendence basis.
Tags #
transcendence basis, transcendence degree, transcendence
theorem
exists_isTranscendenceBasis
(R : Type u_3)
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
(h : Function.Injective ⇑(algebraMap R A))
:
∃ (s : Set A), IsTranscendenceBasis R Subtype.val
theorem
exists_isTranscendenceBasis'
(R : Type u)
{A : Type v}
[CommRing R]
[CommRing A]
[Algebra R A]
(h : Function.Injective ⇑(algebraMap R A))
:
∃ (ι : Type v) (x : ι → A), IsTranscendenceBasis R x
Type version of exists_isTranscendenceBasis.
theorem
AlgebraicIndependent.isTranscendenceBasis_iff
{ι : Type w}
{R : Type u}
[CommRing R]
[Nontrivial R]
{A : Type v}
[CommRing A]
[Algebra R A]
{x : ι → A}
(i : AlgebraicIndependent R x)
:
IsTranscendenceBasis R x ↔ ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Function.Surjective j
theorem
IsTranscendenceBasis.isAlgebraic
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(hx : IsTranscendenceBasis R x)
:
Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
theorem
IsTranscendenceBasis.isEmpty_iff_isAlgebraic
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(hx : IsTranscendenceBasis R x)
:
If x is a transcendence basis of A/R, then it is empty if and only if
A/R is algebraic.
theorem
IsTranscendenceBasis.nonempty_iff_transcendental
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(hx : IsTranscendenceBasis R x)
:
If x is a transcendence basis of A/R, then it is not empty if and only if
A/R is transcendental.
theorem
IsTranscendenceBasis.isAlgebraic_field
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : IsTranscendenceBasis F x)
:
Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (Set.range x))) E