Documentation

Mathlib.RingTheory.AlgebraicIndependent.Basic

Algebraic Independence #

This file contains basic results on algebraic independence of a family of elements of an R-algebra

References #

Tags #

transcendence basis, transcendence degree, transcendence

def Algebra.trdeg (R : Type u_2) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] :

The transcendence degree of a commutative algebra A over a commutative ring R is defined to be the maximal cardinality of an R-algebraically independent set in A.

Stacks Tag 030G

Equations
Instances For
    @[simp]
    theorem algebraicIndependent_empty_type_iff {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] [IsEmpty ι] :
    theorem AlgebraicIndependent.algebraMap_injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
    theorem AlgebraicIndependent.linearIndependent {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
    theorem AlgebraicIndependent.injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] :
    theorem AlgebraicIndependent.ne_zero {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] (i : ι) :
    x i 0
    theorem AlgebraicIndependent.map {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Set.InjOn f (Algebra.adjoin R (Set.range x))) :
    theorem AlgebraicIndependent.map' {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Function.Injective f) :
    theorem AlgebraicIndependent.aeval_of_algebraicIndependent {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) {f : ιMvPolynomial ι R} (hf : AlgebraicIndependent R f) :
    AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)

    If x = {x_i : A | i : ι} and f = {f_i : MvPolynomial ι R | i : ι} are algebraically independent over R, then {f_i(x) | i : ι} is also algebraically independent over R. For the partial converse, see AlgebraicIndependent.of_aeval.

    theorem AlgebraicIndependent.of_aeval {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {f : ιMvPolynomial ι R} (H : AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)) :

    If {f_i(x) | i : ι} is algebraically independent over R, then {f_i : MvPolynomial ι R | i : ι} is also algebraically independent over R. In fact, the x = {x_i : A | i : ι} is also transcendental over R provided that R is a field and ι is finite; the proof needs transcendence degree.

    theorem AlgHom.algebraicIndependent_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective f) :
    theorem AlgebraicIndependent.of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :
    @[deprecated AlgebraicIndependent.of_subsingleton (since := "2025-02-07")]
    theorem algebraicIndependent_of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :

    Alias of AlgebraicIndependent.of_subsingleton.

    theorem isTranscendenceBasis_iff_of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] (x : ιA) :
    theorem IsTranscendenceBasis.of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] [Nonempty ι] :
    theorem trdeg_subsingleton {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :
    theorem algebraicIndependent_adjoin {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hs : AlgebraicIndependent R x) :
    AlgebraicIndependent R fun (i : ι) => x i,
    theorem AlgebraicIndependent.restrictScalars {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {K : Type u_3} [CommRing K] [Algebra R K] [Algebra K A] [IsScalarTower R K A] (hinj : Function.Injective (algebraMap R K)) (ai : AlgebraicIndependent K x) :

    A set of algebraically independent elements in an algebra A over a ring K is also algebraically independent over a subring R of K.

    theorem AlgebraicIndependent.of_ringHom_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [FunLike FRS R S] [RingHomClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (H : AlgebraicIndependent S (g x)) (hf : Function.Injective f) (h : (algebraMap S B).comp f = (↑g).comp (algebraMap R A)) :
    theorem AlgebraicIndependent.ringHom_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [FunLike FRS R S] [RingHomClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (H : AlgebraicIndependent R x) (hf : Function.Surjective f) (hg : Function.Injective g) (h : (algebraMap S B).comp f = (↑g).comp (algebraMap R A)) :
    theorem algebraicIndependent_ringHom_iff_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [EquivLike FRS R S] [RingEquivClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (hg : Function.Injective g) (h : (algebraMap S B).comp f = (↑g).comp (algebraMap R A)) :

    Every finite subset of an algebraically independent set is algebraically independent.

    theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {n : } (H : ∀ (s : Finset A), (AlgebraicIndependent R fun (i : { x : A // x s }) => i)s.card n) (s : Set A) :

    If every finite set of algebraically independent element has cardinality at most n, then the same is true for arbitrary sets of algebraically independent elements.

    theorem AlgebraicIndependent.restrict_of_comp_subtype {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} (hs : AlgebraicIndependent R (x Subtype.val)) :
    theorem AlgebraicIndependent.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
    theorem AlgebraicIndependent.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) {t : Set A} (ht : Set.range x = t) :
    theorem IsTranscendenceBasis.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) :
    theorem IsTranscendenceBasis.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) {t : Set A} (ht : Set.range x = t) :
    theorem AlgEquiv.isTranscendenceBasis {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') (hx : IsTranscendenceBasis R x) :
    theorem AlgEquiv.isTranscendenceBasis_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') :
    theorem AlgebraicIndependent.cardinalMk_le_trdeg {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] {ι : Type v} {x : ιA} (hx : AlgebraicIndependent R x) :
    theorem trdeg_le_of_injective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective f) :
    theorem trdeg_le_of_surjective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Surjective f) :
    theorem AlgEquiv.trdeg_eq {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (e : A ≃ₐ[R] A') :
    theorem algebraicIndependent_comp_subtype {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} :
    theorem algebraicIndependent_of_finite_type {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (H : ∀ (t : Set ι), t.FiniteAlgebraicIndependent R fun (i : t) => x i) :
    theorem AlgebraicIndependent.image_of_comp {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {ι' : Type u_4} (s : Set ι) (f : ιι') (g : ι'A) (hs : AlgebraicIndependent R fun (x : s) => g (f x)) :
    AlgebraicIndependent R fun (x : ↑(f '' s)) => g x
    theorem AlgebraicIndependent.image {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {s : Set ι} {f : ιA} (hs : AlgebraicIndependent R fun (x : s) => f x) :
    AlgebraicIndependent R fun (x : ↑(f '' s)) => x
    theorem algebraicIndependent_iUnion_of_directed {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {η : Type u_3} [Nonempty η] {s : ηSet A} (hs : Directed (fun (x1 x2 : Set A) => x1 x2) s) (h : ∀ (i : η), AlgebraicIndependent R Subtype.val) :
    theorem algebraicIndependent_sUnion_of_directed {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {s : Set (Set A)} (hsn : s.Nonempty) (hs : DirectedOn (fun (x1 x2 : Set A) => x1 x2) s) (h : as, AlgebraicIndependent R Subtype.val) :
    theorem exists_maximal_algebraicIndependent {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s t : Set A) (hst : s t) (hs : AlgebraicIndepOn R id s) :
    ∃ (u : Set A), s u Maximal (fun (x : Set A) => AlgebraicIndepOn R id x x t) u
    theorem AlgebraicIndependent.repr_ker {ι : Type u} {R : Type u_2} {A : Type v} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

    The isomorphism between MvPolynomial (Option ι) R and the polynomial ring over the algebra generated by an algebraically independent family.

    Equations
    Instances For
      theorem algebraicIndependent_empty_type {ι : Type u} {A : Type v} {x : ιA} [CommRing A] {K : Type u_3} [Field K] [Algebra K A] [IsEmpty ι] [Nontrivial A] :