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
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)
:
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.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)
:
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)
:
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.
Equations
- AlgebraicIndependent.matroid R A = (AlgebraicIndependent.indepMatroid✝ R A).matroid.copyBase Set.univ (fun (s : Set A) => IsTranscendenceBasis R Subtype.val) ⋯ ⋯
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]
:
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}
:
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}
:
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)
:
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}
:
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}
:
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}
:
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
AlgebraicIndependent.matroid_spanning_iff_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}
:
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)
:
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)
:
@[simp]
@[simp]
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]
:
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]
: