mathlib documentation

ring_theory.algebraic_independent

Algebraic Independence #

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_ker_eq_bot {ι : 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_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [comm_ring R] [comm_ring A] [algebra R A] :
algebraic_independent R x ∀ (p : mv_polynomial ι R), (mv_polynomial.aeval x) p = 0p = 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] [algebra R A] (h : algebraic_independent R x) (p : mv_polynomial ι R) :
(mv_polynomial.aeval x) p = 0p = 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] [algebra R 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] [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_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) :
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 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.

theorem algebraic_independent_finset_map_embedding_subtype {R : Type u_3} {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (s : set A) (li : algebraic_independent R 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] [algebra R A] {n : } (H : ∀ (s : finset A), algebraic_independent R (λ (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] [algebra R A] {s : set ι} (hs : algebraic_independent R (x coe)) :
theorem algebraic_independent_empty_iff (R : Type u_3) (A : Type u_5) [comm_ring R] [comm_ring A] [algebra R A] :
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} :
algebraic_independent R (λ (x : s), x) ∀ (p : mv_polynomial A R), p mv_polynomial.supported R s(mv_polynomial.aeval id) p = 0p = 0
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 st.finitealgebraic_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 salgebraic_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) :
∃ (u : set A), algebraic_independent R coe s u u t ∀ (x : set A), algebraic_independent R coeu xx tx = 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] [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) _).inv_fun
@[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) :
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] [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 exists_is_transcendence_basis (R : Type u_3) {A : Type u_5} [comm_ring R] [comm_ring A] [algebra R A] (h : function.injective (algebra_map R A)) :
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 = xfunction.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] :
theorem algebraic_independent_empty {K : Type u_4} {A : Type u_5} [comm_ring A] [field K] [algebra K A] [nontrivial A] :