mathlib3 documentation

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 #

References #

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] [algebra R 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 {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [algebra R A] :
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] [algebra R A] (h : algebraic_independent R x) (p : mv_polynomial ι R) :
@[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] [algebra R 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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R x) (f : ι' ι) (hf : function.injective 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] [algebra R A] (hx : algebraic_independent R 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'] [algebra R A] [algebra R A'] (hx : algebraic_independent R x) {f : A →ₐ[R] A'} (hf_inj : set.inj_on f (algebra.adjoin R (set.range 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'] [algebra R A] [algebra R A'] (hx : algebraic_independent R x) {f : A →ₐ[R] A'} (hf_inj : function.injective f) :
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'] [algebra R A] [algebra R A'] (f : A →ₐ[R] A') (hfv : algebraic_independent R (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'] [algebra R A] [algebra R A'] (f : A →ₐ[R] A') (hf : function.injective f) :
theorem algebraic_independent_of_subsingleton {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [algebra R 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] [algebra R A] (e : ι ι') {f : ι' A} :
theorem algebraic_independent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (e : ι ι') {f : ι' A} {g : ι A} (h : f e = g) :
theorem algebraic_independent.of_subtype_range {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R 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] [algebra R A] {ι : Type u_1} {s : set ι} {f : ι A} (hf : set.inj_on f s) :
algebraic_independent R (λ (x : s), f x) algebraic_independent R (λ (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] [algebra R A] (hs : algebraic_independent R x) :
algebraic_independent R (λ (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] [algebra R A] {K : Type u_2} [comm_ring K] [algebra R K] [algebra K A] [is_scalar_tower R K A] (hinj : function.injective (algebra_map R K)) (ai : algebraic_independent 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.

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

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] [algebra R A] {s : set ι} (hs : algebraic_independent R (x coe)) :
theorem algebraic_independent.mono {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {t s : set A} (h : t s) (hx : algebraic_independent R (λ (x : s), x)) :
algebraic_independent R (λ (x : t), x)
theorem algebraic_independent.to_subtype_range {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {ι : Type u_1} {f : ι A} (hf : algebraic_independent R f) :
theorem algebraic_independent.to_subtype_range' {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {ι : Type u_1} {f : ι A} (hf : algebraic_independent R f) {t : set A} (ht : set.range f = 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] [algebra R A] {s : set ι} :
theorem algebraic_independent_subtype {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {s : set A} :
theorem algebraic_independent_of_finite {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (s : set A) (H : (t : set A), t s t.finite algebraic_independent R (λ (x : t), x)) :
algebraic_independent R (λ (x : s), x)
theorem algebraic_independent.image_of_comp {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {ι : Type u_1} {ι' : Type u_2} (s : set ι) (f : ι ι') (g : ι' A) (hs : algebraic_independent R (λ (x : s), g (f x))) :
algebraic_independent R (λ (x : (f '' s)), g x)
theorem algebraic_independent.image {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {ι : Type u_1} {s : set ι} {f : ι A} (hs : algebraic_independent R (λ (x : s), f x)) :
algebraic_independent R (λ (x : (f '' s)), x)
theorem algebraic_independent_Union_of_directed {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] {η : Type u_1} [nonempty η] {s : η set A} (hs : directed has_subset.subset s) (h : (i : η), algebraic_independent R (λ (x : (s i)), x)) :
algebraic_independent R (λ (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] [algebra R A] {s : set (set A)} (hsn : s.nonempty) (hs : directed_on has_subset.subset s) (h : (a : set A), a s algebraic_independent R (λ (x : a), x)) :
theorem exists_maximal_algebraic_independent {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (s t : set A) (hst : s t) (hs : algebraic_independent R coe) :
@[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] [algebra R A] (hx : algebraic_independent R x) (ᾰ : (algebra.adjoin R (set.range x))) :
(hx.aeval_equiv.symm) ᾰ = ((ring_equiv.of_bijective ((mv_polynomial.aeval x).cod_restrict (algebra.adjoin R (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] [algebra R A] (hx : algebraic_independent R x) (ᾰ : mv_polynomial ι R) :
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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R x) (p : mv_polynomial ι 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] [algebra R A] (hx : algebraic_independent R 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] [algebra R A] (hx : algebraic_independent R x) (p : (algebra.adjoin R (set.range x))) :
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] [algebra R A] (hx : algebraic_independent R x) :
theorem algebraic_independent.repr_ker {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [algebra R A] (hx : algebraic_independent R x) :

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

Equations
theorem algebraic_independent.option_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι A} [comm_ring R] [comm_ring A] [algebra R A] (hx : algebraic_independent R x) (a : A) :
def is_transcendence_basis {ι : Type u_1} (R : Type u_3) {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (x : ι A) :
Prop

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

Equations
theorem algebraic_independent.is_transcendence_basis_iff {ι : Type w} {R : Type u} [comm_ring R] [nontrivial R] {A : Type v} [comm_ring A] [algebra R A] {x : ι A} (i : algebraic_independent R x) :
is_transcendence_basis R x (κ : Type v) (w : κ A), algebraic_independent R w (j : ι κ), w j = x function.surjective j
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] [algebra R A] [nontrivial R] (hx : is_transcendence_basis R x) :
@[simp]
theorem algebraic_independent_empty_type {ι : Type u_1} {K : Type u_4} {A : Type u_5} {x : ι A} [comm_ring A] [field K] [algebra K A] [is_empty ι] [nontrivial A] :