# mathlib3documentation

ring_theory.algebraic_independent

# Algebraic Independence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• algebraic_independent - algebraic_independent 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.

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

## TODO #

Prove that a ring is an algebraic extension of the subalgebra generated by a transcendence basis.

## Tags #

transcendence basis, transcendence degree, transcendence

def algebraic_independent {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ι A) [comm_ring R] [comm_ring A] [ A] :
Prop

algebraic_independent 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
theorem algebraic_independent_iff_ker_eq_bot {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] :
theorem algebraic_independent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] :
(p : R), p = 0 p = 0
theorem algebraic_independent.eq_zero_of_aeval_eq_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (h : x) (p : R) :
p = 0 p = 0
theorem algebraic_independent_iff_injective_aeval {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] :
@[simp]
theorem algebraic_independent_empty_type_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] [is_empty ι] :
theorem algebraic_independent.algebra_map_injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
theorem algebraic_independent.linear_independent {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
@[protected]
theorem algebraic_independent.injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) [nontrivial R] :
theorem algebraic_independent.ne_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) [nontrivial R] (i : ι) :
x i 0
theorem algebraic_independent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (f : ι' ι) (hf : function.injective f) :
(x f)
theorem algebraic_independent.coe_range {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
theorem algebraic_independent.map {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι A} [comm_ring R] [comm_ring A] [comm_ring A'] [ A] [ A'] (hx : x) {f : A →ₐ[R] A'} (hf_inj : (set.range x))) :
(f x)
theorem algebraic_independent.map' {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι A} [comm_ring R] [comm_ring A] [comm_ring A'] [ A] [ A'] (hx : x) {f : A →ₐ[R] A'} (hf_inj : function.injective f) :
(f x)
theorem algebraic_independent.of_comp {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι A} [comm_ring R] [comm_ring A] [comm_ring A'] [ A] [ A'] (f : A →ₐ[R] A') (hfv : (f x)) :
theorem alg_hom.algebraic_independent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι A} [comm_ring R] [comm_ring A] [comm_ring A'] [ A] [ A'] (f : A →ₐ[R] A') (hf : function.injective f) :
(f x)
theorem algebraic_independent_of_subsingleton {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] [subsingleton R] :
theorem algebraic_independent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (e : ι ι') {f : ι' A} :
(f e)
theorem algebraic_independent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (e : ι ι') {f : ι' A} {g : ι A} (h : f e = g) :
theorem algebraic_independent_subtype_range {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {f : ι A} (hf : function.injective f) :
theorem algebraic_independent.of_subtype_range {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {f : ι A} (hf : function.injective f) :

Alias of the forward direction of algebraic_independent_subtype_range.

theorem algebraic_independent_image {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {s : set ι} {f : ι A} (hf : s) :
(λ (x : s), f x) (λ (x : (f '' s)), x)
theorem algebraic_independent_adjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hs : x) :
(λ (i : ι), x i, _⟩)
theorem algebraic_independent.restrict_scalars {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] {K : Type u_2} [comm_ring K] [ K] [ A] [ A] (hinj : function.injective K)) (ai : 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 algebraic_independent_finset_map_embedding_subtype {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (s : set A) (li : coe) (t : finset s) :

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

theorem algebraic_independent_bounded_of_finset_algebraic_independent_bounded {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {n : } (H : (s : finset A), (λ (i : 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 algebraic_independent.restrict_of_comp_subtype {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] {s : set ι} (hs : (x coe)) :
(s.restrict x)
theorem algebraic_independent_empty_iff (R : Type u_3) (A : Type u_5) [comm_ring R] [comm_ring A] [ A] :
(λ (x : ), x)
theorem algebraic_independent.mono {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {t s : set A} (h : t s) (hx : (λ (x : s), x)) :
(λ (x : t), x)
theorem algebraic_independent.to_subtype_range {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {f : ι A} (hf : f) :
theorem algebraic_independent.to_subtype_range' {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {f : ι A} (hf : f) {t : set A} (ht : = t) :
theorem algebraic_independent_comp_subtype {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] {s : set ι} :
(x coe) (p : R), p = 0 p = 0
theorem algebraic_independent_subtype {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {s : set A} :
(λ (x : s), x) (p : R), = 0 p = 0
theorem algebraic_independent_of_finite {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (s : set A) (H : (t : set A), t s t.finite (λ (x : t), x)) :
(λ (x : s), x)
theorem algebraic_independent.image_of_comp {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {ι' : Type u_2} (s : set ι) (f : ι ι') (g : ι' A) (hs : (λ (x : s), g (f x))) :
(λ (x : (f '' s)), g x)
theorem algebraic_independent.image {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {ι : Type u_1} {s : set ι} {f : ι A} (hs : (λ (x : s), f x)) :
(λ (x : (f '' s)), x)
theorem algebraic_independent_Union_of_directed {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {η : Type u_1} [nonempty η] {s : η set A} (hs : s) (h : (i : η), (λ (x : (s i)), x)) :
(λ (x : (i : η), s i), x)
theorem algebraic_independent_sUnion_of_directed {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] {s : set (set A)} (hsn : s.nonempty) (hs : s) (h : (a : set A), a s (λ (x : a), x)) :
(λ (x : ⋃₀ s), x)
theorem exists_maximal_algebraic_independent {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (s t : set A) (hst : s t) (hs : coe) :
(u : set A), s u u t (x : set A), u x x t x = u
@[simp]
theorem algebraic_independent.aeval_equiv_symm_apply {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (ᾰ : (set.range x))) :
(hx.aeval_equiv.symm) ᾰ = ((ring_equiv.of_bijective (set.range x)) algebraic_independent.aeval_equiv._proof_1) _).symm)
@[simp]
theorem algebraic_independent.aeval_equiv_apply_coe {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (ᾰ : R) :
((hx.aeval_equiv) ᾰ) =
noncomputable def algebraic_independent.aeval_equiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :

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

Equations
@[simp]
theorem algebraic_independent.algebra_map_aeval_equiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (p : R) :
noncomputable def algebraic_independent.repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :

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

Equations
@[simp]
theorem algebraic_independent.aeval_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (p : (set.range x))) :
((hx.repr) p) = p
theorem algebraic_independent.aeval_comp_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
hx.repr = (set.range x)).val
theorem algebraic_independent.repr_ker {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
noncomputable def algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :

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

Equations
@[simp]
theorem algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin_apply {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (y : R) :
= ((mv_polynomial.aeval (λ (o : option ι), (λ (s : ι), o)) y)
@[simp]
theorem algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin_C {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (r : R) :
@[simp]
theorem algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin_X_none {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) :
@[simp]
theorem algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin_X_some {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (i : ι) :
theorem algebraic_independent.aeval_comp_mv_polynomial_option_equiv_polynomial_adjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (a : A) :
= (mv_polynomial.aeval (λ (o : option ι), x o))
theorem algebraic_independent.option_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] (hx : x) (a : A) :
(λ (o : option ι), x o) ¬is_algebraic (set.range x)) a
def is_transcendence_basis {ι : Type u_1} (R : Type u_3) {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (x : ι A) :
Prop

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

Equations
theorem exists_is_transcendence_basis (R : Type u_3) {A : Type u_5} [comm_ring R] [comm_ring A] [ A] (h : function.injective A)) :
(s : set A),
theorem algebraic_independent.is_transcendence_basis_iff {ι : Type w} {R : Type u} [comm_ring R] [nontrivial R] {A : Type v} [comm_ring A] [ A] {x : ι A} (i : x) :
(κ : Type v) (w : κ A), (j : ι κ), w j = x
theorem is_transcendence_basis.is_algebraic {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [ A] [nontrivial R] (hx : x) :
A
@[simp]
theorem algebraic_independent_empty_type {ι : Type u_1} {K : Type u_4} {A : Type u_5} {x : ι A} [comm_ring A] [field K] [ A] [is_empty ι] [nontrivial A] :
theorem algebraic_independent_empty {K : Type u_4} {A : Type u_5} [comm_ring A] [field K] [ A] [nontrivial A] :