Transcendence basis #
This file defines the transcendence basis as a maximal algebraically independent subset.
Main results #
exists_isTranscendenceBasis: a ring extension has a transcendence basisIsTranscendenceBasis.lift_cardinalMk_eq: any two transcendence bases of a domain have the same cardinality.
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_superset
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set A}
(hs : AlgebraicIndepOn R id s)
:
∃ (t : Set A), s ⊆ t ∧ IsTranscendenceBasis R Subtype.val
theorem
exists_isTranscendenceBasis
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
:
∃ (s : Set A), IsTranscendenceBasis R Subtype.val
theorem
exists_isTranscendenceBasis'
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
:
∃ (ι : Type w) (x : ι → A), IsTranscendenceBasis R x
Type version of exists_isTranscendenceBasis.
theorem
trdeg_eq_iSup_cardinalMk_isTranscendenceBasis
(R : Type u_1)
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
:
Algebra.trdeg R A = ⨆ (ι : { s : Set A // IsTranscendenceBasis R Subtype.val }), Cardinal.mk ↑↑ι
theorem
AlgebraicIndependent.isTranscendenceBasis_iff
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(i : AlgebraicIndependent R x)
:
IsTranscendenceBasis R x ↔ ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Function.Surjective j
theorem
IsTranscendenceBasis.isAlgebraic
{ι : Type u}
{R : Type u_1}
{A : Type w}
{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
AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(ind : AlgebraicIndependent R x)
:
IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
theorem
isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
:
IsTranscendenceBasis R x ↔ AlgebraicIndependent R x ∧ Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
theorem
IsTranscendenceBasis.algebraMap_comp
{ι : Type u}
{R : Type u_1}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[Nontrivial R]
[NoZeroDivisors S]
[Algebra.IsAlgebraic S A]
[FaithfulSMul S A]
{x : ι → S}
(hx : IsTranscendenceBasis R x)
:
IsTranscendenceBasis R (⇑(algebraMap S A) ∘ x)
theorem
IsTranscendenceBasis.isAlgebraic_iff
{R : Type u_1}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[IsDomain S]
[NoZeroDivisors A]
{ι : Type u_2}
{v : ι → A}
(hv : IsTranscendenceBasis R v)
:
Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i)
theorem
IsTranscendenceBasis.polynomial
(ι : Type u)
(R : Type u_1)
[CommRing R]
[Nonempty ι]
[Subsingleton ι]
:
IsTranscendenceBasis R fun (x : ι) => Polynomial.X
theorem
IsTranscendenceBasis.sumElim_comp
{ι : Type u}
{ι' : Type u'}
{R : Type u_1}
{S : Type v}
{A : Type w}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[NoZeroDivisors A]
{x : ι → S}
{y : ι' → A}
(hx : IsTranscendenceBasis R x)
(hy : IsTranscendenceBasis S y)
:
IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))
theorem
IsTranscendenceBasis.isEmpty_iff_isAlgebraic
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(hx : IsTranscendenceBasis R x)
:
IsEmpty ι ↔ Algebra.IsAlgebraic R A
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}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
(hx : IsTranscendenceBasis R x)
:
Nonempty ι ↔ Algebra.Transcendental R A
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}
{F : Type u_2}
{E : Type u_3}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : IsTranscendenceBasis F x)
:
Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (Set.range x))) E
def
AlgebraicIndependent.matroid
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
:
Matroid A
If R is a commutative ring and A is a commutative R-algebra with injective algebra map
and no zero-divisors, then the R-algebraic independent subsets of A form a matroid.
Instances For
instance
AlgebraicIndependent.instFinitaryMatroid
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
:
@[simp]
theorem
AlgebraicIndependent.matroid_e
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
:
theorem
AlgebraicIndependent.matroid_cRank_eq
(R : Type u_1)
(A : Type w)
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
:
(matroid R A).cRank = Algebra.trdeg R A
theorem
AlgebraicIndependent.matroid_indep_iff
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
{s : Set A}
:
(matroid R A).Indep s ↔ AlgebraicIndepOn R id s
theorem
AlgebraicIndependent.matroid_isBase_iff
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
{s : Set A}
:
(matroid R A).IsBase s ↔ IsTranscendenceBasis R Subtype.val
theorem
AlgebraicIndependent.matroid_isBasis_iff
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[IsDomain A]
{s t : Set A}
:
(matroid R A).IsBasis s t ↔ AlgebraicIndepOn R id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(Algebra.adjoin R s)) a
theorem
AlgebraicIndependent.matroid_isBasis_iff_of_subsingleton
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[Subsingleton A]
{s t : Set A}
:
theorem
AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[NoZeroDivisors A]
{s t : Set A}
{a : A}
(h : (matroid R A).IsBasis s t)
:
IsAlgebraic (↥(Algebra.adjoin R s)) a ↔ IsAlgebraic (↥(Algebra.adjoin R t)) a
theorem
AlgebraicIndependent.matroid_closure_eq
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[IsDomain A]
{s : Set A}
:
(matroid R A).closure s = ↑(Subalgebra.algebraicClosure (↥(Algebra.adjoin R s)) A)
theorem
AlgebraicIndependent.matroid_isFlat_iff
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[IsDomain A]
{s : Set A}
:
(matroid R A).IsFlat s ↔ ∃ (S : Subalgebra R A), ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
theorem
AlgebraicIndependent.matroid_spanning_iff
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[IsDomain A]
{s : Set A}
:
(matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A
theorem
AlgebraicIndependent.matroid_isFlat_of_subsingleton
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[Subsingleton A]
(s : Set A)
:
theorem
AlgebraicIndependent.matroid_closure_of_subsingleton
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[FaithfulSMul R A]
[Subsingleton A]
(s : Set A)
:
theorem
exists_isTranscendenceBasis_between
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
(s t : Set A)
(hst : s ⊆ t)
(hs : AlgebraicIndepOn R id s)
[ht : Algebra.IsAlgebraic (↥(Algebra.adjoin R t)) A]
:
∃ (u : Set A), s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
If s ⊆ t are subsets in an R-algebra A such that s is algebraically independent over
R, and A is algebraic over the R-algebra generated by t, then there is a transcendence
basis of A over R between s and t, provided that A is a domain.
This may fail if only R is assumed to be a domain but A is not, because of failure of
transitivity of algebraicity: there may exist a : A such that S := R[a] is algebraic over
R and A is algebraic over S, but A nonetheless contains a transcendental element over R.
The only R-algebraically independent subset of {a} is ∅, which is not a transcendence basis.
See the docstring of IsAlgebraic.restrictScalars_of_isIntegral for an example.
theorem
exists_isTranscendenceBasis_subset
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
[FaithfulSMul R A]
(s : Set A)
[Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A]
:
∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
theorem
isAlgebraic_iff_exists_isTranscendenceBasis_subset
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[IsDomain A]
[FaithfulSMul R A]
{s : Set A}
:
Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
theorem
IsTranscendenceBasis.lift_cardinalMk_eq_trdeg
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
(hx : IsTranscendenceBasis R x)
:
theorem
IsTranscendenceBasis.cardinalMk_eq_trdeg
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
{ι : Type w}
{x : ι → A}
(hx : IsTranscendenceBasis R x)
:
Cardinal.mk ι = Algebra.trdeg R A
theorem
IsTranscendenceBasis.lift_cardinalMk_eq
{ι : Type u}
{ι' : Type u'}
{R : Type u_1}
{A : Type w}
{x : ι → A}
{y : ι' → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
(hx : IsTranscendenceBasis R x)
(hy : IsTranscendenceBasis R y)
:
Any two transcendence bases of a domain A have the same cardinality.
May fail if A is not a domain; see https://mathoverflow.net/a/144580.
theorem
IsTranscendenceBasis.cardinalMk_eq
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
{ι' : Type u}
{y : ι' → A}
(hx : IsTranscendenceBasis R x)
(hy : IsTranscendenceBasis R y)
:
Cardinal.mk ι = Cardinal.mk ι'
@[simp]
theorem
MvPolynomial.trdeg_of_isDomain
{ι : Type u}
{S : Type v}
[CommRing S]
[IsDomain S]
:
Algebra.trdeg S (MvPolynomial ι S) = Cardinal.lift.{v, u} (Cardinal.mk ι)
@[simp]
theorem
Polynomial.trdeg_of_isDomain
{R : Type u_1}
[CommRing R]
[IsDomain R]
:
Algebra.trdeg R (Polynomial R) = 1
theorem
trdeg_lt_aleph0
{R : Type u_1}
{S : Type v}
[CommRing R]
[CommRing S]
[Algebra R S]
[IsDomain R]
[fin : Algebra.FiniteType R S]
:
theorem
Algebra.IsAlgebraic.isDomain_of_adjoin_range
(R : Type u_1)
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
[NoZeroDivisors A]
[Algebra.IsAlgebraic (↥(adjoin R s)) A]
:
IsDomain A
theorem
Algebra.IsAlgebraic.trdeg_le_cardinalMk
(R : Type u_1)
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
[NoZeroDivisors A]
[alg : Algebra.IsAlgebraic (↥(adjoin R s)) A]
:
theorem
Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg_of_finite
{ι : Type u}
(R : Type u_1)
{A : Type w}
(x : ι → A)
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
[FaithfulSMul R A]
[Finite ι]
[alg : Algebra.IsAlgebraic (↥(adjoin R (Set.range x))) A]
(le : Cardinal.lift.{w, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, w} (trdeg R A))
:
theorem
Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg_of_finite
(R : Type u_1)
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
[FaithfulSMul R A]
{ι : Type w}
[Finite ι]
(x : ι → A)
[Algebra.IsAlgebraic (↥(adjoin R (Set.range x))) A]
(le : Cardinal.mk ι ≤ trdeg R A)
:
theorem
Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg
{ι : Type u}
(R : Type u_1)
{A : Type w}
(x : ι → A)
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
[FaithfulSMul R A]
[Algebra.IsAlgebraic (↥(adjoin R (Set.range x))) A]
(fin : trdeg R A < Cardinal.aleph0)
(le : Cardinal.lift.{w, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, w} (trdeg R A))
:
theorem
Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg
(R : Type u_1)
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[NoZeroDivisors A]
[FaithfulSMul R A]
{ι : Type w}
(x : ι → A)
[Algebra.IsAlgebraic (↥(adjoin R (Set.range x))) A]
(fin : trdeg R A < Cardinal.aleph0)
(le : Cardinal.mk ι ≤ trdeg R A)
:
theorem
AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
(hx : AlgebraicIndependent R x)
(fin : Algebra.trdeg R A < Cardinal.aleph0)
(le : Cardinal.lift.{u, w} (Algebra.trdeg R A) ≤ Cardinal.lift.{w, u} (Cardinal.mk ι))
:
theorem
AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
{ι : Type w}
{x : ι → A}
(hx : AlgebraicIndependent R x)
(fin : Algebra.trdeg R A < Cardinal.aleph0)
(le : Algebra.trdeg R A ≤ Cardinal.mk ι)
:
theorem
AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le_of_finite
{ι : Type u}
{R : Type u_1}
{A : Type w}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
[Finite ι]
(hx : AlgebraicIndependent R x)
(le : Cardinal.lift.{u, w} (Algebra.trdeg R A) ≤ Cardinal.lift.{w, u} (Cardinal.mk ι))
:
theorem
AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le_of_finite
{R : Type u_1}
{A : Type w}
[CommRing R]
[CommRing A]
[Algebra R A]
[Nontrivial R]
[NoZeroDivisors A]
{ι : Type w}
[Finite ι]
{x : ι → A}
(hx : AlgebraicIndependent R x)
(le : Algebra.trdeg R A ≤ Cardinal.mk ι)
:
theorem
lift_trdeg_add_eq
(R : Type u_1)
(S : Type v)
(A : Type w)
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[Nontrivial R]
[NoZeroDivisors A]
[FaithfulSMul R S]
[FaithfulSMul S A]
:
Cardinal.lift.{w, v} (Algebra.trdeg R S) + Cardinal.lift.{v, w} (Algebra.trdeg S A) = Cardinal.lift.{v, w} (Algebra.trdeg R A)
theorem
trdeg_add_eq
(R : Type u_1)
(S : Type v)
[CommRing R]
[CommRing S]
[Algebra R S]
[Nontrivial R]
{A : Type v}
[CommRing A]
[NoZeroDivisors A]
[Algebra R A]
[Algebra S A]
[FaithfulSMul R S]
[FaithfulSMul S A]
[IsScalarTower R S A]
:
Algebra.trdeg R S + Algebra.trdeg S A = Algebra.trdeg R A
theorem
IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_diff
{ι : Type u}
{R : Type u_1}
{S : Type v}
[CommRing R]
[CommRing S]
[Algebra R S]
[FaithfulSMul R S]
[NoZeroDivisors S]
(s : Set ι)
(i j : ι)
(v : ι → S)
(hj : j ∈ insert i s)
(H₁ : IsTranscendenceBasis R fun (x : ↑s) => v ↑x)
(H₂ : IsAlgebraic (↥(Algebra.adjoin R (v '' (insert i s \ {j})))) (v j))
:
IsTranscendenceBasis R fun (x : ↑(insert i s \ {j})) => v ↑x
If s is a transcendence basis and j is algebraic over s ∪ {i} \ {j},
then s ∪ {i} \ {j} is also a transcendence basis.
theorem
IsTranscendenceBasis.of_isAlgebraic_adjoin_image_compl
{ι : Type u}
{R : Type u_1}
{S : Type v}
[CommRing R]
[CommRing S]
[Algebra R S]
[FaithfulSMul R S]
[NoZeroDivisors S]
(i j : ι)
(v : ι → S)
(H₁ : IsTranscendenceBasis R fun (x : { x : ι // x ≠ i }) => v ↑x)
(H₂ : IsAlgebraic (↥(Algebra.adjoin R (v '' {j}ᶜ))) (v j))
:
IsTranscendenceBasis R fun (x : { x : ι // x ≠ j }) => v ↑x