# Algebraic Independence #

This file defines algebraic independence of a family of element of an R algebra.

## Main definitions #

• AlgebraicIndependent - AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

• AlgebraicIndependent.repr - The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.

## TODO #

Define the transcendence degree and show it is independent of the choice of a transcendence basis.

## Tags #

transcendence basis, transcendence degree, transcendence

def AlgebraicIndependent {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ιA) [] [] [Algebra R A] :

AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

Equations
Instances For
theorem algebraicIndependent_iff_ker_eq_bot {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] :
RingHom.ker .toRingHom =
theorem algebraicIndependent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] :
∀ (p : ), p = 0p = 0
theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (h : ) (p : ) :
p = 0p = 0
theorem algebraicIndependent_iff_injective_aeval {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] :
@[simp]
theorem algebraicIndependent_empty_type_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] [] :
theorem AlgebraicIndependent.algebraMap_injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
theorem AlgebraicIndependent.linearIndependent {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
theorem AlgebraicIndependent.injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) [] :
theorem AlgebraicIndependent.ne_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) [] (i : ι) :
x i 0
theorem AlgebraicIndependent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (f : ι'ι) (hf : ) :
theorem AlgebraicIndependent.coe_range {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
AlgebraicIndependent R Subtype.val
theorem AlgebraicIndependent.map {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ιA} [] [] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : ) {f : A →ₐ[R] A'} (hf_inj : Set.InjOn f ()) :
theorem AlgebraicIndependent.map' {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ιA} [] [] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : ) {f : A →ₐ[R] A'} (hf_inj : ) :
theorem AlgebraicIndependent.of_comp {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ιA} [] [] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f x)) :
theorem AlgHom.algebraicIndependent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ιA} [] [] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : ) :
theorem algebraicIndependent_of_subsingleton {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] [] :
theorem algebraicIndependent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] (e : ι ι') {f : ι'A} :
theorem algebraicIndependent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] (e : ι ι') {f : ι'A} {g : ιA} (h : f e = g) :
theorem algebraicIndependent_subtype_range {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {f : ιA} (hf : ) :
AlgebraicIndependent R Subtype.val
theorem AlgebraicIndependent.of_subtype_range {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {f : ιA} (hf : ) :
AlgebraicIndependent R Subtype.val

Alias of the forward direction of algebraicIndependent_subtype_range.

theorem algebraicIndependent_image {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {s : Set ι} {f : ιA} (hf : ) :
(AlgebraicIndependent R fun (x : s) => f x) AlgebraicIndependent R fun (x : (f '' s)) => x
theorem algebraicIndependent_adjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hs : ) :
AlgebraicIndependent R fun (i : ι) => x i,
theorem AlgebraicIndependent.restrictScalars {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] {K : Type u_9} [] [Algebra R K] [Algebra K A] [] (hinj : Function.Injective ()) (ai : ) :

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_finset_map_embedding_subtype {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] (s : Set A) (li : AlgebraicIndependent R Subtype.val) (t : Finset s) :
AlgebraicIndependent R Subtype.val

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

theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {n : } (H : ∀ (s : ), (AlgebraicIndependent R fun (i : { x : A // x s }) => i)s.card n) (s : Set A) :
AlgebraicIndependent R Subtype.val n

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_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] {s : Set ι} (hs : AlgebraicIndependent R (x Subtype.val)) :
AlgebraicIndependent R (s.restrict x)
theorem algebraicIndependent_empty_iff (R : Type u_3) (A : Type u_5) [] [] [Algebra R A] :
theorem AlgebraicIndependent.mono {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {t : Set A} {s : Set A} (h : t s) (hx : AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
theorem AlgebraicIndependent.to_subtype_range {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {f : ιA} (hf : ) :
AlgebraicIndependent R Subtype.val
theorem AlgebraicIndependent.to_subtype_range' {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {f : ιA} (hf : ) {t : Set A} (ht : = t) :
AlgebraicIndependent R Subtype.val
theorem algebraicIndependent_comp_subtype {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] {s : Set ι} :
AlgebraicIndependent R (x Subtype.val) p, p = 0p = 0
theorem algebraicIndependent_subtype {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {s : Set A} :
AlgebraicIndependent R Subtype.val p, () p = 0p = 0
theorem algebraicIndependent_of_finite {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] (s : Set A) (H : ts, t.FiniteAlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
theorem AlgebraicIndependent.image_of_comp {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {ι' : Type u_10} (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_3} {A : Type u_5} [] [] [Algebra R A] {ι : Type u_9} {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_3} {A : Type u_5} [] [] [Algebra R A] {η : Type u_9} [] {s : ηSet A} (hs : Directed (fun (x x_1 : Set A) => x x_1) s) (h : ∀ (i : η), AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
theorem algebraicIndependent_sUnion_of_directed {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] {s : Set (Set A)} (hsn : s.Nonempty) (hs : DirectedOn (fun (x x_1 : Set A) => x x_1) s) (h : as, AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
theorem exists_maximal_algebraicIndependent {R : Type u_3} {A : Type u_5} [] [] [Algebra R A] (s : Set A) (t : Set A) (hst : s t) (hs : AlgebraicIndependent R Subtype.val) :
∃ (u : Set A), AlgebraicIndependent R Subtype.val s u u t ∀ (x : Set A), AlgebraicIndependent R Subtype.valu xx tx = u
@[simp]
theorem AlgebraicIndependent.aevalEquiv_apply_coe {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (a : ) :
(hx.aevalEquiv a) = a
@[simp]
theorem AlgebraicIndependent.aevalEquiv_symm_apply {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (b : ()) :
hx.aevalEquiv.symm b =
def AlgebraicIndependent.aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
≃ₐ[R] ()

Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.

Equations
Instances For
theorem AlgebraicIndependent.algebraMap_aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (p : ) :
(algebraMap (()) A) (hx.aevalEquiv p) = p
def AlgebraicIndependent.repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
() →ₐ[R]

The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.

Equations
• hx.repr = hx.aevalEquiv.symm
Instances For
@[simp]
theorem AlgebraicIndependent.aeval_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (p : ()) :
(hx.repr p) = p
theorem AlgebraicIndependent.aeval_comp_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
.comp hx.repr = ().val
theorem AlgebraicIndependent.repr_ker {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
RingHom.ker hx.repr =
def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :

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

Equations
• hx.mvPolynomialOptionEquivPolynomialAdjoin = .toRingEquiv.trans (Polynomial.mapEquiv hx.aevalEquiv.toRingEquiv)
Instances For
@[simp]
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (y : MvPolynomial () R) :
hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (hx.aevalEquiv) ((MvPolynomial.aeval fun (o : ) => o.elim Polynomial.X fun (s : ι) => Polynomial.C ()) y)
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (r : R) :
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) = Polynomial.C ((algebraMap R ()) r)
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) :
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (i : ι) :
hx.mvPolynomialOptionEquivPolynomialAdjoin () = Polynomial.C (hx.aevalEquiv ())
theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (a : A) :
(()).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = (MvPolynomial.aeval fun (o : ) => o.elim a x)
theorem AlgebraicIndependent.option_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] (hx : ) (a : A) :
(AlgebraicIndependent R fun (o : ) => o.elim a x) ¬IsAlgebraic (()) a
def IsTranscendenceBasis {ι : Type u_1} (R : Type u_3) {A : Type u_5} [] [] [Algebra R A] (x : ιA) :

A family is a transcendence basis if it is a maximal algebraically independent subset.

Equations
Instances For
theorem exists_isTranscendenceBasis (R : Type u_3) {A : Type u_5} [] [] [Algebra R A] (h : Function.Injective ()) :
∃ (s : Set A), IsTranscendenceBasis R Subtype.val
theorem AlgebraicIndependent.isTranscendenceBasis_iff {ι : Type w} {R : Type u} [] [] {A : Type v} [] [Algebra R A] {x : ιA} (i : ) :
∀ (κ : Type v) (w : κA), ∀ (j : ικ), w j = x
theorem IsTranscendenceBasis.isAlgebraic {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [] [] [Algebra R A] [] (hx : ) :
theorem algebraicIndependent_empty_type {ι : Type u_1} {K : Type u_4} {A : Type u_5} {x : ιA} [] [] [Algebra K A] [] [] :
theorem algebraicIndependent_empty {K : Type u_4} {A : Type u_5} [] [] [Algebra K A] [] :
AlgebraicIndependent K Subtype.val