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 xstates the family of elementsxis algebraically independent overR, 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.
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] :
algebraic_independent R x ↔ ∀ (p : mv_polynomial ι R), ⇑(mv_polynomial.aeval x) 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]
[algebra R A]
(h : algebraic_independent R x)
(p : mv_polynomial ι R) :
⇑(mv_polynomial.aeval x) p = 0 → p = 0
@[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 ι] :
algebraic_independent R x ↔ function.injective ⇑(algebra_map R A)
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) :
algebraic_independent R (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]
[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))) :
algebraic_independent R (⇑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']
[algebra R A]
[algebra R A']
(hx : algebraic_independent R x)
{f : A →ₐ[R] A'}
(hf_inj : function.injective ⇑f) :
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) :
algebraic_independent R (⇑f ∘ x) ↔ algebraic_independent R 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]
[algebra R A]
[subsingleton R] :
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 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.
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) :
algebraic_independent R coe → cardinal.mk ↥s ≤ ↑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
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)) :
algebraic_independent R (s.restrict x)
theorem
algebraic_independent_empty_iff
(R : Type u_3)
(A : Type u_5)
[comm_ring R]
[comm_ring A]
[algebra R A] :
algebraic_independent R (λ (x : ↥∅), ↑x) ↔ function.injective ⇑(algebra_map 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_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 ι} :
algebraic_independent R (x ∘ coe) ↔ ∀ (p : mv_polynomial ι R), p ∈ mv_polynomial.supported R s → ⇑(mv_polynomial.aeval x) p = 0 → p = 0
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 = 0 → p = 0
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)) :
algebraic_independent R (λ (x : ↥⋃₀ s), ↑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) :
↑(⇑(hx.aeval_equiv) ᾰ) = ⇑(mv_polynomial.aeval x) ᾰ
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) :
mv_polynomial ι R ≃ₐ[R] ↥(algebra.adjoin R (set.range x))
Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.
Equations
- hx.aeval_equiv = alg_equiv.of_bijective ((mv_polynomial.aeval x).cod_restrict (algebra.adjoin R (set.range x)) algebraic_independent.aeval_equiv._proof_1) _
@[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) :
⇑(algebra_map ↥(algebra.adjoin R (set.range x)) A) (⇑(hx.aeval_equiv) p) = ⇑(mv_polynomial.aeval x) p
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) :
↥(algebra.adjoin R (set.range x)) →ₐ[R] mv_polynomial ι R
The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.
Equations
- hx.repr = ↑(hx.aeval_equiv.symm)
@[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) :
(mv_polynomial.aeval x).comp hx.repr = (algebra.adjoin R (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]
[algebra R A]
(hx : algebraic_independent R x) :
ring_hom.ker ↑(hx.repr) = ⊥
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) :
mv_polynomial (option ι) R ≃+* polynomial ↥(algebra.adjoin R (set.range x))
The isomorphism between mv_polynomial (option ι) R and the polynomial ring over
the algebra generated by an algebraically independent family.
@[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]
[algebra R A]
(hx : algebraic_independent R x)
(y : mv_polynomial (option ι) R) :
⇑(hx.mv_polynomial_option_equiv_polynomial_adjoin) y = polynomial.map ↑(hx.aeval_equiv) (⇑(mv_polynomial.aeval (λ (o : option ι), option.elim polynomial.X (λ (s : ι), ⇑polynomial.C (mv_polynomial.X 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]
[algebra R A]
(hx : algebraic_independent R x)
(r : R) :
⇑(hx.mv_polynomial_option_equiv_polynomial_adjoin) (⇑mv_polynomial.C r) = ⇑polynomial.C (⇑(algebra_map R ↥(algebra.adjoin R (set.range x))) 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]
[algebra R A]
(hx : algebraic_independent R 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]
[algebra R A]
(hx : algebraic_independent R x)
(i : ι) :
⇑(hx.mv_polynomial_option_equiv_polynomial_adjoin) (mv_polynomial.X (option.some i)) = ⇑polynomial.C (⇑(hx.aeval_equiv) (mv_polynomial.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]
[algebra R A]
(hx : algebraic_independent R x)
(a : A) :
↑(polynomial.aeval a).comp hx.mv_polynomial_option_equiv_polynomial_adjoin.to_ring_hom = ↑(mv_polynomial.aeval (λ (o : option ι), option.elim a 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]
[algebra R A]
(hx : algebraic_independent R x)
(a : A) :
algebraic_independent R (λ (o : option ι), option.elim a x o) ↔ ¬is_algebraic ↥(algebra.adjoin R (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]
[algebra R A]
(x : ι → A) :
Prop
A family is a transcendence basis if it is a maximal algebraically independent subset.
Equations
- is_transcendence_basis R x = (algebraic_independent R x ∧ ∀ (s : set A), algebraic_independent R coe → set.range x ≤ s → set.range x = s)
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)) :
∃ (s : set A), is_transcendence_basis R coe
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) :
algebra.is_algebraic ↥(algebra.adjoin R (set.range 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]
[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] :